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.

• An A-valued presheaf P : Cᵒᵖ ⥤ A is defined to be a sheaf (for the topology J) iff for every E : A, the type-valued presheaves of sets given by sending U : Cᵒᵖ to Hom_{A}(E, P U) are all sheaves of sets, see CategoryTheory.Presheaf.IsSheaf.
• When A = Type, this recovers the basic definition of sheaves of sets, see CategoryTheory.isSheaf_iff_isSheaf_of_type.
• A alternate definition in terms of limits, unconditionally equivalent to the original one: see CategoryTheory.Presheaf.isSheaf_iff_isLimit.
• An alternate definition when C is small, has pullbacks and A has products is given by an equalizer condition CategoryTheory.Presheaf.IsSheaf'. This is equivalent to the earlier definition, shown in CategoryTheory.Presheaf.isSheaf_iff_isSheaf'.
• When A = Type, this is definitionally equal to the equalizer condition for presieves in CategoryTheory.Sites.SheafOfTypes.
• When A has limits and there is a functor s : A ⥤ Type which is faithful, reflects isomorphisms and preserves limits, then P : Cᵒᵖ ⥤ A is a sheaf iff the underlying presheaf of types P ⋙ s : Cᵒᵖ ⥤ Type is a sheaf (CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget). Cf https://stacks.math.columbia.edu/tag/0073, which is a weaker version of this statement (it's only over spaces, not sites) and https://stacks.math.columbia.edu/tag/00YR (a), which additionally assumes filtered colimits.

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.

def CategoryTheory.Presheaf.IsSheaf {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) : Prop

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

• CategoryTheory.Presheaf.IsSheaf J P = ∀ (E : A), CategoryTheory.Presieve.IsSheaf J (P.comp (CategoryTheory.coyoneda.obj (Opposite.op E)))

def CategoryTheory.Presheaf.IsSeparated {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) [CategoryTheory.ConcreteCategory A] : Prop

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.

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.

@[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) (x✝ : C) (f : x✝ ⟶ 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.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

• hx.cone = { pt := Opposite.unop E, π := (CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily P S E).invFun ⟨x, hx⟩ }

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.

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.

theorem CategoryTheory.Presheaf.isSheaf_iff_isLimit {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) : CategoryTheory.Presheaf.IsSheaf J P ↔ ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone S.arrows.cocone.op))

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⦄, ∀ S ∈ J 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.

theorem CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (R : CategoryTheory.Presieve X) : Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.generate R).arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSheafFor (P.comp (CategoryTheory.coyoneda.obj E)) R

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.

theorem CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.HasPullbacks C] (K : CategoryTheory.Pretopology C) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.Pretopology.toGrothendieck C K) P ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.generate R).arrows.cocone.op))

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 }) ⋯

