Sheaves of types on a Grothendieck topology

Defines the notion of a sheaf of types (usually called a sheaf of sets by mathematicians) on a category equipped with a Grothendieck topology, as well as a range of equivalent conditions useful in different situations.

In Mathlib/CategoryTheory/Sites/IsSheafFor.lean it is defined what it means for a presheaf to be a sheaf for a particular sieve. Given a Grothendieck topology J, P is a sheaf if it is a sheaf for every sieve in the topology. See IsSheaf.

In the case where the topology is generated by a basis, it suffices to check P is a sheaf for every presieve in the pretopology. See isSheaf_pretopology.

We also provide equivalent conditions to satisfy alternate definitions given in the literature.

• Stacks: In Equalizer.Presieve.sheaf_condition, the sheaf condition at a presieve is shown to be equivalent to that of https://stacks.math.columbia.edu/tag/00VM (and combined with isSheaf_pretopology, this shows the notions of IsSheaf are exactly equivalent.)

  The condition of https://stacks.math.columbia.edu/tag/00Z8 is virtually identical to the statement of isSheafFor_iff_yonedaSheafCondition (since the bijection described there carries the same information as the unique existence.)

• Maclane-Moerdijk [MM92]: Using compatible_iff_sieveCompatible, the definitions of IsSheaf are equivalent. There are also alternate definitions given:

  • Sheaf for a pretopology (Prop 1): isSheaf_pretopology combined with pullbackCompatible_iff.
  • Sheaf for a pretopology as equalizer (Prop 1, bis): Equalizer.Presieve.sheaf_condition combined with the previous.

References

• [MM92]: Sheaves in geometry and logic, Saunders MacLane, and Ieke Moerdijk: Chapter III, Section 4.
• [Elephant]: Sketches of an Elephant, P. T. Johnstone: C2.1.
• https://stacks.math.columbia.edu/tag/00VL (sheaves on a pretopology or site)
• https://stacks.math.columbia.edu/tag/00ZB (sheaves on a topology)

def CategoryTheory.Presieve.IsSeparated {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ (Type w)) : Prop

A presheaf is separated for a topology if it is separated for every sieve in the topology.

Equations

• CategoryTheory.Presieve.IsSeparated J P = ∀ {X : C}, ∀ S ∈ J.sieves X, CategoryTheory.Presieve.IsSeparatedFor P S.arrows

def CategoryTheory.Presieve.IsSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ (Type w)) : Prop

A presheaf is a sheaf for a topology if it is a sheaf for every sieve in the topology.

If the given topology is given by a pretopology, isSheaf_pretopology shows it suffices to check the sheaf condition at presieves in the pretopology.

Equations

• CategoryTheory.Presieve.IsSheaf J P = ∀ ⦃X : C⦄, ∀ S ∈ J.sieves X, CategoryTheory.Presieve.IsSheafFor P S.arrows

