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

      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
      • R.compatibleYonedaFamily_toCocone W x hx = { pt := W, ι := { app := fun (f : R.category) => x f.obj.hom , naturality := } }
      Instances For
        Equations
        Instances For
          theorem CategoryTheory.Sieve.yonedaFamily_fromCocone_compatible {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (S : CategoryTheory.Sieve X) (s : CategoryTheory.Limits.Cocone S.arrows.diagram) :
          (S.arrows.yonedaFamilyOfElements_fromCocone s).Compatible

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

          The category of sheaves on a grothendieck topology.

          Instances For
            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 : X.Hom Y), x.val = y.valx = y

            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

              The inclusion functor from sheaves to presheaves.

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.sheafOfTypesBotEquiv_inverse_map_val {C : Type u} [CategoryTheory.Category.{v, u} C] :
                ∀ {X Y : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : X Y), (CategoryTheory.sheafOfTypesBotEquiv.inverse.map f).val = f
                @[simp]
                theorem CategoryTheory.sheafOfTypesBotEquiv_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] :
                CategoryTheory.sheafOfTypesBotEquiv.counitIso = CategoryTheory.Iso.refl ({ obj := fun (P : CategoryTheory.Functor Cᵒᵖ (Type w)) => { val := P, cond := }, map := fun {X Y : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : X Y) => { val := f }, map_id := , map_comp := }.comp (CategoryTheory.sheafOfTypesToPresheaf ))
                @[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

                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.