Documentation

Mathlib.CategoryTheory.Sites.SheafOfTypes

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.

References #

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

Equations
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_of_le {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {J₁ J₂ : GrothendieckTopology C} :
      J₁ J₂IsSheaf J₂ PIsSheaf J₁ P
      theorem CategoryTheory.Presieve.isSheaf_of_nat_equiv {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {P₁ : Functor Cᵒᵖ (Type w)} {P₂ : Functor Cᵒᵖ (Type w')} (e : X : C⦄ → P₁.obj (Opposite.op X) P₂.obj (Opposite.op X)) (he : ∀ ⦃X Y : C⦄ (f : X Y) (x : P₁.obj (Opposite.op Y)), e (P₁.map f.op x) = P₂.map f.op (e x)) (hP₁ : IsSheaf J P₁) :
      IsSheaf J P₂
      theorem CategoryTheory.Presieve.isSheaf_iff_of_nat_equiv {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {P₁ : Functor Cᵒᵖ (Type w)} {P₂ : Functor Cᵒᵖ (Type w')} (e : X : C⦄ → P₁.obj (Opposite.op X) P₂.obj (Opposite.op X)) (he : ∀ ⦃X Y : C⦄ (f : X Y) (x : P₁.obj (Opposite.op Y)), e (P₁.map f.op x) = P₂.map f.op (e x)) :
      IsSheaf J P₁ IsSheaf J P₂
      theorem CategoryTheory.Presieve.isSheaf_iso {C : Type u} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type w)} (J : GrothendieckTopology C) {P' : Functor Cᵒᵖ (Type w)} (i : P P') (h : IsSheaf J P) :
      IsSheaf J P'

      The property of being a sheaf is preserved by isomorphism.

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

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

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

      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
      Instances For

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