Documentation

Mathlib.CategoryTheory.Sites.Sheaf

Sheaves taking values in a category #

If C is a category with a Grothendieck topology, we define the notion of a sheaf taking values in an arbitrary category A. We follow the definition in https://stacks.math.columbia.edu/tag/00VR, noting that the presheaf of sets "defined above" can be seen in the comments between tags 00VQ and 00VR on the page https://stacks.math.columbia.edu/tag/00VL. The advantage of this definition is that we need no assumptions whatsoever on A other than the assumption that the morphisms in C and A live in the same universe.

Implementation notes #

Occasionally we need to take a limit in A of a collection of morphisms of C indexed by a collection of objects in C. This turns out to force the morphisms of A to be in a sufficiently large universe. Rather than use UnivLE we prove some results for a category A' instead, whose morphism universe of A' is defined to be max u₁ v₁, where u₁, v₁ are the universes for C. Perhaps after we get better at handling universe inequalities this can be changed.

A sheaf of A is a presheaf P : Cᵒᵖ => A such that for every E : A, the presheaf of types given by sending U : C to Hom_{A}(E, P U) is a sheaf of types.

https://stacks.math.columbia.edu/tag/00VR

Equations
Instances For

    Condition that a presheaf with values in a concrete category is separated for a Grothendieck topology.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily_apply_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.Sieve X) (E : Aᵒᵖ) (π : (S.arrows.diagram.op.comp P).cones.obj E) (Y : C) (f : Y X) (h : S.arrows f) :
      ((CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily P S E) π) f h = π.app (Opposite.op { obj := CategoryTheory.Over.mk f, property := h })
      @[simp]
      theorem CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily_symm_apply_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.Sieve X) (E : Aᵒᵖ) (x : { x : CategoryTheory.Presieve.FamilyOfElements (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows // x.SieveCompatible }) (f : S.arrows.categoryᵒᵖ) :
      ((CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily P S E).symm x).app f = x (Opposite.unop f).obj.hom
      def CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.Sieve X) (E : Aᵒᵖ) :
      (S.arrows.diagram.op.comp P).cones.obj E { x : CategoryTheory.Presieve.FamilyOfElements (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows // x.SieveCompatible }

      Given a sieve S on X : C, a presheaf P : Cᵒᵖ ⥤ A, and an object E of A, the cones over the natural diagram S.arrows.diagram.op ⋙ P associated to S and P with cone point E are in 1-1 correspondence with sieve_compatible family of elements for the sieve S and the presheaf of types Hom (E, P -).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def CategoryTheory.Presieve.FamilyOfElements.SieveCompatible.cone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {P : CategoryTheory.Functor Cᵒᵖ A} {X : C} {S : CategoryTheory.Sieve X} {E : Aᵒᵖ} {x : CategoryTheory.Presieve.FamilyOfElements (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows} (hx : x.SieveCompatible) :
        CategoryTheory.Limits.Cone (S.arrows.diagram.op.comp P)

        The cone corresponding to a sieve_compatible family of elements, dot notation enabled.

        Equations
        Instances For
          def CategoryTheory.Presheaf.homEquivAmalgamation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {P : CategoryTheory.Functor Cᵒᵖ A} {X : C} {S : CategoryTheory.Sieve X} {E : Aᵒᵖ} {x : CategoryTheory.Presieve.FamilyOfElements (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows} (hx : x.SieveCompatible) :
          (hx.cone P.mapCone S.arrows.cocone.op) { t : (P.comp (CategoryTheory.coyoneda.obj E)).obj (Opposite.op X) // x.IsAmalgamation t }

          Cone morphisms from the cone corresponding to a sieve_compatible family to the natural cone associated to a sieve S and a presheaf P are in 1-1 correspondence with amalgamations of the family.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem CategoryTheory.Presheaf.isLimit_iff_isSheafFor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.Sieve X) :
            Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone S.arrows.cocone.op)) ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSheafFor (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows

            Given sieve S and presheaf P : Cᵒᵖ ⥤ A, their natural associated cone is a limit cone iff Hom (E, P -) is a sheaf of types for the sieve S and all E : A.

            theorem CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.Sieve X) :
            (∀ (c : CategoryTheory.Limits.Cone (S.arrows.diagram.op.comp P)), Subsingleton (c P.mapCone S.arrows.cocone.op)) ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSeparatedFor (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows

            Given sieve S and presheaf P : Cᵒᵖ ⥤ A, their natural associated cone admits at most one morphism from every cone in the same category (i.e. over the same diagram), iff Hom (E, P -)is separated for the sieve S and all E : A.

            A presheaf P is a sheaf for the Grothendieck topology J iff for every covering sieve S of J, the natural cone associated to P and S is a limit cone.

            theorem CategoryTheory.Presheaf.isSeparated_iff_subsingleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ A) :
            (∀ (E : A), CategoryTheory.Presieve.IsSeparated J (P.comp (CategoryTheory.coyoneda.obj (Opposite.op E)))) ∀ ⦃X : C⦄, SJ X, ∀ (c : CategoryTheory.Limits.Cone (S.arrows.diagram.op.comp P)), Subsingleton (c P.mapCone S.arrows.cocone.op)

            A presheaf P is separated for the Grothendieck topology J iff for every covering sieve S of J, the natural cone associated to P and S admits at most one morphism from every cone in the same category.

            Given presieve R and presheaf P : Cᵒᵖ ⥤ A, the natural cone associated to P and the sieve Sieve.generate R generated by R is a limit cone iff Hom (E, P -) is a sheaf of types for the presieve R and all E : A.

            A presheaf P is a sheaf for the Grothendieck topology generated by a pretopology K iff for every covering presieve R of K, the natural cone associated to P and Sieve.generate R is a limit cone.

            def CategoryTheory.Presheaf.IsSheaf.amalgamate {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {E : A} {X : C} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) (S : J.Cover X) (x : (I : S.Arrow) → E P.obj (Opposite.op I.Y)) (hx : ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂), CategoryTheory.CategoryStruct.comp (x I₁) (P.map r.g₁.op) = CategoryTheory.CategoryStruct.comp (x I₂) (P.map r.g₂.op)) :
            E P.obj (Opposite.op X)

            This is a wrapper around Presieve.IsSheafFor.amalgamate to be used below. If Ps a sheaf, S is a cover of X, and x is a collection of morphisms from E to P evaluated at terms in the cover which are compatible, then we can amalgamate the xs to obtain a single morphism E ⟶ P.obj (op X).

            Equations
            • hP.amalgamate S x hx = .amalgamate (fun (Y : C) (f : Y X) (hf : (↑S).arrows f) => x { Y := Y, f := f, hf := hf })
            Instances For
              @[simp]
              theorem CategoryTheory.Presheaf.IsSheaf.amalgamate_map_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {E : A} {X : C} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) (S : J.Cover X) (x : (I : S.Arrow) → E P.obj (Opposite.op I.Y)) (hx : ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂), CategoryTheory.CategoryStruct.comp (x I₁) (P.map r.g₁.op) = CategoryTheory.CategoryStruct.comp (x I₂) (P.map r.g₂.op)) (I : S.Arrow) {Z : A} (h : P.obj (Opposite.op I.Y) Z) :
              @[simp]
              theorem CategoryTheory.Presheaf.IsSheaf.amalgamate_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {E : A} {X : C} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) (S : J.Cover X) (x : (I : S.Arrow) → E P.obj (Opposite.op I.Y)) (hx : ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂), CategoryTheory.CategoryStruct.comp (x I₁) (P.map r.g₁.op) = CategoryTheory.CategoryStruct.comp (x I₂) (P.map r.g₂.op)) (I : S.Arrow) :
              CategoryTheory.CategoryStruct.comp (hP.amalgamate S x hx) (P.map I.f.op) = x I
              theorem CategoryTheory.Presheaf.IsSheaf.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {E : A} {X : C} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) (S : J.Cover X) (e₁ : E P.obj (Opposite.op X)) (e₂ : E P.obj (Opposite.op X)) (h : ∀ (I : S.Arrow), CategoryTheory.CategoryStruct.comp e₁ (P.map I.f.op) = CategoryTheory.CategoryStruct.comp e₂ (P.map I.f.op)) :
              e₁ = e₂
              theorem CategoryTheory.Presheaf.IsSheaf.hom_ext_ofArrows {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) {I : Type u_1} {S : C} {X : IC} (f : (i : I) → X i S) (hf : CategoryTheory.Sieve.ofArrows X f J S) {E : A} {x : E P.obj (Opposite.op S)} {y : E P.obj (Opposite.op S)} (h : ∀ (i : I), CategoryTheory.CategoryStruct.comp x (P.map (f i).op) = CategoryTheory.CategoryStruct.comp y (P.map (f i).op)) :
              x = y
              theorem CategoryTheory.Presheaf.IsSheaf.exists_unique_amalgamation_ofArrows {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) {I : Type u_1} {S : C} {X : IC} (f : (i : I) → X i S) (hf : CategoryTheory.Sieve.ofArrows X f J S) {E : A} (x : (i : I) → E P.obj (Opposite.op (X i))) (hx : ∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W X i) (b : W X j), CategoryTheory.CategoryStruct.comp a (f i) = CategoryTheory.CategoryStruct.comp b (f j)CategoryTheory.CategoryStruct.comp (x i) (P.map a.op) = CategoryTheory.CategoryStruct.comp (x j) (P.map b.op)) :
              ∃! g : E P.obj (Opposite.op S), ∀ (i : I), CategoryTheory.CategoryStruct.comp g (P.map (f i).op) = x i
              def CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) {I : Type u_1} {S : C} {X : IC} (f : (i : I) → X i S) (hf : CategoryTheory.Sieve.ofArrows X f J S) {E : A} (x : (i : I) → E P.obj (Opposite.op (X i))) (hx : ∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W X i) (b : W X j), CategoryTheory.CategoryStruct.comp a (f i) = CategoryTheory.CategoryStruct.comp b (f j)CategoryTheory.CategoryStruct.comp (x i) (P.map a.op) = CategoryTheory.CategoryStruct.comp (x j) (P.map b.op)) :
              E P.obj (Opposite.op S)

              If P : Cᵒᵖ ⥤ A is a sheaf and f i : X i ⟶ S is a covering family, then a morphism E ⟶ P.obj (op S) can be constructed from a compatible family of morphisms x : E ⟶ P.obj (op (X i)).

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows_map_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) {I : Type u_1} {S : C} {X : IC} (f : (i : I) → X i S) (hf : CategoryTheory.Sieve.ofArrows X f J S) {E : A} (x : (i : I) → E P.obj (Opposite.op (X i))) (hx : ∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W X i) (b : W X j), CategoryTheory.CategoryStruct.comp a (f i) = CategoryTheory.CategoryStruct.comp b (f j)CategoryTheory.CategoryStruct.comp (x i) (P.map a.op) = CategoryTheory.CategoryStruct.comp (x j) (P.map b.op)) (i : I) {Z : A} (h : P.obj (Opposite.op (X i)) Z) :
                @[simp]
                theorem CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) {I : Type u_1} {S : C} {X : IC} (f : (i : I) → X i S) (hf : CategoryTheory.Sieve.ofArrows X f J S) {E : A} (x : (i : I) → E P.obj (Opposite.op (X i))) (hx : ∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W X i) (b : W X j), CategoryTheory.CategoryStruct.comp a (f i) = CategoryTheory.CategoryStruct.comp b (f j)CategoryTheory.CategoryStruct.comp (x i) (P.map a.op) = CategoryTheory.CategoryStruct.comp (x j) (P.map b.op)) (i : I) :
                CategoryTheory.CategoryStruct.comp (hP.amalgamateOfArrows f hf x hx) (P.map (f i).op) = x i
                structure CategoryTheory.Sheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] :
                Type (max (max (max u₁ u₂) v₁) v₂)

                The category of sheaves taking values in A on a grothendieck topology.

                Instances For
                  theorem CategoryTheory.Sheaf.Hom.ext_iff {C : Type u₁} :
                  ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} A} {X Y : CategoryTheory.Sheaf J A} {x y : X.Hom Y}, x = y x.val = y.val
                  theorem CategoryTheory.Sheaf.Hom.ext {C : Type u₁} :
                  ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} A} {X Y : CategoryTheory.Sheaf J A} {x y : X.Hom Y}, x.val = y.valx = y

                  Morphisms between sheaves are just morphisms of presheaves.

                  • val : X.val Y.val

                    a morphism between the underlying presheaves

                  Instances For

                    The inclusion functor from sheaves to presheaves.

                    Equations
                    Instances For
                      @[reducible, inline]

                      The sections of a sheaf (i.e. evaluation as a presheaf on C).

                      Equations
                      Instances For

                        The functor Sheaf J A ⥤ Cᵒᵖ ⥤ A is fully faithful.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[reducible, inline]

                          The bijection (X ⟶ Y) ≃ (X.val ⟶ Y.val) when X and Y are sheaves.

                          Equations
                          Instances For

                            This is stated as a lemma to prevent class search from forming a loop since a sheaf morphism is monic if and only if it is monic as a presheaf morphism (under suitable assumption).

                            @[simp]
                            theorem CategoryTheory.sheafOver_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {J : CategoryTheory.GrothendieckTopology C} (ℱ : CategoryTheory.Sheaf J A) (E : A) :
                            (CategoryTheory.sheafOver E).val = .val.comp (CategoryTheory.coyoneda.obj (Opposite.op E))

                            The sheaf of sections guaranteed by the sheaf condition.

                            Equations
                            Instances For
                              @[simp]
                              theorem CategoryTheory.sheafEquivSheafOfTypes_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) :
                              (CategoryTheory.sheafEquivSheafOfTypes J).counitIso = CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.SheafOfTypes J) => CategoryTheory.Iso.refl (({ obj := fun (S : CategoryTheory.SheafOfTypes J) => { val := S.val, cond := }, map := fun {X Y : CategoryTheory.SheafOfTypes J} (f : X Y) => { val := f.val }, map_id := , map_comp := }.comp { obj := fun (S : CategoryTheory.Sheaf J (Type w)) => { val := S.val, cond := }, map := fun {X Y : CategoryTheory.Sheaf J (Type w)} (f : X Y) => { val := f.val }, map_id := , map_comp := }).obj X))

                              The category of sheaves taking values in Type is the same as the category of set-valued sheaves.

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

                                If the empty sieve is a cover of X, then F(X) is terminal.

                                Equations
                                Instances For
                                  Equations
                                  • CategoryTheory.sheafHomHasZSMul = { smul := fun (n : ) (f : P Q) => { val := { app := fun (U : Cᵒᵖ) => n f.val.app U, naturality := } } }
                                  Equations
                                  • CategoryTheory.instSubHomSheaf = { sub := fun (f g : P Q) => { val := f.val - g.val } }
                                  Equations
                                  • CategoryTheory.instNegHomSheaf = { neg := fun (f : P Q) => { val := -f.val } }
                                  Equations
                                  • CategoryTheory.sheafHomHasNSMul = { smul := fun (n : ) (f : P Q) => { val := { app := fun (U : Cᵒᵖ) => n f.val.app U, naturality := } } }
                                  Equations
                                  • CategoryTheory.instZeroHomSheaf = { zero := { val := 0 } }
                                  Equations
                                  • CategoryTheory.instAddHomSheaf = { add := fun (f g : P Q) => { val := f.val + g.val } }
                                  @[simp]
                                  theorem CategoryTheory.Sheaf.Hom.add_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.Preadditive A] {P : CategoryTheory.Sheaf J A} {Q : CategoryTheory.Sheaf J A} (f : P Q) (g : P Q) (U : Cᵒᵖ) :
                                  (f + g).val.app U = f.val.app U + g.val.app U
                                  Equations
                                  Equations
                                  • CategoryTheory.instPreadditiveSheaf = { homGroup := fun (P Q : CategoryTheory.Sheaf J A) => CategoryTheory.Sheaf.Hom.addCommGroup, add_comp := , comp_add := }

                                  When P is a sheaf and S is a cover, the associated multifork is a limit.

                                  Equations
                                  Instances For

                                    If F : Cᵒᵖ ⥤ A is a sheaf for a Grothendieck topology J on C, and S is a cover of X : C, then the multifork S.multifork F is limit.

                                    Equations
                                    • hP.isLimitMultifork S = .some
                                    Instances For

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

                                      Equations
                                      Instances For

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

                                        Equations
                                        Instances For

                                          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.

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

                                            An alternative definition of the sheaf condition in terms of equalizers. This is shown to be equivalent in CategoryTheory.Presheaf.isSheaf_iff_isSheaf'.

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

                                              For a concrete category (A, s) where the forgetful functor s : A ⥤ Type v preserves limits and reflects isomorphisms, and A has limits, an A-valued presheaf P : Cᵒᵖ ⥤ A is a sheaf iff its underlying Type-valued presheaf P ⋙ s : Cᵒᵖ ⥤ Type is a sheaf.

                                              Note this lemma applies for "algebraic" categories, eg groups, abelian groups and rings, but not for the category of topological spaces, topological rings, etc since reflecting isomorphisms doesn't hold.