Sheaf cohomology

Let C be a category equipped with a Grothendieck topology J. We define the cohomology types Sheaf.H F n of an abelian sheaf F on the site (C, J) for all n : ℕ. These abelian groups are defined as the Ext-groups from the constant abelian sheaf with values ℤ (actually ULift ℤ) to F.

We also define Sheaf.cohomologyPresheaf F n : Cᵒᵖ ⥤ AddCommGrpCat which is the presheaf which sends U to the nth Ext-group from the free abelian sheaf generated by the presheaf of sets yoneda.obj U to F.

TODO

• if U is a terminal object of C, define an isomorphism (F.cohomologyPresheaf n).obj (Opposite.op U) ≃+ Sheaf.H F n.
• if U : C, define an isomorphism (F.cohomologyPresheaf n).obj (Opposite.op U) ≃+ Sheaf.H (F.over U) n.

@[reducible, inline]

abbrev CategoryTheory.Sheaf.H {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (F : Sheaf J AddCommGrpCat) [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (n : ℕ) : Type w'

The cohomology of an abelian sheaf in degree n.

Equations

• F.H n = CategoryTheory.Abelian.Ext ((CategoryTheory.constantSheaf J AddCommGrpCat).obj (AddCommGrpCat.of (ULift.{?u.69, 0} ℤ))) F n

noncomputable def CategoryTheory.Sheaf.cohomologyPresheafFunctor {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (n : ℕ) : Functor (Sheaf J AddCommGrpCat) (Functor Cᵒᵖ AddCommGrpCat)

The bifunctor which sends an abelian sheaf F and an object U to the nth Ext-group from the free abelian sheaf generated by the presheaf of sets yoneda.obj U to F.

Equations

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Sheaf.cohomologyPresheaf {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) (n : ℕ) : Functor Cᵒᵖ AddCommGrpCat

Given an abelian sheaf F, this is the presheaf which sends U to the nth Ext-group from the free abelian sheaf generated by the presheaf of sets yoneda.obj U to F.

Equations

• F.cohomologyPresheaf n = (CategoryTheory.Sheaf.cohomologyPresheafFunctor J n).obj F

@[reducible, inline]

noncomputable abbrev CategoryTheory.Sheaf.H' {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) (n : ℕ) (X : C) : AddCommGrpCat

Given an abelian sheaf F on (C, J), n : ℕ and X : C, this is the degree-n sheaf cohomology of X with values in F.

Equations

• F.H' n X = (F.cohomologyPresheaf n).obj (Opposite.op X)

instance CategoryTheory.Sheaf.instSubsingletonHHAddNatOfNat {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {n : ℕ} [Injective F] : Subsingleton (F.H (n + 1))

noncomputable def CategoryTheory.Sheaf.H.equiv₀ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {T : C} (hT : Limits.IsTerminal T) : F.H 0 ≃+ ↑(F.obj.obj (Opposite.op T))

The additive equivalence between H F 0 and the evaluation of F at a terminal object

Equations

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

noncomputable def CategoryTheory.Sheaf.H.map {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {F G : Sheaf J AddCommGrpCat} (f : F ⟶ G) (n : ℕ) : F.H n →+ G.H n

Given a morphism of sheaves f : F ⟶ G, H.map f n is the induced additive map on cohomology groups H F n →+ H G n

Equations

• CategoryTheory.Sheaf.H.map f n = (CategoryTheory.Abelian.Ext.mk₀ f).postcomp ((CategoryTheory.constantSheaf J AddCommGrpCat).obj (AddCommGrpCat.of (ULift.{?u.58, 0} ℤ))) ⋯

theorem CategoryTheory.Sheaf.H.addEquiv₀_map {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {F G : Sheaf J AddCommGrpCat} (f : F ⟶ G) (x : F.H 0) : Abelian.Ext.addEquiv₀ ((map f 0) x) = CategoryStruct.comp (Abelian.Ext.addEquiv₀ x) f

theorem CategoryTheory.Sheaf.H.addEquiv₀_map_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {F G : Sheaf J AddCommGrpCat} (f : F ⟶ G) (x : F.H 0) {Z : Sheaf J AddCommGrpCat} (h : G ⟶ Z) : CategoryStruct.comp (Abelian.Ext.addEquiv₀ ((map f 0) x)) h = CategoryStruct.comp (Abelian.Ext.addEquiv₀ x) (CategoryStruct.comp f h)

theorem CategoryTheory.Sheaf.H.equiv₀_naturality {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {T : C} (hT : Limits.IsTerminal T) {F G : Sheaf J AddCommGrpCat} (f : F ⟶ G) (x : F.H 0) : (ConcreteCategory.hom (f.hom.app (Opposite.op T))) ((equiv₀ F hT) x) = (equiv₀ G hT) ((map f 0) x)

H.equiv₀ is natural

theorem CategoryTheory.Sheaf.H.equiv₀_symm_naturality {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {T : C} (hT : Limits.IsTerminal T) {F G : Sheaf J AddCommGrpCat} (f : F ⟶ G) (x : ↑(F.obj.obj (Opposite.op T))) : (map f 0) ((equiv₀ F hT).symm x) = (equiv₀ G hT).symm ((ConcreteCategory.hom (f.hom.app (Opposite.op T))) x)

theorem CategoryTheory.Sheaf.H.map_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {F G : Sheaf J AddCommGrpCat} (f : F ⟶ G) {n : ℕ} (x : F.H n) : (map f n) x = Abelian.Ext.comp x (Abelian.Ext.mk₀ f) ⋯

@[simp]

theorem CategoryTheory.Sheaf.H.map_id_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {F : Sheaf J AddCommGrpCat} {n : ℕ} (x : F.H n) : (map (CategoryStruct.id F) n) x = x

theorem CategoryTheory.Sheaf.H.map_comp_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {F G : Sheaf J AddCommGrpCat} (f : F ⟶ G) {n : ℕ} {G' : Sheaf J AddCommGrpCat} (g : G ⟶ G') (x : F.H n) : (map (CategoryStruct.comp f g) n) x = (map g n) ((map f n) x)

@[simp]

theorem CategoryTheory.Sheaf.H.map_add_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {F G : Sheaf J AddCommGrpCat} {n : ℕ} (f g : F ⟶ G) (x : F.H n) : (map (f + g) n) x = (map f n) x + (map g n) x

noncomputable def CategoryTheory.Sheaf.functorH {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (n : ℕ) : Functor (Sheaf J AddCommGrpCat) AddCommGrpCat

H as a functor.

Equations

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

@[simp]

theorem CategoryTheory.Sheaf.functorH_map {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (n : ℕ) {X✝ Y✝ : Sheaf J AddCommGrpCat} (f : X✝ ⟶ Y✝) : (functorH J n).map f = AddCommGrpCat.ofHom (H.map f n)

@[simp]

theorem CategoryTheory.Sheaf.functorH_obj_coe {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (n : ℕ) (F : Sheaf J AddCommGrpCat) : ↑((functorH J n).obj F) = F.H n

instance CategoryTheory.Sheaf.instAdditiveAddCommGrpCatFunctorH {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (n : ℕ) : (functorH J n).Additive

theorem CategoryTheory.Sheaf.subsingleton_H_of_isZero {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {F : Sheaf J AddCommGrpCat} (h : Limits.IsZero F) (n : ℕ) : Subsingleton (F.H n)

@[deprecated CategoryTheory.Sheaf.functorH (since := "2026-05-05")]

def CategoryTheory.Sheaf.cohomologyFunctor {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (n : ℕ) : Functor (Sheaf J AddCommGrpCat) AddCommGrpCat

Alias of CategoryTheory.Sheaf.functorH.

---

H as a functor.

Equations

• @CategoryTheory.Sheaf.cohomologyFunctor = @CategoryTheory.Sheaf.functorH