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

• 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.
• 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₁} [] {A : Type u₂} [] (P : ) :

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

Instances For
@[simp]
theorem CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily_apply_coe {C : Type u₁} [] {A : Type u₂} [] (P : ) {X : C} (S : ) (E : Aᵒᵖ) (π : ().obj E) (Y : C) (f : Y X) (h : S.arrows f) :
↑() Y f h = π.app (Opposite.op { obj := , property := h })
@[simp]
theorem CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily_symm_apply_app {C : Type u₁} [] {A : Type u₂} [] (P : ) {X : C} (S : ) (E : Aᵒᵖ) (x : ) (f : (CategoryTheory.FullSubcategory fun f => S.arrows f.hom)ᵒᵖ) :
( x).app f = x ((CategoryTheory.Presieve.diagram S.arrows).obj f.unop) f.unop.obj.hom (_ : S.arrows f.unop.obj.hom)
def CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily {C : Type u₁} [] {A : Type u₂} [] (P : ) {X : C} (S : ) (E : Aᵒᵖ) :
().obj E

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

Instances For
def CategoryTheory.Presieve.FamilyOfElements.SieveCompatible.cone {C : Type u₁} [] {A : Type u₂} [] {P : } {X : C} {S : } {E : Aᵒᵖ} {x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp P (CategoryTheory.coyoneda.obj E)) S.arrows} :

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

Instances For
def CategoryTheory.Presheaf.homEquivAmalgamation {C : Type u₁} [] {A : Type u₂} [] {P : } {X : C} {S : } {E : Aᵒᵖ} {x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp P (CategoryTheory.coyoneda.obj E)) S.arrows} :
()

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.

Instances For
theorem CategoryTheory.Presheaf.isLimit_iff_isSheafFor {C : Type u₁} [] {A : Type u₂} [] (P : ) {X : C} (S : ) :
Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone ())) ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSheafFor (CategoryTheory.Functor.comp P (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₁} [] {A : Type u₂} [] (P : ) {X : C} (S : ) :
(∀ (c : ), Subsingleton (c P.mapCone ())) ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSeparatedFor (CategoryTheory.Functor.comp P (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₁} [] {A : Type u₂} [] (P : ) :
∀ ⦃X : C⦄ (S : ), Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone ()))

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₁} [] {A : Type u₂} [] (P : ) :
(∀ (E : A), CategoryTheory.Presieve.IsSeparated J (CategoryTheory.Functor.comp P (CategoryTheory.coyoneda.obj ()))) ∀ ⦃X : C⦄ (S : ), ∀ (c : ), Subsingleton (c P.mapCone ())

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₁} [] {A : Type u₂} [] (P : ) {X : C} (R : ) :
Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone ())) ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSheafFor (CategoryTheory.Functor.comp P (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₁} [] {A : Type u₂} [] (P : ) (K : ) :
∀ ⦃X : C⦄ (R : ), Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone ()))

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₁} [] {A : Type u₂} [] {E : A} {X : C} {P : } (hP : ) (x : (I : ) → E P.obj (Opposite.op I.Y)) (hx : ∀ (I : ), CategoryTheory.CategoryStruct.comp () (P.map I.g₁.op) = CategoryTheory.CategoryStruct.comp () (P.map I.g₂.op)) :
E P.obj ()

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

Instances For
@[simp]
theorem CategoryTheory.Presheaf.IsSheaf.amalgamate_map_assoc {C : Type u₁} [] {A : Type u₂} [] {E : A} {X : C} {P : } (hP : ) (x : (I : ) → E P.obj (Opposite.op I.Y)) (hx : ∀ (I : ), CategoryTheory.CategoryStruct.comp () (P.map I.g₁.op) = CategoryTheory.CategoryStruct.comp () (P.map I.g₂.op)) {Z : A} (h : P.obj (Opposite.op I.Y) Z) :
@[simp]
theorem CategoryTheory.Presheaf.IsSheaf.amalgamate_map {C : Type u₁} [] {A : Type u₂} [] {E : A} {X : C} {P : } (hP : ) (x : (I : ) → E P.obj (Opposite.op I.Y)) (hx : ∀ (I : ), CategoryTheory.CategoryStruct.comp () (P.map I.g₁.op) = CategoryTheory.CategoryStruct.comp () (P.map I.g₂.op)) :
theorem CategoryTheory.Presheaf.IsSheaf.hom_ext {C : Type u₁} [] {A : Type u₂} [] {E : A} {X : C} {P : } (hP : ) (e₁ : E P.obj ()) (e₂ : E P.obj ()) (h : ∀ (I : ), CategoryTheory.CategoryStruct.comp e₁ (P.map I.f.op) = CategoryTheory.CategoryStruct.comp e₂ (P.map I.f.op)) :
e₁ = e₂
theorem CategoryTheory.Presheaf.isSheaf_of_iso_iff {C : Type u₁} [] {A : Type u₂} [] {P : } {P' : } (e : P P') :
theorem CategoryTheory.Presheaf.isSheaf_of_isTerminal {C : Type u₁} [] {A : Type u₂} [] {X : A} (hX : ) :
structure CategoryTheory.Sheaf {C : Type u₁} [] (A : Type u₂) [] :
Type (max (max (max u₁ u₂) v₁) v₂)
• val :

