# 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 [MLM92]: 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 #

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

Equations
• = ∀ {X : C}, SJ.sieves X,
Instances For

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
Instances For
theorem CategoryTheory.Presieve.IsSheaf.isSheafFor {C : Type u} {X : C} {P : } (hp : ) (R : ) (hr : J.sieves X) :
theorem CategoryTheory.Presieve.isSheaf_of_le {C : Type u} (P : ) :
J₁ J₂
theorem CategoryTheory.Presieve.isSheaf_iso {C : Type u} {P : } {P' : } (i : P P') (h : ) :

The property of being a sheaf is preserved by isomorphism.

theorem CategoryTheory.Presieve.isSheaf_of_yoneda {C : Type u} {P : } (h : ∀ {X : C}, SJ.sieves X, ) :
theorem CategoryTheory.Presieve.isSheaf_pretopology {C : Type u} {P : } (K : ) :
∀ {X : C}, RK.coverings X,

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} {P : } :

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

def CategoryTheory.Presieve.compatibleYonedaFamily_toCocone {C : Type u} {X : C} (R : ) (W : C) (x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.yoneda.obj W) R) (hx : x.Compatible) :

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
• R.compatibleYonedaFamily_toCocone W x hx = { pt := W, ι := { app := fun (f : R.category) => x f.obj.hom , naturality := } }
Instances For
Equations
• R.yonedaFamilyOfElements_fromCocone s f hf = s.app { obj := , property := hf }
Instances For
theorem CategoryTheory.Sieve.yonedaFamily_fromCocone_compatible {C : Type u} {X : C} (S : ) (s : CategoryTheory.Limits.Cocone S.arrows.diagram) :
(S.arrows.yonedaFamilyOfElements_fromCocone s).Compatible
theorem CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit {C : Type u} {X : C} (S : ) :
(∀ (W : C), CategoryTheory.Presieve.IsSheafFor (CategoryTheory.yoneda.obj W) S.arrows) Nonempty (CategoryTheory.Limits.IsColimit S.arrows.cocone)

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} :
Type (max u v (w + 1))

The category of sheaves on a grothendieck topology.

Instances For

the condition that the presheaf is a sheaf

theorem CategoryTheory.SheafOfTypes.Hom.ext_iff {C : Type u} :
∀ {inst : } {J : } {X Y : } (x y : X.Hom Y), x = y x.val = y.val
theorem CategoryTheory.SheafOfTypes.Hom.ext {C : Type u} :
∀ {inst : } {J : } {X Y : } (x y : X.Hom Y), x.val = y.valx = y
structure CategoryTheory.SheafOfTypes.Hom {C : Type u} (X : ) (Y : ) :
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

Instances For
@[simp]
@[simp]
theorem CategoryTheory.SheafOfTypes.instCategory_comp_val {C : Type u} :
∀ {X Y Z : } (f : X Y) (g : Y Z), .val = CategoryTheory.CategoryStruct.comp f.val g.val
Equations
• CategoryTheory.SheafOfTypes.instCategory =
theorem CategoryTheory.SheafOfTypes.Hom.ext' {C : Type u} {X : } {Y : } (f : X Y) (g : X Y) (w : f.val = g.val) :
f = g
Equations
• X.instInhabitedHom = { default := }
@[simp]
theorem CategoryTheory.sheafOfTypesToPresheaf_obj {C : Type u} (self : ) :
self = self.val
@[simp]
theorem CategoryTheory.sheafOfTypesToPresheaf_map {C : Type u} :
∀ {X Y : } (f : X Y), = f.val

The inclusion functor from sheaves to presheaves.

Equations
• = { obj := CategoryTheory.SheafOfTypes.val, map := fun {X Y : } (f : X Y) => f.val, map_id := , map_comp := }
Instances For
Equations
• =
Equations
• =
@[simp]
theorem CategoryTheory.sheafOfTypesBotEquiv_unitIso {C : Type u} :
CategoryTheory.sheafOfTypesBotEquiv.unitIso =
@[simp]
theorem CategoryTheory.sheafOfTypesBotEquiv_functor {C : Type u} :
CategoryTheory.sheafOfTypesBotEquiv.functor =
@[simp]
theorem CategoryTheory.sheafOfTypesBotEquiv_inverse_map_val {C : Type u} :
∀ {X Y : } (f : X Y), (CategoryTheory.sheafOfTypesBotEquiv.inverse.map f).val = f
@[simp]
theorem CategoryTheory.sheafOfTypesBotEquiv_counitIso {C : Type u} :
CategoryTheory.sheafOfTypesBotEquiv.counitIso = CategoryTheory.Iso.refl ({ obj := fun (P : ) => { val := P, cond := }, map := fun {X Y : } (f : X Y) => { val := f }, map_id := , map_comp := }.comp )
@[simp]
theorem CategoryTheory.sheafOfTypesBotEquiv_inverse_obj_val {C : Type u} (P : ) :
(CategoryTheory.sheafOfTypesBotEquiv.inverse.obj P).val = P

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.
Instances For
Equations
• One or more equations did not get rendered due to their size.