@[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

@[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) : CategoryTheory.CategoryStruct.comp (hP.amalgamate S x hx) (CategoryTheory.CategoryStruct.comp (P.map I.f.op) h) = CategoryTheory.CategoryStruct.comp (x I) h

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₂ : 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 : I → C} (f : (i : I) → X i ⟶ S) (hf : CategoryTheory.Sieve.ofArrows X f ∈ J S) {E : A} {x 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.existsUnique_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 : I → C} (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

@[deprecated CategoryTheory.Presheaf.IsSheaf.existsUnique_amalgamation_ofArrows]

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 : I → C} (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

Alias of CategoryTheory.Presheaf.IsSheaf.existsUnique_amalgamation_ofArrows.

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 : I → C} (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

• hP.amalgamateOfArrows f hf x hx = Exists.choose ⋯

@[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 : I → C} (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

@[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 : I → C} (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) : CategoryTheory.CategoryStruct.comp (hP.amalgamateOfArrows f hf x hx) (CategoryTheory.CategoryStruct.comp (P.map (f i).op) h) = CategoryTheory.CategoryStruct.comp (x i) h

theorem CategoryTheory.Presheaf.isSheaf_of_iso_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {J : CategoryTheory.GrothendieckTopology C} {P P' : CategoryTheory.Functor Cᵒᵖ A} (e : P ≅ P') : CategoryTheory.Presheaf.IsSheaf J P ↔ CategoryTheory.Presheaf.IsSheaf J P'

theorem CategoryTheory.Presheaf.isSheaf_of_isTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (J : CategoryTheory.GrothendieckTopology C) {X : A} (hX : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Presheaf.IsSheaf J ((CategoryTheory.Functor.const Cᵒᵖ).obj X)

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.

• val : CategoryTheory.Functor Cᵒᵖ A

  the underlying presheaf

• cond : CategoryTheory.Presheaf.IsSheaf J self.val

  the condition that the presheaf is a sheaf

structure CategoryTheory.Sheaf.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (X Y : CategoryTheory.Sheaf J A) : Type (max u₁ v₂)

Morphisms between sheaves are just morphisms of presheaves.

• val : X.val ⟶ Y.val

  a morphism between the underlying presheaves

theorem CategoryTheory.Sheaf.Hom.ext {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} A} {X Y : CategoryTheory.Sheaf J A} {x y : X.Hom Y} (val : x.val = y.val) : x = y

instance CategoryTheory.Sheaf.instCategorySheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] : CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (CategoryTheory.Sheaf J A)

Equations

• CategoryTheory.Sheaf.instCategorySheaf = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Sheaf.instCategorySheaf_id_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (x✝ : CategoryTheory.Sheaf J A) : (CategoryTheory.CategoryStruct.id x✝).val = CategoryTheory.CategoryStruct.id x✝.val

@[simp]

theorem CategoryTheory.Sheaf.instCategorySheaf_comp_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {X✝ Y✝ Z✝ : CategoryTheory.Sheaf J A} (f : X✝ ⟶ Y✝) (g : Y✝ ⟶ Z✝) : (CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val

instance CategoryTheory.Sheaf.instInhabitedHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (X : CategoryTheory.Sheaf J A) : Inhabited (X.Hom X)

Equations

• X.instInhabitedHom = { default := CategoryTheory.CategoryStruct.id X }

theorem CategoryTheory.Sheaf.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {X Y : CategoryTheory.Sheaf J A} (x y : X ⟶ Y) (h : x.val = y.val) : x = y

def CategoryTheory.sheafToPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] : CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Functor Cᵒᵖ A)

The inclusion functor from sheaves to presheaves.

Equations

• CategoryTheory.sheafToPresheaf J A = { obj := CategoryTheory.Sheaf.val, map := fun {X Y : CategoryTheory.Sheaf J A} (f : X ⟶ Y) => f.val, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.sheafToPresheaf_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] (self : CategoryTheory.Sheaf J A) : (CategoryTheory.sheafToPresheaf J A).obj self = self.val

@[simp]

theorem CategoryTheory.sheafToPresheaf_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] {X✝ Y✝ : CategoryTheory.Sheaf J A} (f : X✝ ⟶ Y✝) : (CategoryTheory.sheafToPresheaf J A).map f = f.val

@[reducible, inline]

abbrev CategoryTheory.sheafSections {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor (CategoryTheory.Sheaf J A) A)

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

Equations

• CategoryTheory.sheafSections J A = (CategoryTheory.sheafToPresheaf J A).flip

def CategoryTheory.fullyFaithfulSheafToPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] : (CategoryTheory.sheafToPresheaf J A).FullyFaithful

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

Equations

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

@[simp]

theorem CategoryTheory.fullyFaithfulSheafToPresheaf_preimage_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] {X✝ Y✝ : CategoryTheory.Sheaf J A} (f : (CategoryTheory.sheafToPresheaf J A).obj X✝ ⟶ (CategoryTheory.sheafToPresheaf J A).obj Y✝) : ((CategoryTheory.fullyFaithfulSheafToPresheaf J A).preimage f).val = f

@[reducible, inline]

abbrev CategoryTheory.Sheaf.homEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {X Y : CategoryTheory.Sheaf J A} : (X ⟶ Y) ≃ (X.val ⟶ Y.val)

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

Equations

