Sheaf cohomology with closed supports #

Let F be a sheaf of abelian groups on a topological space X, let W be an open subset and let S be a closed subset. The sections of F over W supported in S are those whose restriction to W ∖ S vanishes; they form the subgroup Γ_S(W, F) of F(W), and a morphism of sheaves maps supported sections to supported sections.

The cohomology of F on W with supports in S is the relative cohomology H_Sⁿ(W, F) = Hⁿ(W, W ∖ S; F) = Extⁿ(ℤ_{W, W ∖ S}, F) of the inclusion W ∖ S ⟶ W (CategoryTheory.Sheaf.relativeH'), where ℤ_{W, W ∖ S} is the cokernel of the map of free abelian sheaves ℤ_{W ∖ S} ⟶ ℤ_W. In degree zero it is Γ_S(W, F), and the long exact sequence of the pair is the support sequence

⋯ ⟶ H_Sⁿ(W, F) ⟶ Hⁿ(W, F) ⟶ Hⁿ(W ∖ S, F) ⟶ H_Sⁿ⁺¹(W, F) ⟶ ⋯

(CategoryTheory.Sheaf.relativeH'.exact_toH'_cohomologyPresheaf_map, relativeH'.exact_cohomologyPresheaf_map_δ and relativeH'.exact_δ_toH'). Flasque sheaves have no cohomology with supports in positive degrees; this is the acyclicity input for computing cohomology with supports by flasque resolutions.

For closed subsets Z ≤ S, the triple W ∖ S ⟶ W ∖ Z ⟶ W gives the long exact sequence of supports

⋯ ⟶ H_Zⁿ(W, F) ⟶ H_Sⁿ(W, F) ⟶ H_Sⁿ(W ∖ Z, F) ⟶ H_Zⁿ⁺¹(W, F) ⟶ ⋯,

whose first map enlarges the support and whose second map is restriction to W ∖ Z.

For opens W' ≤ W, the inclusion of pairs (W', W' ∖ S) ⟶ (W, W ∖ S) induces restriction maps H_Sⁿ(W, F) ⟶ H_Sⁿ(W', F), which make W ↦ H_Sⁿ(W, F) a presheaf; sheafifying it gives the local cohomology sheaves of F with supports in S (TauCeti.Topology.Sheaves.LocalCohomology.Basic). On an open W disjoint from S the inclusion W ∖ S ⟶ W is an isomorphism, so H_Sⁿ(W, F) = 0. Excision says that cohomology with supports in S only depends on a neighbourhood of S: if S ∩ W ⊆ W', restriction is an isomorphism H_Sⁿ(W, F) ≃+ H_Sⁿ(W', F). The proof shows that the map of relative free sheaves ℤ_{W', W' ∖ S} ⟶ ℤ_{W, W ∖ S} is already an isomorphism, by the Yoneda criterion TauCeti.CategoryTheory.isIso_relativeFreeYonedaSheafMap_iff: a section over W' supported in S glues with zero on W ∖ S to a unique section over W supported in S.

Main declarations #

CategoryTheory.Sheaf.supportedSections F S W: the sections Γ_S(W, F) of F over W supported in S;
CategoryTheory.Sheaf.supportedH F S W n: the cohomology H_Sⁿ(W, F) of F on W with supports in S;
CategoryTheory.Sheaf.supportedHZeroEquiv: H_S⁰(W, F) ≃+ Γ_S(W, F);
CategoryTheory.Sheaf.subsingleton_supportedH_of_le_compl: H_Sⁿ(W, F) = 0 when W is disjoint from S;
CategoryTheory.Sheaf.relativeH'.subsingleton_succ_of_isFlasque: a flasque sheaf has no relative cohomology in positive degrees for an inclusion of opens; in particular it has no cohomology with supports in positive degrees.
CategoryTheory.Sheaf.relativeH'.extClass_postcomp_bijective_of_isFlasque: dimension shifting, the connecting maps Hⁿ⁺¹(V, U; F₃) ⟶ Hⁿ⁺²(V, U; F₁) of a short exact sequence 0 ⟶ F₁ ⟶ F₂ ⟶ F₃ ⟶ 0 with F₂ flasque are bijective;
CategoryTheory.Sheaf.supportedHRestrict: the restriction map H_Sⁿ(W, F) ⟶ H_Sⁿ(W', F) for W' ≤ W, and CategoryTheory.Sheaf.supportedHPresheaf F S n, the presheaf W ↦ H_Sⁿ(W, F);
CategoryTheory.Sheaf.relativeH'.mk₀_g_postcomp_bijective_of_isFlasque: for such a sequence with F₁ flasque, the maps Hⁿ⁺¹(V, U; F₂) ⟶ Hⁿ⁺¹(V, U; F₃) are bijective;
CategoryTheory.Sheaf.supportedHPresheafPostcomp: the morphism of presheaves H_Sᵐ(-, F) ⟶ H_Sᵏ(-, G) given by the Yoneda product with a class in Extⁿ(F, G), an isomorphism when the Yoneda products are bijective on every open (CategoryTheory.Sheaf.isIso_supportedHPresheafPostcomp);
CategoryTheory.Sheaf.supportedHPresheafδ: the connecting morphism H_Sⁿ(-, F₃) ⟶ H_Sⁿ⁺¹(-, F₁) of presheaves attached to a short exact sequence 0 ⟶ F₁ ⟶ F₂ ⟶ F₃ ⟶ 0, an isomorphism in positive degrees when F₂ is flasque (CategoryTheory.Sheaf.isIso_supportedHPresheafδ_succ);
CategoryTheory.Sheaf.existsUnique_mem_supportedSections_map_eq: excision for sections supported in S;
TopologicalSpace.Closeds.isIso_relativeFreeYonedaSheafMap_complInclusion: excision for the relative free sheaves ℤ_{W, W ∖ S};
CategoryTheory.Sheaf.supportedHExcisionEquiv: excision H_Sⁿ(W, F) ≃+ H_Sⁿ(W', F) when S ∩ W ⊆ W';
CategoryTheory.Sheaf.supportedHMap and CategoryTheory.Sheaf.supportedHδ: for Z ≤ S, the map H_Zⁿ(W, F) ⟶ H_Sⁿ(W, F) and the connecting map H_Sⁿ(W ∖ Z, F) ⟶ H_Zⁿ⁺¹(W, F) of the long exact sequence of supports, whose exactness is CategoryTheory.Sheaf.exact_supportedHMap_supportedHRestrict, CategoryTheory.Sheaf.exact_supportedHRestrict_supportedHδ and CategoryTheory.Sheaf.exact_supportedHδ_supportedHMap.

References #

A. Grothendieck, Local cohomology, Lecture Notes in Mathematics 41, §1.
R. Hartshorne, Algebraic Geometry, Exercises III.2.3–2.4.
M. Kashiwara and P. Schapira, Sheaves on Manifolds, §2.3 and §2.6.