Cohomology on a localized site

Cohomology at an object agrees with cohomology of the restricted sheaf on the localized site when restriction and its left adjoint are exact. On a preorder site, this left adjoint is extension by zero to the ambient site. For the site of open subsets of a space, the comparison identifies cohomology on an open subset with cohomology of the restricted sheaf.

The comparison uses the action of the left adjoint on free abelian representable sheaves and Mathlib's CategoryTheory.Adjunction.extEquiv for exact adjunctions.

Main declarations

• CategoryTheory.GrothendieckTopology.sheafPullbackFreeYonedaIso: extension on the source objects defining cohomology on an object of the site.
• CategoryTheory.GrothendieckTopology.cohomologyPresheafEvaluationIsoFunctorOverH: the comparison, natural in the coefficient sheaf.
• CategoryTheory.Sheaf.cohomologyPresheafObjIsoOverH: Hⁿ(U, F) ≅ Hⁿ(F.over U).

This comparison transports acyclicity of the restricted sheaf to vanishing of cohomology on the corresponding object, for instance from affine acyclicity to local vanishing hypotheses.

noncomputable def CategoryTheory.GrothendieckTopology.sheafPullbackFreeYonedaIso {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (U : C) [HasSheafify J AddCommGrpCat] [HasSheafify (J.over U) AddCommGrpCat] [(J.overPullback AddCommGrpCat U).IsRightAdjoint] (V : Over U) : ((Over.forget U).sheafPullback AddCommGrpCat (J.over U) J).obj ((TauCeti.CategoryTheory.freeYonedaSheafFunctor (J.over U)).obj V) ≅ (TauCeti.CategoryTheory.freeYonedaSheafFunctor J).obj V.left

Extension to the ambient site sends the free abelian sheaf on V : Over U to the free abelian sheaf on V.left.

Equations

• J.sheafPullbackFreeYonedaIso U V = (CategoryTheory.GrothendieckTopology.extendedSectionsCorepresentation✝ J U V).uniqueUpToIso (TauCeti.CategoryTheory.freeYonedaSheafCorepresentableBy J V.left)

theorem CategoryTheory.GrothendieckTopology.instIsLeftAdjointSheafOverOverAddCommGrpCatSheafPullbackForget_tauCeti {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (U : C) [(J.overPullback AddCommGrpCat U).IsRightAdjoint] : ((Over.forget U).sheafPullback AddCommGrpCat (J.over U) J).IsLeftAdjoint

theorem CategoryTheory.GrothendieckTopology.instAdditiveSheafAddCommGrpCatOverOverOverPullback_tauCeti {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (U : C) : (J.overPullback AddCommGrpCat U).Additive

theorem CategoryTheory.GrothendieckTopology.instAdditiveSheafOverOverAddCommGrpCatSheafPullbackForget_tauCeti {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (U : C) [HasSheafify J AddCommGrpCat] [HasSheafify (J.over U) AddCommGrpCat] [(J.overPullback AddCommGrpCat U).IsRightAdjoint] [Limits.PreservesFiniteLimits ((Over.forget U).sheafPullback AddCommGrpCat (J.over U) J)] : ((Over.forget U).sheafPullback AddCommGrpCat (J.over U) J).Additive

noncomputable def CategoryTheory.GrothendieckTopology.cohomologyPresheafEvaluationIsoFunctorOverH {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (U : C) [HasSheafify J AddCommGrpCat] [HasSheafify (J.over U) AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] [HasExt (Sheaf (J.over U) AddCommGrpCat)] [(J.overPullback AddCommGrpCat U).IsRightAdjoint] [Limits.PreservesFiniteColimits (J.overPullback AddCommGrpCat U)] [Limits.PreservesFiniteLimits ((Over.forget U).sheafPullback AddCommGrpCat (J.over U) J)] (n : ℕ) : (Sheaf.cohomologyPresheafFunctor J n).comp ((evaluation Cᵒᵖ AddCommGrpCat).obj (Opposite.op U)) ≅ (J.overPullback AddCommGrpCat U).comp (Sheaf.functorH (J.over U) n)

Under an exact restriction adjunction, cohomology at U agrees with the cohomology of the restricted sheaf, naturally in the coefficient sheaf.

Equations

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

noncomputable def CategoryTheory.Sheaf.cohomologyPresheafObjIsoOverH {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) (n : ℕ) (U : C) [HasSheafify (J.over U) AddCommGrpCat] [HasExt (Sheaf (J.over U) AddCommGrpCat)] [(J.overPullback AddCommGrpCat U).IsRightAdjoint] [Limits.PreservesFiniteColimits (J.overPullback AddCommGrpCat U)] [Limits.PreservesFiniteLimits ((Over.forget U).sheafPullback AddCommGrpCat (J.over U) J)] : F.H' n U ≅ ↧((F.over U).H n)

Under an exact restriction adjunction, cohomology at an object is the cohomology of the restricted sheaf on the localized site.

Equations

• F.cohomologyPresheafObjIsoOverH n U = (J.cohomologyPresheafEvaluationIsoFunctorOverH U n).app F