• CategoryTheory.Sheaf.homEquiv = (CategoryTheory.fullyFaithfulSheafToPresheaf J A).homEquiv

instance CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] : (CategoryTheory.sheafToPresheaf J A).Full

instance CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] : (CategoryTheory.sheafToPresheaf J A).Faithful

instance CategoryTheory.instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] : (CategoryTheory.sheafToPresheaf J A).ReflectsIsomorphisms

theorem CategoryTheory.Sheaf.Hom.mono_of_presheaf_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] {F G : CategoryTheory.Sheaf J A} (f : F ⟶ G) [h : CategoryTheory.Mono f.val] : CategoryTheory.Mono f

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

instance CategoryTheory.Sheaf.Hom.epi_of_presheaf_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] {F G : CategoryTheory.Sheaf J A} (f : F ⟶ G) [h : CategoryTheory.Epi f.val] : CategoryTheory.Epi f

theorem CategoryTheory.isSheaf_iff_isSheaf_of_type {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ (Type w)) : CategoryTheory.Presheaf.IsSheaf J P ↔ CategoryTheory.Presieve.IsSheaf J P

def CategoryTheory.sheafOver {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.Sheaf J (Type v₂)

The sheaf of sections guaranteed by the sheaf condition.

Equations

• CategoryTheory.sheafOver ℱ E = { val := ℱ.val.comp (CategoryTheory.coyoneda.obj (Opposite.op E)), cond := ⋯ }

@[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))

theorem CategoryTheory.Presheaf.IsSheaf.isSheafFor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (hP : CategoryTheory.Presheaf.IsSheaf J P) {X : C} (S : CategoryTheory.Sieve X) (hS : S ∈ J X) : CategoryTheory.Presieve.IsSheafFor P S.arrows

theorem CategoryTheory.Presheaf.isSheaf_bot {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.Presheaf.IsSheaf ⊥ P

def CategoryTheory.sheafBotEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] : CategoryTheory.Sheaf ⊥ A ≌ CategoryTheory.Functor Cᵒᵖ A

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.

@[simp]

theorem CategoryTheory.sheafBotEquivalence_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] : (CategoryTheory.sheafBotEquivalence A).counitIso = CategoryTheory.Iso.refl ({ obj := fun (P : CategoryTheory.Functor Cᵒᵖ A) => { val := P, cond := ⋯ }, map := fun {X Y : CategoryTheory.Functor Cᵒᵖ A} (f : X ⟶ Y) => { val := f }, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.sheafToPresheaf ⊥ A))

@[simp]

theorem CategoryTheory.sheafBotEquivalence_inverse_obj_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A) : ((CategoryTheory.sheafBotEquivalence A).inverse.obj P).val = P

@[simp]

theorem CategoryTheory.sheafBotEquivalence_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] : (CategoryTheory.sheafBotEquivalence A).functor = CategoryTheory.sheafToPresheaf ⊥ A

@[simp]

theorem CategoryTheory.sheafBotEquivalence_inverse_map_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ A} (f : X✝ ⟶ Y✝) : ((CategoryTheory.sheafBotEquivalence A).inverse.map f).val = f

@[simp]

theorem CategoryTheory.sheafBotEquivalence_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] : (CategoryTheory.sheafBotEquivalence A).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Sheaf ⊥ A))

instance CategoryTheory.instInhabitedSheafBotGrothendieckTopologyType {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : Inhabited (CategoryTheory.Sheaf ⊥ (Type w))

Equations

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

def CategoryTheory.Sheaf.isTerminalOfBotCover {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (F : CategoryTheory.Sheaf J A) (X : C) (H : ⊥ ∈ J X) : CategoryTheory.Limits.IsTerminal (F.val.obj (Opposite.op X))

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

Equations

• F.isTerminalOfBotCover X H = CategoryTheory.Limits.IsTerminal.ofUnique (F.val.obj (Opposite.op X))

instance CategoryTheory.sheafHomHasZSMul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.Preadditive A] {P Q : CategoryTheory.Sheaf J A} : SMul ℤ (P ⟶ Q)

Equations

• CategoryTheory.sheafHomHasZSMul = { smul := fun (n : ℤ) (f : P ⟶ Q) => { val := { app := fun (U : Cᵒᵖ) => n • f.val.app U, naturality := ⋯ } } }

instance CategoryTheory.instSubHomSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.Preadditive A] {P Q : CategoryTheory.Sheaf J A} : Sub (P ⟶ Q)

