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.

First define what it means for a presheaf P : Cᵒᵖ ⥤ Type v to be a sheaf for a particular presieve R on X:

In the special case where R is a sieve, the compatibility condition can be simplified:

In the special case where C has pullbacks, the compatibility condition can be simplified:

Now 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.

Implementation #

The sheaf condition is given as a proposition, rather than a subsingleton in Type (max u₁ v). This doesn't seem to make a big difference, other than making a couple of definitions noncomputable, but it means that equivalent conditions can be given as statements rather than statements, which can be convenient.

References #

A family of elements for a presheaf P given a collection of arrows R with fixed codomain X consists of an element of P Y for every f : Y ⟶ X in R. A presheaf is a sheaf (resp, separated) if every compatible family of elements has exactly one (resp, at most one) amalgamation.

This data is referred to as a family in [MM92], Chapter III, Section 4. It is also a concrete version of the elements of the middle object in https://stacks.math.columbia.edu/tag/00VM which is more useful for direct calculations. It is also used implicitly in Definition C2.1.2 in [Elephant].

Instances For

    A family of elements for a presheaf on the presieve R₂ can be restricted to a smaller presieve R₁.

    Instances For

      A family of elements for the arrow set R is compatible if for any f₁ : Y₁ ⟶ X and f₂ : Y₂ ⟶ X in R, and any g₁ : Z ⟶ Y₁ and g₂ : Z ⟶ Y₂, if the square g₁ ≫ f₁ = g₂ ≫ f₂ commutes then the elements of P Z obtained by restricting the element of P Y₁ along g₁ and restricting the element of P Y₂ along g₂ are the same.

      In special cases, this condition can be simplified, see pullbackCompatible_iff and compatible_iff_sieveCompatible.

      This is referred to as a "compatible family" in Definition C2.1.2 of [Elephant], and on nlab: https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents

      Instances For

        If the category C has pullbacks, this is an alternative condition for a family of elements to be compatible: For any f : Y ⟶ X and g : Z ⟶ X in the presieve R, the restriction of the given elements for f and g to the pullback agree. This is equivalent to being compatible (provided C has pullbacks), shown in pullbackCompatible_iff.

        This is the definition for a "matching" family given in [MM92], Chapter III, Section 4, Equation (5). Viewing the type FamilyOfElements as the middle object of the fork in https://stacks.math.columbia.edu/tag/00VM, this condition expresses that pr₀* (x) = pr₁* (x), using the notation defined there.

        Instances For

          Extend a family of elements to the sieve generated by an arrow set. This is the construction described as "easy" in Lemma C2.1.3 of [Elephant].

          Instances For

            If the arrow set for a family of elements is actually a sieve (i.e. it is downward closed) then the consistency condition can be simplified. This is an equivalent condition, see compatible_iff_sieveCompatible.

            This is the notion of "matching" given for families on sieves given in [MM92], Chapter III, Section 4, Equation 1, and nlab: https://ncatlab.org/nlab/show/matching+family. See also the discussion before Lemma C2.1.4 of [Elephant].

            Instances For
              @[simp]

              Given a family of elements x for the sieve S generated by a presieve R, if x is restricted to R and then extended back up to S, the resulting extension equals x.

              Compatible families of elements for a presheaf of types P and a presieve R are in 1-1 correspondence with compatible families for the same presheaf and the sieve generated by R, through extension and restriction.

              Instances For
                theorem CategoryTheory.Presieve.FamilyOfElements.comp_of_compatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {Y : C} (S : CategoryTheory.Sieve X) {x : CategoryTheory.Presieve.FamilyOfElements P S.arrows} (t : CategoryTheory.Presieve.FamilyOfElements.Compatible x) {f : Y X} (hf : S.arrows f) {Z : C} (g : Z Y) :
                x Z (CategoryTheory.CategoryStruct.comp g f) (_ : S.arrows (CategoryTheory.CategoryStruct.comp g f)) = Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver P.toPrefunctor (Opposite.op Y) (Opposite.op Z) g.op (x Y f hf)

                Given a family of elements of a sieve S on X whose values factors through F, we can realize it as a family of elements of S.functorPushforward F. Since the preimage is obtained by choice, this is not well-defined generally.

                Instances For

                  Given a family of elements of a sieve S on X, and a map Y ⟶ X, we can obtain a family of elements of S.pullback f by taking the same elements.

                  Instances For

                    Given a morphism of presheaves f : P ⟶ Q, we can take a family of elements valued in P to a family of elements valued in Q by composing with f.

                    Instances For

                      The given element t of P.obj (op X) is an amalgamation for the family of elements x if every restriction P.map f.op t = x_f for every arrow f in the presieve R.

                      This is the definition given in https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents, and https://ncatlab.org/nlab/show/matching+family, as well as [MM92], Chapter III, Section 4, equation (2).

                      Instances For

                        A presheaf is separated for a presieve if there is at most one amalgamation.

                        Instances For
                          theorem CategoryTheory.Presieve.IsSeparatedFor.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (hR : CategoryTheory.Presieve.IsSeparatedFor P R) {t₁ : P.obj (Opposite.op X)} {t₂ : P.obj (Opposite.op X)} (h : ∀ ⦃Y : C⦄ ⦃f : Y X⦄, R Y fCᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver P.toPrefunctor (Opposite.op X) (Opposite.op Y) f.op t₁ = Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver P.toPrefunctor (Opposite.op X) (Opposite.op Y) f.op t₂) :
                          t₁ = t₂

                          We define P to be a sheaf for the presieve R if every compatible family has a unique amalgamation.

                          This is the definition of a sheaf for the given presieve given in C2.1.2 of [Elephant], and https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents. Using compatible_iff_sieveCompatible, this is equivalent to the definition of a sheaf in [MM92], Chapter III, Section 4.

                          Instances For

                            This is an equivalent condition to be a sheaf, which is useful for the abstraction to local operators on elementary toposes. However this definition is defined only for sieves, not presieves. The equivalence between this and IsSheafFor is given in isSheafFor_iff_yonedaSheafCondition. This version is also useful to establish that being a sheaf is preserved under isomorphism of presheaves.

                            See the discussion before Equation (3) of [MM92], Chapter III, Section 4. See also C2.1.4 of [Elephant]. This is also a direct reformulation of https://stacks.math.columbia.edu/tag/00Z8.

                            Instances For

                              (Implementation). This is a (primarily internal) equivalence between natural transformations and compatible families.

                              Cf the discussion after Lemma 7.47.10 in https://stacks.math.columbia.edu/tag/00YW. See also the proof of C2.1.4 of [Elephant], and the discussion in [MM92], Chapter III, Section 4.

                              Instances For
                                theorem CategoryTheory.Presieve.extension_iff_amalgamation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (x : CategoryTheory.Sieve.functor S P) (g : CategoryTheory.yoneda.obj X P) :
                                CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.functorInclusion S) g = x CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation (↑(CategoryTheory.Presieve.natTransEquivCompatibleFamily x)) (CategoryTheory.yonedaEquiv g)

                                (Implementation). A lemma useful to prove isSheafFor_iff_yonedaSheafCondition.

                                The yoneda version of the sheaf condition is equivalent to the sheaf condition.

                                C2.1.4 of [Elephant].

                                If P is a sheaf for the sieve S on X, a natural transformation from S (viewed as a functor) to P can be (uniquely) extended to all of yoneda.obj X.

                                  f
                                

                                S → P ↓ ↗ yX

                                Instances For
                                  @[simp]

                                  Show that the extension of f : S.functor ⟶ P to all of yoneda.obj X is in fact an extension, ie that the triangle below commutes, provided P is a sheaf for S

                                    f
                                  

                                  S → P ↓ ↗ yX

                                  If P is a sheaf for the sieve S on X, then if two natural transformations from yoneda.obj X to P agree when restricted to the subfunctor given by S, they are equal.

                                  Get the amalgamation of the given compatible family, provided we have a sheaf.

                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.Presieve.IsSheafFor.valid_glue {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {Y : C} {R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSheafFor P R) {x : CategoryTheory.Presieve.FamilyOfElements P R} (hx : CategoryTheory.Presieve.FamilyOfElements.Compatible x) (f : Y X) (Hf : R Y f) :
                                    Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver P.toPrefunctor (Opposite.op X) (Opposite.op Y) f.op (CategoryTheory.Presieve.IsSheafFor.amalgamate t x hx) = x Y f Hf

                                    Every presheaf is a sheaf for the maximal sieve.

                                    [Elephant] C2.1.5(ii)

                                    If P is a sheaf for S, and it is iso to P', then P' is a sheaf for S. This shows that "being a sheaf for a presieve" is a mathematical or hygienic property.

                                    If a presieve R on X has a subsieve S such that:

                                    • P is a sheaf for S.
                                    • For every f in R, P is separated for the pullback of S along f,

                                    then P is a sheaf for R.

                                    This is closely related to [Elephant] C2.1.6(i).

                                    If P is a sheaf for every pullback of the sieve S, then P is a sheaf for any presieve which contains S. This is closely related to [Elephant] C2.1.6.

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

                                    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.

                                      Instances For

                                        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

                                        Instances For

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

                                          The middle object of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram of https://stacks.math.columbia.edu/tag/00VM.

                                          Instances For
                                            theorem CategoryTheory.Equalizer.FirstObj.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))} {X : C} {R : CategoryTheory.Presieve X} (z₁ : CategoryTheory.Equalizer.FirstObj P R) (z₂ : CategoryTheory.Equalizer.FirstObj P R) (h : ∀ (Y : C) (f : Y X) (hf : R Y f), CategoryTheory.Limits.Pi.π ((Y : C) × { f // R Y f }) (Type (max v₁ u₁)) CategoryTheory.types (fun f => P.obj (Opposite.op f.fst)) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => P.obj (Opposite.op f.fst))) { fst := Y, snd := { val := f, property := hf } } z₁ = CategoryTheory.Limits.Pi.π ((Y : C) × { f // R Y f }) (Type (max v₁ u₁)) CategoryTheory.types (fun f => P.obj (Opposite.op f.fst)) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => P.obj (Opposite.op f.fst))) { fst := Y, snd := { val := f, property := hf } } z₂) :
                                            z₁ = z₂
                                            @[simp]
                                            theorem CategoryTheory.Equalizer.firstObjEqFamily_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (R : CategoryTheory.Presieve X) (t : CategoryTheory.Equalizer.FirstObj P R) (Y : C) (f : Y X) (hf : R Y f) :
                                            Type (max v₁ u₁).hom CategoryTheory.types (CategoryTheory.Equalizer.FirstObj P R) (CategoryTheory.Presieve.FamilyOfElements P R) (CategoryTheory.Equalizer.firstObjEqFamily P R) t Y f hf = CategoryTheory.Limits.Pi.π ((Y : C) × { f // R Y f }) (Type (max v₁ u₁)) CategoryTheory.types (fun f => P.obj (Opposite.op f.fst)) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => P.obj (Opposite.op f.fst))) { fst := Y, snd := { val := f, property := hf } } t

                                            The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram of https://stacks.math.columbia.edu/tag/00VM.

                                            Instances For

                                              This section establishes the equivalence between the sheaf condition of Equation (3) [MM92] and the definition of IsSheafFor.

                                              The rightmost object of the fork diagram of Equation (3) [MM92], which contains the data used to check a family is compatible.

                                              Instances For
                                                theorem CategoryTheory.Equalizer.Sieve.SecondObj.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))} {X : C} {S : CategoryTheory.Sieve X} (z₁ : CategoryTheory.Equalizer.Sieve.SecondObj P S) (z₂ : CategoryTheory.Equalizer.Sieve.SecondObj P S) (h : ∀ (Y Z : C) (g : Z Y) (f : Y X) (hf : S.arrows f), CategoryTheory.Limits.Pi.π ((Y : C) × (Z : C) × (_ : Z Y) × { f' // S.arrows f' }) (Type (max v₁ u₁)) CategoryTheory.types (fun f => P.obj (Opposite.op f.snd.fst)) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => P.obj (Opposite.op f.snd.fst))) { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } z₁ = CategoryTheory.Limits.Pi.π ((Y : C) × (Z : C) × (_ : Z Y) × { f' // S.arrows f' }) (Type (max v₁ u₁)) CategoryTheory.types (fun f => P.obj (Opposite.op f.snd.fst)) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => P.obj (Opposite.op f.snd.fst))) { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } z₂) :
                                                z₁ = z₂

                                                This section establishes the equivalence between the sheaf condition of https://stacks.math.columbia.edu/tag/00VM and the definition of isSheafFor.

                                                The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which contains the data used to check a family of elements for a presieve is compatible.

                                                Instances For

                                                  The category of sheaves on a grothendieck topology.

                                                  Instances For
                                                    • val : X.val Y.val

                                                      a morphism between the underlying presheaves

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

                                                    Instances For
                                                      @[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]

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

                                                      Instances For