Ext from the unit module sheaf on a space computes sheaf cohomology #
On a topological space the acyclicity hypothesis of SheafOfModules.extUnitAddEquivH holds
unconditionally: injective sheaves of modules are flasque
(SheafOfModules.isFlasque_toSheaf_of_injective) and flasque sheaves are acyclic
(TopCat.Sheaf.subsingleton_H_of_isFlasque). So Ext^n (unit R) M ≃+ H^n (M) for every
sheaf of R-modules M on a space, Hartshorne III.2.6.
The HasExt instance on abelian sheaves is passed explicitly, as in
Topology/Sheaves/Cech/BasisComparison.lean, and the cohomology is Sheaf.derivedH.
theorem
SheafOfModules.subsingleton_derivedH_toSheaf_of_injective
{X : TopCat}
(R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) RingCat)
[hExt : CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat)]
(I : SheafOfModules R)
[CategoryTheory.Injective I]
(n : ℕ)
:
Subsingleton (CategoryTheory.Sheaf.derivedH hExt ((toSheaf R).obj I) (n + 1))
Injective sheaves of modules on a space are acyclic for Sheaf.H.
noncomputable def
SheafOfModules.extUnitAddEquivDerivedH
{X : TopCat}
(R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) RingCat)
[hExt : CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat)]
[hExtM : CategoryTheory.HasExt (SheafOfModules R)]
(M : SheafOfModules R)
(n : ℕ)
:
Ext from the unit computes sheaf cohomology on a space.
Ext^n (unit R) M ≃+ H^n (toSheaf M) for every sheaf of R-modules M.