Equations

• CategoryTheory.instSubHomSheaf = { sub := fun (f g : P ⟶ Q) => { val := f.val - g.val } }

instance CategoryTheory.instNegHomSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.Preadditive A] {P Q : CategoryTheory.Sheaf J A} : Neg (P ⟶ Q)

Equations

• CategoryTheory.instNegHomSheaf = { neg := fun (f : P ⟶ Q) => { val := -f.val } }

instance CategoryTheory.sheafHomHasNSMul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.Preadditive A] {P Q : CategoryTheory.Sheaf J A} : SMul ℕ (P ⟶ Q)

Equations

• CategoryTheory.sheafHomHasNSMul = { smul := fun (n : ℕ) (f : P ⟶ Q) => { val := { app := fun (U : Cᵒᵖ) => n • f.val.app U, naturality := ⋯ } } }

instance CategoryTheory.instZeroHomSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.Preadditive A] {P Q : CategoryTheory.Sheaf J A} : Zero (P ⟶ Q)

Equations

• CategoryTheory.instZeroHomSheaf = { zero := { val := 0 } }

instance CategoryTheory.instAddHomSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.Preadditive A] {P Q : CategoryTheory.Sheaf J A} : Add (P ⟶ Q)

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 Q : CategoryTheory.Sheaf J A} (f g : P ⟶ Q) (U : Cᵒᵖ) : (f + g).val.app U = f.val.app U + g.val.app U

instance CategoryTheory.Sheaf.Hom.addCommGroup {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.Preadditive A] {P Q : CategoryTheory.Sheaf J A} : AddCommGroup (P ⟶ Q)

Equations

• CategoryTheory.Sheaf.Hom.addCommGroup = Function.Injective.addCommGroup (fun (f : P.Hom Q) => f.val) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance CategoryTheory.instPreadditiveSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.Preadditive A] : CategoryTheory.Preadditive (CategoryTheory.Sheaf J A)

Equations

• CategoryTheory.instPreadditiveSheaf = { homGroup := fun (x x_1 : CategoryTheory.Sheaf J A) => CategoryTheory.Sheaf.Hom.addCommGroup, add_comp := ⋯, comp_add := ⋯ }

def CategoryTheory.Presheaf.isLimitOfIsSheaf {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) {X : C} (S : J.Cover X) (hP : CategoryTheory.Presheaf.IsSheaf J P) : CategoryTheory.Limits.IsLimit (S.multifork P)

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

Equations

• CategoryTheory.Presheaf.isLimitOfIsSheaf J P S hP = { lift := fun (E : CategoryTheory.Limits.Multifork (S.index P)) => hP.amalgamate S (fun (x : S.Arrow) => E.ι x) ⋯, fac := ⋯, uniq := ⋯ }

theorem CategoryTheory.Presheaf.isSheaf_iff_multifork {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) : CategoryTheory.Presheaf.IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), Nonempty (CategoryTheory.Limits.IsLimit (S.multifork P))

def CategoryTheory.Presheaf.IsSheaf.isLimitMultifork {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) {X : C} (S : J.Cover X) : CategoryTheory.Limits.IsLimit (S.multifork P)

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

theorem CategoryTheory.Presheaf.isSheaf_iff_multiequalizer {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) [∀ (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] : CategoryTheory.Presheaf.IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), CategoryTheory.IsIso (S.toMultiequalizer P)

def CategoryTheory.Presheaf.firstObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.HasProducts A] : A

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

