Ext from the unit module sheaf computes sheaf cohomology

For a sheaf of rings R on a site with a terminal object, Ext^n (unit R) M in sheaves of R-modules is identified with the sheaf cohomology H^n of the underlying abelian sheaf of M, provided injective sheaves of modules are acyclic for H. This is the classical statement that cohomology of an 𝒪-module may be computed in 𝒪-modules or in abelian sheaves (Hartshorne III.2.6), routed through extComparisonAddEquiv:

• the comparison morphism is unitFromConstant : ℤ ⟶ toSheaf (unit R), the map from the constant sheaf sending 1 to 1;
• in degree zero the comparison is f ↦ unitFromConstant ≫ toSheaf.map f, which is a bijection because both sides are the sections of M over the terminal object (unitHomEquiv, sectionsEquivOfIsTerminal, and the constant-sheaf adjunction);
• acyclicity of images of injectives is the hypothesis, supplied on a topological space by flasqueness (Topology/Sheaves/ModulesCohomology.lean).

Main results

• SheafOfModules.unitFromConstant, SheafOfModules.bijective_unitFromConstant_comp.
• SheafOfModules.extUnitAddEquivH.

noncomputable def SheafOfModules.unitFromConstant {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : (CategoryTheory.constantSheaf J AddCommGrpCat).obj (AddCommGrpCat.of (ULift.{u, 0} ℤ)) ⟶ (toSheaf R).obj (unit R)

The map from the constant sheaf ℤ to the underlying abelian sheaf of unit R sending 1 to 1.

Equations

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

theorem SheafOfModules.homEquiv_unitFromConstant_comp {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (M : SheafOfModules R) (f : unit R ⟶ M) : ((CategoryTheory.constantSheafAdj J AddCommGrpCat hT).homEquiv (AddCommGrpCat.of (ULift.{u, 0} ℤ)) ((toSheaf R).obj M)) (CategoryTheory.CategoryStruct.comp (unitFromConstant R hT) ((toSheaf R).map f)) = (((CategoryTheory.sheafSections J AddCommGrpCat).obj (Opposite.op T)).obj ((toSheaf R).obj M)).uliftZMultiplesAddEquiv.symm ((CategoryTheory.ConcreteCategory.hom (f.val.app (Opposite.op T))) 1)

Under the constant-sheaf adjunction, unitFromConstant ≫ toSheaf.map f is the section f 1 over the terminal object.

theorem SheafOfModules.bijective_unitFromConstant_comp {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (M : SheafOfModules R) : Function.Bijective fun (f : unit R ⟶ M) => CategoryTheory.CategoryStruct.comp (unitFromConstant R hT) ((toSheaf R).map f)

Degree zero. f ↦ unitFromConstant ≫ toSheaf.map f is a bijection from maps unit R ⟶ M to maps ℤ ⟶ toSheaf M: both are the sections of M over the terminal object.

theorem SheafOfModules.bijective_extComparisonMap_unitFromConstant_zero {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) [hExtM : CategoryTheory.HasExt (SheafOfModules R)] [hExtA : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (M : SheafOfModules R) : Function.Bijective (CategoryTheory.extComparisonMap (unitFromConstant R hT))

The Ext comparison along toSheaf from unitFromConstant is bijective in degree zero.

noncomputable def SheafOfModules.extUnitAddEquivH {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) [hExtM : CategoryTheory.HasExt (SheafOfModules R)] [hExtA : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (hacyclic : ∀ (I : SheafOfModules R) [CategoryTheory.Injective I] (n : ℕ), Subsingleton (((toSheaf R).obj I).H (n + 1))) (M : SheafOfModules R) (n : ℕ) : CategoryTheory.Abelian.Ext (unit R) M n ≃+ ((toSheaf R).obj M).H n

Ext from the unit computes sheaf cohomology. Ext^n (unit R) M ≃+ H^n (toSheaf M) for every n, once injective sheaves of modules are acyclic for H.

Equations

• SheafOfModules.extUnitAddEquivH R hT hacyclic M n = CategoryTheory.extComparisonAddEquiv (SheafOfModules.unitFromConstant R hT) ⋯ hacyclic M n