theorem CategoryTheory.Presieve.IsSheaf.isSheafFor {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (J : CategoryTheory.GrothendieckTopology C) {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (hp : CategoryTheory.Presieve.IsSheaf J P) (R : CategoryTheory.Presieve X) (hr : CategoryTheory.Sieve.generate R ∈ J.sieves X) : CategoryTheory.Presieve.IsSheafFor P R

theorem CategoryTheory.Presieve.isSheaf_of_le {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {J₁ : CategoryTheory.GrothendieckTopology C} {J₂ : CategoryTheory.GrothendieckTopology C} : J₁ ≤ J₂ → CategoryTheory.Presieve.IsSheaf J₂ P → CategoryTheory.Presieve.IsSheaf J₁ P

theorem CategoryTheory.Presieve.isSeparated_of_isSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ (Type w)) (h : CategoryTheory.Presieve.IsSheaf J P) : CategoryTheory.Presieve.IsSeparated J P

theorem CategoryTheory.Presieve.isSheaf_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (J : CategoryTheory.GrothendieckTopology C) {P' : CategoryTheory.Functor Cᵒᵖ (Type w)} (i : P ≅ P') (h : CategoryTheory.Presieve.IsSheaf J P) : CategoryTheory.Presieve.IsSheaf J P'

The property of being a sheaf is preserved by isomorphism.

theorem CategoryTheory.Presieve.isSheaf_of_yoneda {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {P : CategoryTheory.Functor Cᵒᵖ (Type v)} (h : ∀ {X : C}, ∀ S ∈ J.sieves X, CategoryTheory.Presieve.YonedaSheafCondition P S) : CategoryTheory.Presieve.IsSheaf J P

theorem CategoryTheory.Presieve.isSheaf_pretopology {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} [CategoryTheory.Limits.HasPullbacks C] (K : CategoryTheory.Pretopology C) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.Pretopology.toGrothendieck C K) P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor P R

For a topology generated by a basis, it suffices to check the sheaf condition on the basis presieves only.

theorem CategoryTheory.Presieve.isSheaf_bot {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} : CategoryTheory.Presieve.IsSheaf ⊥ P

Any presheaf is a sheaf for the bottom (trivial) grothendieck topology.

def CategoryTheory.Presieve.compatibleYonedaFamily_toCocone {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (R : CategoryTheory.Presieve X) (W : C) (x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.yoneda.obj W) R) (hx : CategoryTheory.Presieve.FamilyOfElements.Compatible x) : CategoryTheory.Limits.Cocone (CategoryTheory.Presieve.diagram R)

For a presheaf of the form yoneda.obj W, a compatible family of elements on a sieve is the same as a co-cone over the sieve. Constructing a co-cone from a compatible family works for any presieve, as does constructing a family of elements from a co-cone. Showing compatibility of the family needs the sieve condition. Note: This is related to CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily

Equations

• CategoryTheory.Presieve.compatibleYonedaFamily_toCocone R W x hx = { pt := W, ι := { app := fun (f : CategoryTheory.Presieve.category R) => x f.obj.hom ⋯, naturality := ⋯ } }

def CategoryTheory.Presieve.yonedaFamilyOfElements_fromCocone {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (R : CategoryTheory.Presieve X) (s : CategoryTheory.Limits.Cocone (CategoryTheory.Presieve.diagram R)) : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.yoneda.obj s.pt) R

Equations

• CategoryTheory.Presieve.yonedaFamilyOfElements_fromCocone R s f hf = s.ι.app { obj := CategoryTheory.Over.mk f, property := hf }

theorem CategoryTheory.Sieve.yonedaFamily_fromCocone_compatible {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (S : CategoryTheory.Sieve X) (s : CategoryTheory.Limits.Cocone (CategoryTheory.Presieve.diagram S.arrows)) : CategoryTheory.Presieve.FamilyOfElements.Compatible (CategoryTheory.Presieve.yonedaFamilyOfElements_fromCocone S.arrows s)

theorem CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (S : CategoryTheory.Sieve X) : (∀ (W : C), CategoryTheory.Presieve.IsSheafFor (CategoryTheory.yoneda.obj W) S.arrows) ↔ Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Presieve.cocone S.arrows))

The base of a sieve S is a colimit of S iff all Yoneda-presheaves satisfy the sheaf condition for S.

structure CategoryTheory.SheafOfTypes {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) : Type (max u v (w + 1))

The category of sheaves on a grothendieck topology.

• val : CategoryTheory.Functor Cᵒᵖ (Type w)

  the underlying presheaf

• cond : CategoryTheory.Presieve.IsSheaf J self.val

  the condition that the presheaf is a sheaf

theorem CategoryTheory.SheafOfTypes.Hom.ext_iff {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C} {X Y : CategoryTheory.SheafOfTypes J} (x y : CategoryTheory.SheafOfTypes.Hom X Y), x = y ↔ x.val = y.val

theorem CategoryTheory.SheafOfTypes.Hom.ext {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C} {X Y : CategoryTheory.SheafOfTypes J} (x y : CategoryTheory.SheafOfTypes.Hom X Y), x.val = y.val → x = y

structure CategoryTheory.SheafOfTypes.Hom {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (X : CategoryTheory.SheafOfTypes J) (Y : CategoryTheory.SheafOfTypes J) : Type (max u u_1)

Morphisms between sheaves of types are just morphisms between the underlying presheaves.

• val : X.val ⟶ Y.val

  a morphism between the underlying presheaves

@[simp]

theorem CategoryTheory.SheafOfTypes.instCategorySheafOfTypes_id_val {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} : ∀ (x : CategoryTheory.SheafOfTypes J), (CategoryTheory.CategoryStruct.id x).val = CategoryTheory.CategoryStruct.id x.val

@[simp]

theorem CategoryTheory.SheafOfTypes.instCategorySheafOfTypes_comp_val {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} : ∀ {X Y Z : CategoryTheory.SheafOfTypes J} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val

instance CategoryTheory.SheafOfTypes.instCategorySheafOfTypes {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} : CategoryTheory.Category.{max u u_1, max (max u v) (u_1 + 1)} (CategoryTheory.SheafOfTypes J)

Equations

• CategoryTheory.SheafOfTypes.instCategorySheafOfTypes = CategoryTheory.Category.mk ⋯ ⋯ ⋯

theorem CategoryTheory.SheafOfTypes.Hom.ext' {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : CategoryTheory.SheafOfTypes J} {Y : CategoryTheory.SheafOfTypes J} (f : X ⟶ Y) (g : X ⟶ Y) (w : f.val = g.val) : f = g

instance CategoryTheory.SheafOfTypes.instInhabitedHom {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (X : CategoryTheory.SheafOfTypes J) : Inhabited (CategoryTheory.SheafOfTypes.Hom X X)

Equations

• CategoryTheory.SheafOfTypes.instInhabitedHom X = { default := CategoryTheory.CategoryStruct.id X }

@[simp]

theorem CategoryTheory.sheafOfTypesToPresheaf_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (self : CategoryTheory.SheafOfTypes J) : (CategoryTheory.sheafOfTypesToPresheaf J).obj self = self.val

@[simp]

theorem CategoryTheory.sheafOfTypesToPresheaf_map {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) : ∀ {X Y : CategoryTheory.SheafOfTypes J} (f : X ⟶ Y), (CategoryTheory.sheafOfTypesToPresheaf J).map f = f.val

def CategoryTheory.sheafOfTypesToPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) : CategoryTheory.Functor (CategoryTheory.SheafOfTypes J) (CategoryTheory.Functor Cᵒᵖ (Type w))

The inclusion functor from sheaves to presheaves.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.instFullSheafOfTypesInstCategorySheafOfTypesFunctorOppositeOppositeTypeTypesCategorySheafOfTypesToPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) : CategoryTheory.Functor.Full (CategoryTheory.sheafOfTypesToPresheaf J)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.instFaithfulSheafOfTypesInstCategorySheafOfTypesFunctorOppositeOppositeTypeTypesCategorySheafOfTypesToPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) : CategoryTheory.Functor.Faithful (CategoryTheory.sheafOfTypesToPresheaf J)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.sheafOfTypesBotEquiv_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.sheafOfTypesBotEquiv.counitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.comp { toPrefunctor := { obj := fun (P : CategoryTheory.Functor Cᵒᵖ (Type w)) => { val := P, cond := ⋯ }, map := fun {X Y : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : X ⟶ Y) => (CategoryTheory.sheafOfTypesToPresheaf ⊥).preimage f }, map_id := ⋯, map_comp := ⋯ } (CategoryTheory.sheafOfTypesToPresheaf ⊥))

