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_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 f.unop.obj.hom
      @[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 { unop := { obj := CategoryTheory.Over.mk f, property := h } }
      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 { unop := 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 { unop := E }))) ∀ ⦃X : C⦄, SJ.sieves 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 { unop := I.Y }) (hx : ∀ (I : S.Relation), CategoryTheory.CategoryStruct.comp (x I.fst) (P.map I.g₁.op) = CategoryTheory.CategoryStruct.comp (x I.snd) (P.map I.g₂.op)) :
            E P.obj { unop := 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.sieve.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 { unop := I.Y }) (hx : ∀ (I : S.Relation), CategoryTheory.CategoryStruct.comp (x I.fst) (P.map I.g₁.op) = CategoryTheory.CategoryStruct.comp (x I.snd) (P.map I.g₂.op)) (I : S.Arrow) {Z : A} (h : P.obj { unop := 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 { unop := I.Y }) (hx : ∀ (I : S.Relation), CategoryTheory.CategoryStruct.comp (x I.fst) (P.map I.g₁.op) = CategoryTheory.CategoryStruct.comp (x I.snd) (P.map I.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 { unop := X }) (e₂ : E P.obj { unop := 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 (fun (i : I) => X i) f J.sieves S) {E : A} {x : E P.obj { unop := S }} {y : E P.obj { unop := 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 (fun (i : I) => X i) f J.sieves S) {E : A} (x : (i : I) → E P.obj { unop := 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 { unop := 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 (fun (i : I) => X i) f J.sieves S) {E : A} (x : (i : I) → E P.obj { unop := 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 { unop := 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 (fun (i : I) => X i) f J.sieves S) {E : A} (x : (i : I) → E P.obj { unop := 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 { unop := 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 (fun (i : I) => X i) f J.sieves S) {E : A} (x : (i : I) → E P.obj { unop := 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 {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
                  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

                  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 { unop := 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

                                    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.

                                    Equations
                                    Instances For

                                      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.

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