Local cohomology sheaves #

Let F be a sheaf of abelian groups on a topological space X and let S be a closed subset. The groups Γ_S(W, F) of sections supported in S form a subsheaf Γ_S(F) of F (CategoryTheory.Sheaf.supportedSectionsSheaf), and Γ_S(F) is flasque when F is: a section over U supported in S glues with zero on V ∖ S and then extends from U ∪ (V ∖ S) to V.

The local cohomology sheaf 𝓗_Sⁿ(F) is the sheafification of the presheaf W ↦ H_Sⁿ(W, F) of cohomology with supports in S (CategoryTheory.Sheaf.supportedHSheaf). In degree zero that presheaf is already the sheaf Γ_S(F), so 𝓗_S⁰(F) ≅ Γ_S(F). The sheaves 𝓗_Sⁿ(F) are supported in S: their stalks vanish off S, because H_Sⁿ(W, F) = 0 for every open W disjoint from S. For a flasque sheaf F they vanish in positive degrees, since then H_Sⁿ⁺¹(W, F) = 0 for every W. More generally, 𝓗_Sⁿ(F) = 0 exactly when, for every open W, every class in H_Sⁿ(W, F) vanishes locally on W (TopCat.Presheaf.isZero_presheafToSheaf_obj_iff).

The sheaves 𝓗_Sⁿ(F) are the coefficients of the local-to-global comparison for cohomology with supports in S; for a closed submanifold M of codimension n in a manifold X, the sheaf 𝓗_Mⁿ(ℤ_X) is the relative orientation sheaf of M in X.

The sheaves Γ_S(F) form the left exact supported-section functor Γ_S (CategoryTheory.Sheaf.supportedSectionsFunctor). For a short exact sequence 0 ⟶ F₁ ⟶ F₂ ⟶ F₃ ⟶ 0 with 𝓗_S¹(F₁) = 0, the sequence 0 ⟶ Γ_S(F₁) ⟶ Γ_S(F₂) ⟶ Γ_S(F₃) ⟶ 0 is short exact: a section of F₃ supported in S defines a class in H_S¹(W, F₁) which vanishes locally, so the section lifts locally. The main result is support truncation: if 𝓗_S^q(F) = 0 for all q < n, then H_S^q(W, F) = 0 for all q < n and every open W. It is proved by dimension shifting along an embedding F ⟶ I into an injective sheaf, for the more general statement where Γ_S(F) is only assumed flasque and 𝓗_S^q(F) = 0 for 0 < q < n: the quotient I / F again has Γ_S(I / F) flasque, as a quotient of the flasque sheaf Γ_S(I) by Γ_S(F), and the connecting maps H_S^q(W, I / F) ⟶ H_S^{q+1}(W, F) are bijective for q > 0. This is the form in which purity of local cohomology, the vanishing of 𝓗_S^q(F) below the codimension, gives the vanishing of the global groups H_S^q(W, F).

The edge comparison is the next step of the same argument. If 𝓗_S^q(F) = 0 for all q < n, then the presheaf W ↦ H_Sⁿ(W, F) is already a sheaf, so the sheafification map identifies H_Sⁿ(W, F) with the sections of 𝓗_Sⁿ(F) over W. In degree one, for Γ_S(F) flasque, the connecting maps identify H_S¹(-, F) with the cokernel sheaf of Γ_S(I) ⟶ Γ_S(I / F), whose sections are computed objectwise because Γ_S(F) and Γ_S(I) are flasque; in higher degrees the connecting maps form an isomorphism of presheaves H_Sⁿ(-, I / F) ≅ H_Sⁿ⁺¹(-, F). Together with the long exact sequence of supports and support truncation this gives the degenerate edge comparison H_Zⁿ(W, F) ≃+ Γ_Z(W, 𝓗_Sⁿ(F)) for closed Z ≤ S, compatible with restriction: the j = 0 case of H_Z^{n+j}(W, F) ≃ H_Z^j(W, 𝓗_Sⁿ(F)), which holds when 𝓗_S^q(F) = 0 for all q ≠ n. For a real-analytic manifold M of dimension n in a complexification, where purity gives 𝓗_M^q(𝓞) = 0 for q ≠ n, this identifies the sections of 𝓗_Mⁿ(𝓞) over W with H_Mⁿ(W, 𝓞).