@[simp]

theorem CategoryTheory.sheafOfTypesBotEquiv_unitIso_inv_app_val {C : Type u} [CategoryTheory.Category.{v, u} C] : ∀ (x : CategoryTheory.SheafOfTypes ⊥), (CategoryTheory.sheafOfTypesBotEquiv.unitIso.inv.app x).val = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp (CategoryTheory.sheafOfTypesToPresheaf ⊥) { toPrefunctor := { obj := fun (P : CategoryTheory.Functor Cᵒᵖ (Type w)) => { val := P, cond := ⋯ }, map := fun {X Y : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : X ⟶ Y) => (CategoryTheory.sheafOfTypesToPresheaf ⊥).preimage f }, map_id := ⋯, map_comp := ⋯ }).obj x).val

@[simp]

theorem CategoryTheory.sheafOfTypesBotEquiv_functor {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.sheafOfTypesBotEquiv.functor = CategoryTheory.sheafOfTypesToPresheaf ⊥

@[simp]

theorem CategoryTheory.sheafOfTypesBotEquiv_inverse_map {C : Type u} [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : X ⟶ Y), CategoryTheory.sheafOfTypesBotEquiv.inverse.map f = (CategoryTheory.sheafOfTypesToPresheaf ⊥).preimage f

@[simp]

theorem CategoryTheory.sheafOfTypesBotEquiv_inverse_obj_val {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) : (CategoryTheory.sheafOfTypesBotEquiv.inverse.obj P).val = P

@[simp]

theorem CategoryTheory.sheafOfTypesBotEquiv_unitIso_hom_app_val {C : Type u} [CategoryTheory.Category.{v, u} C] : ∀ (x : CategoryTheory.SheafOfTypes ⊥), (CategoryTheory.sheafOfTypesBotEquiv.unitIso.hom.app x).val = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (CategoryTheory.SheafOfTypes ⊥)).obj x).val

def CategoryTheory.sheafOfTypesBotEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.SheafOfTypes ⊥ ≌ CategoryTheory.Functor Cᵒᵖ (Type w)

The category of sheaves on the bottom (trivial) grothendieck topology is equivalent to the category of presheaves.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.instInhabitedSheafOfTypesBotGrothendieckTopologyToBotInstCompleteLatticeGrothendieckTopology {C : Type u} [CategoryTheory.Category.{v, u} C] : Inhabited (CategoryTheory.SheafOfTypes ⊥)

Equations

• One or more equations did not get rendered due to their size.