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

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

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 })
@[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
@[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
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 functor Sheaf J A ⥤ Cᵒᵖ ⥤ A is fully faithful.

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

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

Equations

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

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

Equations
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

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

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

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

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.

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.

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.