• CategoryTheory.Presheaf.firstObj R P = ∏ᶜ fun (f : (V : C) × { f : V ⟶ U // R f }) => P.obj (Opposite.op f.fst)

def CategoryTheory.Presheaf.forkMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.HasProducts A] : P.obj (Opposite.op U) ⟶ CategoryTheory.Presheaf.firstObj R P

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

• CategoryTheory.Presheaf.forkMap R P = CategoryTheory.Limits.Pi.lift fun (f : (V : C) × { f : V ⟶ U // R f }) => P.map (↑f.snd).op

def CategoryTheory.Presheaf.secondObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasPullbacks C] : A

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.

def CategoryTheory.Presheaf.firstMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Presheaf.firstObj R P ⟶ CategoryTheory.Presheaf.secondObj R P

The map pr₀* of https://stacks.math.columbia.edu/tag/00VM.

Equations

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

def CategoryTheory.Presheaf.secondMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Presheaf.firstObj R P ⟶ CategoryTheory.Presheaf.secondObj R P

The map pr₁* of https://stacks.math.columbia.edu/tag/00VM.

Equations

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

theorem CategoryTheory.Presheaf.w {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.forkMap R P) (CategoryTheory.Presheaf.firstMap R P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.forkMap R P) (CategoryTheory.Presheaf.secondMap R P)

def CategoryTheory.Presheaf.IsSheaf' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasPullbacks C] (P : CategoryTheory.Functor Cᵒᵖ A) : Prop

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.

def CategoryTheory.Presheaf.isSheafForIsSheafFor' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasPullbacks C] (P : CategoryTheory.Functor Cᵒᵖ A) (s : CategoryTheory.Functor A (Type (max v₁ u₁))) [∀ (J : Type (max v₁ u₁)), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) s] (U : C) (R : CategoryTheory.Presieve U) : CategoryTheory.Limits.IsLimit (s.mapCone (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Presheaf.forkMap R P) ⋯)) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.forkMap (P.comp s) R) ⋯)

(Implementation). An auxiliary lemma to convert between sheaf conditions.

Equations

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

theorem CategoryTheory.Presheaf.isSheaf_iff_isSheaf' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A' : Type u₂} [CategoryTheory.Category.{max v₁ u₁, u₂} A'] (J : CategoryTheory.GrothendieckTopology C) (P' : CategoryTheory.Functor Cᵒᵖ A') [CategoryTheory.Limits.HasProducts A'] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Presheaf.IsSheaf J P' ↔ CategoryTheory.Presheaf.IsSheaf' J P'

The equalizer definition of a sheaf given by isSheaf' is equivalent to isSheaf.

theorem CategoryTheory.Presheaf.isSheaf_of_isSheaf_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ A) (s : CategoryTheory.Functor A B) [CategoryTheory.Limits.ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s] (h : CategoryTheory.Presheaf.IsSheaf J (P.comp s)) : CategoryTheory.Presheaf.IsSheaf J P

theorem CategoryTheory.Presheaf.isSheaf_comp_of_isSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ A) (s : CategoryTheory.Functor A B) [CategoryTheory.Limits.PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s] (h : CategoryTheory.Presheaf.IsSheaf J P) : CategoryTheory.Presheaf.IsSheaf J (P.comp s)

theorem CategoryTheory.Presheaf.isSheaf_iff_isSheaf_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ A) (s : CategoryTheory.Functor A B) [CategoryTheory.Limits.HasLimitsOfSize.{v₁, max v₁ u₁, v₂, u₂} A] [CategoryTheory.Limits.PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s] [s.ReflectsIsomorphisms] : CategoryTheory.Presheaf.IsSheaf J P ↔ CategoryTheory.Presheaf.IsSheaf J (P.comp s)

theorem CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A' : Type u₂} [CategoryTheory.Category.{max v₁ u₁, u₂} A'] (J : CategoryTheory.GrothendieckTopology C) (P' : CategoryTheory.Functor Cᵒᵖ A') (s : CategoryTheory.Functor A' (Type (max v₁ u₁))) [CategoryTheory.Limits.HasLimits A'] [CategoryTheory.Limits.PreservesLimits s] [s.ReflectsIsomorphisms] : CategoryTheory.Presheaf.IsSheaf J P' ↔ CategoryTheory.Presheaf.IsSheaf J (P'.comp s)

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.