The degenerate edge comparison holds in every degree: if 𝓗_S^q(F) = 0 for all q ≠ n, then H_Z^{n+j}(-, F) ≅ H_Z^j(-, 𝓗_Sⁿ(F)) as presheaves, for every closed Z ≤ S and every j. For n = 0 the inclusion Γ_S(F) ⟶ F induces the bijections H_Z^j(W, Γ_S(F)) ⟶ H_Z^j(W, F), by dimension shifting along F ⟶ I: as 𝓗_S¹(F) = 0, the sequence 0 ⟶ Γ_S(F) ⟶ Γ_S(I) ⟶ Γ_S(I / F) ⟶ 0 is short exact and the inclusions form a morphism of short exact sequences into 0 ⟶ F ⟶ I ⟶ I / F ⟶ 0 whose middle terms are both flasque. For n = 1, with Γ_S(F) flasque, the image of Γ_S(I) ⟶ Γ_S(I / F) is flasque and its cokernel is 𝓗_S¹(F), so in positive degrees H_Z^{j+2}(W, F) ≅ H_Z^{j+1}(W, I / F) ≅ H_Z^{j+1}(W, Γ_S(I / F)) ≅ H_Z^{j+1}(W, 𝓗_S¹(F)), the middle step being the case n = 0 for I / F. For n ≥ 2 the connecting maps identify H_Z^{n+j}(-, F) with H_Z^{n-1+j}(-, I / F) and 𝓗_Sⁿ(F) with 𝓗_S^{n-1}(I / F), and I / F again satisfies the hypotheses with n - 1. This is the form in which purity and the vanishing of H_Z^{n+1}(W, 𝓞) give H_Z¹(W, 𝓗_Mⁿ(𝓞)) = 0, the flabbiness of the sheaf of hyperfunctions.

Main declarations #

CategoryTheory.Sheaf.supportedSectionsSheaf F S: the sheaf Γ_S(F) of sections supported in S, which is flasque when F is;
CategoryTheory.Sheaf.supportedSectionsι F S: the inclusion Γ_S(F) ⟶ F, a monomorphism;
CategoryTheory.Sheaf.supportedSectionsLift: the factorization through Γ_S(F) of a morphism into F whose sections are supported in S;
CategoryTheory.Sheaf.supportedHSheaf F S n: the local cohomology sheaf 𝓗_Sⁿ(F);
CategoryTheory.Sheaf.supportedHSheafZeroIso: 𝓗_S⁰(F) ≅ Γ_S(F);
CategoryTheory.Sheaf.isZero_stalk_supportedHSheaf_of_notMem: the stalks of 𝓗_Sⁿ(F) at points outside S vanish;
CategoryTheory.Sheaf.isZero_supportedHSheaf_succ_of_isFlasque: 𝓗_Sⁿ⁺¹(F) = 0 for a flasque sheaf F.
CategoryTheory.Sheaf.supportedSectionsFunctor S: the supported-section functor Γ_S, which is left exact (CategoryTheory.Sheaf.exact_map_supportedSectionsFunctor) and through which H_S⁰(W, F) ≃+ Γ_S(W, F) is natural in F (CategoryTheory.Sheaf.supportedHZeroEquiv_naturality_right);
CategoryTheory.Sheaf.shortExact_map_supportedSectionsFunctor: Γ_S preserves a short exact sequence 0 ⟶ F₁ ⟶ F₂ ⟶ F₃ ⟶ 0 with 𝓗_S¹(F₁) = 0;
CategoryTheory.Sheaf.subsingleton_supportedH_of_isZero_supportedHSheaf: support truncation.
CategoryTheory.Sheaf.isSheaf_supportedHPresheaf_of_isZero_supportedHSheaf: if 𝓗_S^q(F) = 0 for q < n, the presheaf W ↦ H_Sⁿ(W, F) is a sheaf;
CategoryTheory.Sheaf.supportedHSectionsEquiv: under the same hypothesis, H_Sⁿ(W, F) ≃+ 𝓗_Sⁿ(F)(W), given by the sheafification map;
CategoryTheory.Sheaf.supportedHEdgeEquiv: the degenerate edge comparison H_Zⁿ(W, F) ≃+ Γ_Z(W, 𝓗_Sⁿ(F)) for closed Z ≤ S;
CategoryTheory.Sheaf.bijective_postcomp_mk₀_supportedSectionsι: if 𝓗_S^q(F) = 0 for q > 0, the inclusion Γ_S(F) ⟶ F induces bijections H_Z^j(W, Γ_S(F)) ⟶ H_Z^j(W, F);
CategoryTheory.Sheaf.supportedHPresheafEdgeIso: the degenerate edge comparison in every degree, H_Z^{n+j}(-, F) ≅ H_Z^j(-, 𝓗_Sⁿ(F)) when 𝓗_S^q(F) = 0 for all q ≠ n.

References #

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