the underlying presheaf

• cond :

the condition that the presheaf is a sheaf

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

Instances For
theorem CategoryTheory.Sheaf.Hom.ext_iff {C : Type u₁} :
∀ {inst : } {J : } {A : Type u₂} {inst_1 : } {X Y : } (x y : ), x = y x.val = y.val
theorem CategoryTheory.Sheaf.Hom.ext {C : Type u₁} :
∀ {inst : } {J : } {A : Type u₂} {inst_1 : } {X Y : } (x y : ), x.val = y.valx = y
structure CategoryTheory.Sheaf.Hom {C : Type u₁} [] {A : Type u₂} [] (X : ) (Y : ) :
Type (max u₁ v₂)
• val : X.val Y.val

a morphism between the underlying presheaves

Morphisms between sheaves are just morphisms of presheaves.

Instances For
@[simp]
theorem CategoryTheory.Sheaf.instCategorySheaf_comp_val {C : Type u₁} [] {A : Type u₂} [] :
∀ {X Y Z : } (f : X Y) (g : Y Z), ().val = CategoryTheory.CategoryStruct.comp f.val g.val
@[simp]
theorem CategoryTheory.Sheaf.instCategorySheaf_id_val {C : Type u₁} [] {A : Type u₂} [] :
∀ (x : ),
instance CategoryTheory.Sheaf.instCategorySheaf {C : Type u₁} [] {A : Type u₂} [] :
instance CategoryTheory.Sheaf.instInhabitedHom {C : Type u₁} [] {A : Type u₂} [] (X : ) :
theorem CategoryTheory.Sheaf.hom_ext {C : Type u₁} [] {A : Type u₂} [] {X : } {Y : } (x : X Y) (y : X Y) (h : x.val = y.val) :
x = y
@[simp]
theorem CategoryTheory.sheafToPresheaf_map {C : Type u₁} [] (A : Type u₂) [] :
∀ {X Y : } (f : X Y), ().map f = f.val
@[simp]
theorem CategoryTheory.sheafToPresheaf_obj {C : Type u₁} [] (A : Type u₂) [] (self : ) :
().obj self = self.val
def CategoryTheory.sheafToPresheaf {C : Type u₁} [] (A : Type u₂) [] :

The inclusion functor from sheaves to presheaves.

Instances For
theorem CategoryTheory.Sheaf.Hom.mono_of_presheaf_mono {C : Type u₁} [] (A : Type u₂) [] {F : } {G : } (f : F G) [h : CategoryTheory.Mono f.val] :

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₁} [] (A : Type u₂) [] {F : } {G : } (f : F G) [h : CategoryTheory.Epi f.val] :
@[simp]
theorem CategoryTheory.sheafOver_val {C : Type u₁} [] {A : Type u₂} [] (ℱ : ) (E : A) :
().val = CategoryTheory.Functor.comp .val (CategoryTheory.coyoneda.obj ())
def CategoryTheory.sheafOver {C : Type u₁} [] {A : Type u₂} [] (ℱ : ) (E : A) :

The sheaf of sections guaranteed by the sheaf condition.

