Sheaf cohomology at a terminal object #
Mathlib carries two accounts of the cohomology of an abelian sheaf F on a site (C, J):
CategoryTheory.Sheaf.H F n, theExt-groups from the constant sheafℤ, which is the cohomology of the site as a whole;CategoryTheory.Sheaf.H' F n X, theExt-groups from the sheafification of the free abelian presheaf onyoneda.obj X, which is the cohomology of the objectX.
They agree when X is a terminal object, and this file supplies that comparison. The abstract
Mayer-Vietoris sequence of Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris is stated
in terms of Sheaf.H', so the comparison is what lets a covering of the whole site compute
Sheaf.H.
Main declarations #
CategoryTheory.Sheaf.cohomologyPresheafEvaluationIsoFunctorH: the comparison as a natural isomorphism in the coefficient sheaf;CategoryTheory.Sheaf.cohomologyPresheafObjIsoH: its specializationHⁿ(T, F) ≅ Hⁿ(F)at a terminal objectT, as an isomorphism of abelian groups.
noncomputable def
CategoryTheory.Sheaf.cohomologyPresheafEvaluationIsoFunctorH
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
[HasSheafify J AddCommGrpCat]
[HasExt (Sheaf J AddCommGrpCat)]
(n : ℕ)
{T : C}
(hT : Limits.IsTerminal T)
:
(cohomologyPresheafFunctor J n).comp ((evaluation Cᵒᵖ AddCommGrpCat).obj (Opposite.op T)) ≅ functorH J n
At a terminal object T, the cohomology presheaf evaluated at T is the cohomology of the
site, naturally in the coefficient sheaf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Sheaf.cohomologyPresheafObjIsoH
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
[HasSheafify J AddCommGrpCat]
[HasExt (Sheaf J AddCommGrpCat)]
(F : Sheaf J AddCommGrpCat)
(n : ℕ)
{T : C}
(hT : Limits.IsTerminal T)
:
At a terminal object, the cohomology of the object is the cohomology of the site.