Documentation

Mathlib.CategoryTheory.Sites.IsSheafFor

The sheaf condition for a presieve #

We 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:

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 [MLM92], 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 [Joh02].

Equations
Instances For
    Equations
    • CategoryTheory.Presieve.instInhabitedFamilyOfElementsBot = { default := fun (x : C) (x_1 : x X) => False.elim }

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

    Equations
    Instances For

      The image of a family of elements by a morphism of presheaves.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.Presieve.FamilyOfElements.map_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (p : CategoryTheory.Presieve.FamilyOfElements P R) (φ : P Q) {Y : C} (f : Y X) (hf : R f) :
        p.map φ f hf = φ.app (Opposite.op Y) (p f hf)

        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 [Joh02], and on nlab: https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents

        For a more explicit version in the case where R is of the form Presieve.ofArrows, see CategoryTheory.Presieve.Arrows.Compatible.

        Equations
        • One or more equations did not get rendered due to their size.
        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 [MLM92], 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.

          For a more explicit version in the case where R is of the form Presieve.ofArrows, see CategoryTheory.Presieve.Arrows.PullbackCompatible.

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

            The restriction of a compatible family is compatible.

            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 [Joh02].

            Equations
            • x✝¹.sieveExtend x hf = P.map .choose.op (x✝¹ .choose )
            Instances For

              The extension of a compatible family to the generated sieve is compatible.

              theorem CategoryTheory.Presieve.extend_agrees {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C} {R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P R} (t : x.Compatible) {f : Y X} (hf : R f) :
              x.sieveExtend f = x f hf

              The extension of a family agrees with the original family.

              @[simp]

              The restriction of an extension is the original.

              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 [MLM92], 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 [Joh02].

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

                Two compatible families on the sieve generated by a presieve R are equal if and only if they are equal when restricted to R.

                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.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_apply_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : { x : CategoryTheory.Presieve.FamilyOfElements P R // x.Compatible }) :
                  (CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible x) = (↑x).sieveExtend
                  theorem CategoryTheory.Presieve.FamilyOfElements.comp_of_compatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C} (S : CategoryTheory.Sieve X) {x : CategoryTheory.Presieve.FamilyOfElements P S.arrows} (t : x.Compatible) {f : Y X} (hf : S.arrows f) {Z : C} (g : Z Y) :
                  x (CategoryTheory.CategoryStruct.comp g f) = P.map g.op (x 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.

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

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

                      Equations
                      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 [MLM92], Chapter III, Section 4, equation (2).

                        Equations
                        • x.IsAmalgamation t = ∀ ⦃Y : C⦄ (f : Y X) (h : R f), P.map f.op t = x f h
                        Instances For
                          theorem CategoryTheory.Presieve.isAmalgamation_sieveExtend {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) (t : P.obj (Opposite.op X)) (ht : x.IsAmalgamation t) :
                          x.sieveExtend.IsAmalgamation t

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

                          Equations
                          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₁ t₂ : P.obj (Opposite.op X)} (h : ∀ ⦃Y : C⦄ ⦃f : Y X⦄, R fP.map f.op t₁ = P.map 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 [Joh02], and https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents. Using compatible_iff_sieveCompatible, this is equivalent to the definition of a sheaf in [MLM92], Chapter III, Section 4.

                            Equations
                            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 [MLM92], Chapter III, Section 4. See also C2.1.4 of [Joh02]. This is also a direct reformulation of https://stacks.math.columbia.edu/tag/00Z8.

                              Equations
                              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 [Joh02], and the discussion in [MLM92], Chapter III, Section 4.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                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 : S.functor P) (g : CategoryTheory.yoneda.obj X P) :
                                  CategoryTheory.CategoryStruct.comp S.functorInclusion g = x (↑(CategoryTheory.Presieve.natTransEquivCompatibleFamily x)).IsAmalgamation (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 [Joh02].

                                  noncomputable def CategoryTheory.Presieve.IsSheafFor.extend {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (f : S.functor P) :
                                  CategoryTheory.yoneda.obj X P

                                  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

                                  Equations
                                  • h.extend f = .choose
                                  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

                                    theorem CategoryTheory.Presieve.IsSheafFor.unique_extend {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) {f : S.functor P} (t : CategoryTheory.yoneda.obj X P) (ht : CategoryTheory.CategoryStruct.comp S.functorInclusion t = f) :
                                    t = h.extend f

                                    The extension of f to yoneda.obj X is unique.

                                    theorem CategoryTheory.Presieve.IsSheafFor.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (t₁ t₂ : CategoryTheory.yoneda.obj X P) (ht : CategoryTheory.CategoryStruct.comp S.functorInclusion t₁ = CategoryTheory.CategoryStruct.comp S.functorInclusion t₂) :
                                    t₁ = t₂

                                    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.

                                    P is a sheaf for R iff it is separated for R and there exists an amalgamation.

                                    If P is separated for R and every family has an amalgamation, then P is a sheaf for R.

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

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

                                      Every presheaf is a sheaf for the maximal sieve.

                                      [Joh02] 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 [Joh02] 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 [Joh02] C2.1.6.

                                      def CategoryTheory.Presieve.Arrows.Compatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : IC} (π : (i : I) → X i B) (x : (i : I) → P.obj (Opposite.op (X i))) :

                                      A more explicit version of FamilyOfElements.Compatible for a Presieve.ofArrows.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_iff_ofArrows {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : IC} (π : (i : I) → X i B) (x : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.ofArrows X π)) (t : P.obj (Opposite.op B)) :
                                        x.IsAmalgamation t ∀ (i : I), P.map (π i).op t = x (π i)
                                        theorem CategoryTheory.Presieve.Arrows.Compatible.exists_familyOfElements {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {B : C} {I : Type u_1} {X : IC} {π : (i : I) → X i B} {x : (i : I) → P.obj (Opposite.op (X i))} (hx : CategoryTheory.Presieve.Arrows.Compatible P π x) :
                                        ∃ (x' : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.ofArrows X π)), ∀ (i : I), x' (π i) = x i

                                        A FamilyOfElements associated to an explicit family of elements.

                                        Equations
                                        • hx.familyOfElements = .choose
                                        Instances For
                                          @[simp]
                                          theorem CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_ofArrows_mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {B : C} {I : Type u_1} {X : IC} {π : (i : I) → X i B} {x : (i : I) → P.obj (Opposite.op (X i))} (hx : CategoryTheory.Presieve.Arrows.Compatible P π x) (i : I) :
                                          hx.familyOfElements (π i) = x i
                                          theorem CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_compatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {B : C} {I : Type u_1} {X : IC} {π : (i : I) → X i B} {x : (i : I) → P.obj (Opposite.op (X i))} (hx : CategoryTheory.Presieve.Arrows.Compatible P π x) :
                                          hx.familyOfElements.Compatible
                                          theorem CategoryTheory.Presieve.isSheafFor_arrows_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : IC} (π : (i : I) → X i B) :
                                          CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ∀ (x : (i : I) → P.obj (Opposite.op (X i))), CategoryTheory.Presieve.Arrows.Compatible P π x∃! t : P.obj (Opposite.op B), ∀ (i : I), P.map (π i).op t = x i
                                          def CategoryTheory.Presieve.Arrows.PullbackCompatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : IC} (π : (i : I) → X i B) [(CategoryTheory.Presieve.ofArrows X π).hasPullbacks] (x : (i : I) → P.obj (Opposite.op (X i))) :

                                          A more explicit version of FamilyOfElements.PullbackCompatible for a Presieve.ofArrows.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            theorem CategoryTheory.Presieve.isSheafFor_arrows_iff_pullbacks {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : IC} (π : (i : I) → X i B) [(CategoryTheory.Presieve.ofArrows X π).hasPullbacks] :
                                            CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ∀ (x : (i : I) → P.obj (Opposite.op (X i))), CategoryTheory.Presieve.Arrows.PullbackCompatible P π x∃! t : P.obj (Opposite.op B), ∀ (i : I), P.map (π i).op t = x i