Instances For
@[simp]
theorem CategoryTheory.sheafEquivSheafOfTypes_inverse_obj_val {C : Type u₁} [] (S : ) :
(().inverse.obj S).val = S.val
@[simp]
theorem CategoryTheory.sheafEquivSheafOfTypes_functor_obj_val {C : Type u₁} [] (S : ) :
(().functor.obj S).val = S.val
@[simp]
theorem CategoryTheory.sheafEquivSheafOfTypes_inverse_map_val {C : Type u₁} [] :
∀ {X Y : } (f : X Y), (().inverse.map f).val = f.val
@[simp]
theorem CategoryTheory.sheafEquivSheafOfTypes_functor_map_val {C : Type u₁} [] :
∀ {X Y : } (f : X Y), (().functor.map f).val = f.val
@[simp]
theorem CategoryTheory.sheafEquivSheafOfTypes_counitIso {C : Type u₁} [] :
().counitIso = CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Functor.mk { obj := fun S => { val := S.val, cond := (_ : ) }, map := fun {X Y} f => { val := f.val } }) (CategoryTheory.Functor.mk { obj := fun S => { val := S.val, cond := (_ : ) }, map := fun {X Y} f => { val := f.val } })).obj X)

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

Instances For
def CategoryTheory.Sheaf.isTerminalOfBotCover {C : Type u₁} [] {A : Type u₂} [] (F : ) (X : C) (H : ) :

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

Instances For
instance CategoryTheory.sheafHomHasZsmul {C : Type u₁} [] {A : Type u₂} [] {P : } {Q : } :
SMul (P Q)
instance CategoryTheory.instSubHomSheafToQuiverToCategoryStructInstCategorySheaf {C : Type u₁} [] {A : Type u₂} [] {P : } {Q : } :
Sub (P Q)
instance CategoryTheory.instNegHomSheafToQuiverToCategoryStructInstCategorySheaf {C : Type u₁} [] {A : Type u₂} [] {P : } {Q : } :
Neg (P Q)
instance CategoryTheory.sheafHomHasNsmul {C : Type u₁} [] {A : Type u₂} [] {P : } {Q : } :
SMul (P Q)
instance CategoryTheory.instZeroHomSheafToQuiverToCategoryStructInstCategorySheaf {C : Type u₁} [] {A : Type u₂} [] {P : } {Q : } :
Zero (P Q)
instance CategoryTheory.instAddHomSheafToQuiverToCategoryStructInstCategorySheaf {C : Type u₁} [] {A : Type u₂} [] {P : } {Q : } :
@[simp]
theorem CategoryTheory.Sheaf.Hom.add_app {C : Type u₁} [] {A : Type u₂} [] {P : } {Q : } (f : P Q) (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₁} [] {A : Type u₂} [] {P : } {Q : } :
def CategoryTheory.Presheaf.isLimitOfIsSheaf {C : Type u₁} [] {A : Type u₂} [] (P : ) {X : C} (hP : ) :

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

Instances For
theorem CategoryTheory.Presheaf.isSheaf_iff_multifork {C : Type u₁} [] {A : Type u₂} [] (P : ) :
theorem CategoryTheory.Presheaf.isSheaf_iff_multiequalizer {C : Type u₁} [] {A : Type u₂} [] (P : ) [] :
def CategoryTheory.Presheaf.firstObj {C : Type u₁} [] {A : Type u₂} [] {U : C} (R : ) (P : ) :
A

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

Instances For
def CategoryTheory.Presheaf.forkMap {C : Type u₁} [] {A : Type u₂} [] {U : C} (R : ) (P : ) :
P.obj ()

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

Instances For
def CategoryTheory.Presheaf.secondObj {C : Type u₁} [] {A : Type u₂} [] {U : C} (R : ) (P : ) :
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.

Instances For
def CategoryTheory.Presheaf.firstMap {C : Type u₁} [] {A : Type u₂} [] {U : C} (R : ) (P : ) :

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

Instances For
def CategoryTheory.Presheaf.secondMap {C : Type u₁} [] {A : Type u₂} [] {U : C} (R : ) (P : ) :

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

Instances For
theorem CategoryTheory.Presheaf.w {C : Type u₁} [] {A : Type u₂} [] {U : C} (R : ) (P : ) :
def CategoryTheory.Presheaf.IsSheaf' {C : Type u₁} [] {A : Type u₂} [] (P : ) :

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

Instances For

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

Instances For
theorem CategoryTheory.Presheaf.isSheaf_iff_isSheaf' {C : Type u₁} [] {A' : Type u₂} [] (P' : ) :

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

theorem CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget {C : Type u₁} [] {A' : Type u₂} [] (P' : ) (s : CategoryTheory.Functor A' (Type (max v₁ u₁))) :

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.