Let X be a preorder ≤, and consider the associated Alexandrov topology on X. Given a functor F : X ⥤ C to a complete category, we can extend F to a presheaf on (the topological space) X by taking the right Kan extension along the canonical functor X ⥤ (Opens X)ᵒᵖ sending x : X to the principal open {y | x ≤ y} in the Alexandrov topology.

This file proves that this presheaf is a sheaf.

def Alexandrov.principalOpen {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] (x : X) : TopologicalSpace.Opens X

Given x : X, this is the principal open subset of X generated by x.

theorem Alexandrov.self_mem_principalOpen {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] (x : X) : x ∈ principalOpen x

@[simp]

theorem Alexandrov.principalOpen_le_iff {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] {x : X} (U : TopologicalSpace.Opens X) : principalOpen x ≤ U ↔ x ∈ U

theorem Alexandrov.principalOpen_le {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] {x y : X} (h : x ≤ y) : principalOpen y ≤ principalOpen x

def Alexandrov.principals (X : Type v) [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] : CategoryTheory.Functor X (TopologicalSpace.Opens X)ᵒᵖ

The functor sending x : X to the principal open associated with x.

@[simp]

theorem Alexandrov.principals_map (X : Type v) [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] {x y : X} (f : x ⟶ y) : (principals X).map f = ⋯.hom.op

@[simp]

theorem Alexandrov.principals_obj (X : Type v) [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] (x : X) : (principals X).obj x = Opposite.op (principalOpen x)

theorem Alexandrov.exists_le_of_le_sup {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] {ι : Type v} {x : X} (Us : ι → TopologicalSpace.Opens X) (h : principalOpen x ≤ iSup Us) : ∃ (i : ι), principalOpen x ≤ Us i

@[reducible, inline]

noncomputable abbrev Alexandrov.principalsKanExtension {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] (F : CategoryTheory.Functor X C) : CategoryTheory.Functor (TopologicalSpace.Opens X)ᵒᵖ C

The right Kan extension of F along X ⥤ (Opens X)ᵒᵖ.

@[reducible, inline]

abbrev Alexandrov.generator {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] (U : TopologicalSpace.Opens X) : CategoryTheory.Functor (CategoryTheory.StructuredArrow (Opposite.op U) (principals X)) X

Given a structured arrow f with domain U : Opens X over principals X, this functor sends f to its "generator", an element of X.

def Alexandrov.projSup {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] {ι : Type v} (Us : ι → TopologicalSpace.Opens X) : CategoryTheory.Functor (CategoryTheory.StructuredArrow (Opposite.op (iSup Us)) (principals X)) (TopCat.Presheaf.SheafCondition.OpensLeCover Us)ᵒᵖ

Given a structured arrow f with domain iSup Us over principals X, where Us is a family of Opens X, this functor sends f to the principal open associated with it, considered as an object in the full subcategory of all V : Opens X such that V ≤ Us i for some i.

This definition is primarily meant to be used in lowerCone, and isLimit below.

@[simp]

theorem Alexandrov.projSup_obj {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] {ι : Type v} (Us : ι → TopologicalSpace.Opens X) (f : CategoryTheory.StructuredArrow (Opposite.op (iSup Us)) (principals X)) : (projSup Us).obj f = Opposite.op { obj := principalOpen f.right, property := ⋯ }

@[simp]

theorem Alexandrov.projSup_map {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] {ι : Type v} (Us : ι → TopologicalSpace.Opens X) {X✝ Y✝ : CategoryTheory.StructuredArrow (Opposite.op (iSup Us)) (principals X)} (e : X✝ ⟶ Y✝) : (projSup Us).map e = (CategoryTheory.ObjectProperty.homMk (CategoryTheory.homOfLE ⋯)).op

noncomputable def Alexandrov.lowerCone {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {F : CategoryTheory.Functor X C} {α : Type v} (Us : α → TopologicalSpace.Opens X) (S : CategoryTheory.Limits.Cone ((CategoryTheory.ObjectProperty.ι fun (V : TopologicalSpace.Opens ↑(TopCat.of X)) => ∃ (i : α), V ≤ Us i).op.comp (principalsKanExtension F))) : CategoryTheory.Limits.Cone ((generator (iSup Us)).comp F)

This is an auxiliary definition which is only meant to be used in isLimit below.

@[simp]

theorem Alexandrov.lowerCone_pt {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {F : CategoryTheory.Functor X C} {α : Type v} (Us : α → TopologicalSpace.Opens X) (S : CategoryTheory.Limits.Cone ((CategoryTheory.ObjectProperty.ι fun (V : TopologicalSpace.Opens ↑(TopCat.of X)) => ∃ (i : α), V ≤ Us i).op.comp (principalsKanExtension F))) : (lowerCone Us S).pt = S.pt

@[simp]

theorem Alexandrov.lowerCone_π_app {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {F : CategoryTheory.Functor X C} {α : Type v} (Us : α → TopologicalSpace.Opens X) (S : CategoryTheory.Limits.Cone ((CategoryTheory.ObjectProperty.ι fun (V : TopologicalSpace.Opens ↑(TopCat.of X)) => ∃ (i : α), V ≤ Us i).op.comp (principalsKanExtension F))) (f : CategoryTheory.StructuredArrow (Opposite.op (iSup Us)) (principals X)) : (lowerCone Us S).π.app f = CategoryTheory.CategoryStruct.comp (S.π.app ((projSup Us).obj f)) (CategoryTheory.Limits.limit.π ((generator (principalOpen f.right)).comp F) { left := { as := PUnit.unit }, right := f.right, hom := CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.fromPUnit (Opposite.op (principalOpen f.right))).obj { as := PUnit.unit }) })

noncomputable def Alexandrov.isLimit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {X : TopCat} [Preorder ↑X] [Topology.IsUpperSet ↑X] (F : CategoryTheory.Functor (↑X) C) (α : Type v) (Us : α → TopologicalSpace.Opens ↑X) : CategoryTheory.Limits.IsLimit ((principalsKanExtension F).mapCone (TopCat.Presheaf.SheafCondition.opensLeCoverCocone Us).op)

This is the main construction in this file showing that the right Kan extension of F : X ⥤ C along principals : X ⥤ (Opens X)ᵒᵖ is a sheaf, by showing that a certain cone is a limit cone.

See isSheaf_principalsKanExtension for the main application.

theorem Alexandrov.isSheaf_principalsKanExtension {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {X : TopCat} [Preorder ↑X] [Topology.IsUpperSet ↑X] (F : CategoryTheory.Functor (↑X) C) : TopCat.Presheaf.IsSheaf (principalsKanExtension F)

theorem Topology.IsUpperSet.isSheaf_of_isRightKanExtension {X : Type v} [TopologicalSpace X] [Preorder X] [Topology.IsUpperSet X] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] (F : CategoryTheory.Functor X C) (P : CategoryTheory.Functor (TopologicalSpace.Opens X)ᵒᵖ C) (η : (Alexandrov.principals X).comp P ⟶ F) [P.IsRightKanExtension η] : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology X) P

The main theorem of this file. If X is a topological space and preorder whose topology is the UpperSet topology associated with the preorder, F : X ⥤ C is a functor into a complete category from the preorder category, and P : (Opens X)ᵒᵖ ⥤ C denotes the right Kan extension of F along the functor X ⥤ (Open X)ᵒᵖ which sends x : X to {y | x ≤ y}, then P is a sheaf.