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ᵒᵖ ⥤ AddCommGrp 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.

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

The cohomology of an abelian sheaf in degree n.

Equations

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

noncomputable instance CategoryTheory.Sheaf.instAddCommGroupH {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (F : CategoryTheory.Sheaf J AddCommGrp) [CategoryTheory.HasSheafify J AddCommGrp] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrp)] (n : ℕ) : AddCommGroup (F.H n)

Equations

• F.instAddCommGroupH n = id inferInstance

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

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} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasSheafify J AddCommGrp] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrp)] (F : CategoryTheory.Sheaf J AddCommGrp) (n : ℕ) : CategoryTheory.Functor Cᵒᵖ AddCommGrp

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