Closed-immersion cohomology

Cohomological consequences of closed inclusions used in the Grothendieck vanishing proof.

Main results

• PushforwardHIso — pushforward along a closed inclusion preserves sheaf cohomology, as an isomorphism in every degree.
• subsingleton_sheafH_of_closedImmersion_middle — vanishing of Hⁿ of the middle term in the closed-immersion short exact sequence, given vanishing for the kernel and the pullback.

The closed-inclusion stalk, exactness, and adjunction-unit short exact sequence API live in ClosedImmersion.lean. LES-facing Sheaf.H wrappers come from CohomologyAPI.lean, and the flasque infrastructure from FlasqueVanishing.lean.

Closed-immersion cohomology consequences

noncomputable def PushforwardHIso {X : TopCat} (Z : Set ↑X) (hZ : IsClosed Z) (G : TopCat.Sheaf AddCommGrpCat (TopCat.of ↑Z)) (n : ℕ) : AddCommGrpCat.of (CategoryTheory.Sheaf.H G n) ≅ AddCommGrpCat.of (CategoryTheory.Sheaf.H ((TopCat.Sheaf.pushforward AddCommGrpCat (TopCat.closedIncl hZ)).obj G) n)

Pushforward along a closed inclusion preserves sheaf cohomology in every degree, as an isomorphism. The proof is by induction: in degree zero via sections, in degree one via the cokernel model of H¹, and in higher degrees via dimension-shift isomorphisms on both sides combined with the induction hypothesis on the next term of an injective resolution.

Equations

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

theorem subsingleton_sheafH_of_closedImmersion_middle {X : TopCat} (Z : Set ↑X) (hZ : IsClosed Z) (F : TopCat.Sheaf AddCommGrpCat X) (n : ℕ) (h₁ : Subsingleton (CategoryTheory.Sheaf.H (closedImmersionSES Z hZ F).X₁ n)) (h₃ : Subsingleton (CategoryTheory.Sheaf.H ((TopCat.Sheaf.pullback AddCommGrpCat (TopCat.closedIncl hZ)).obj F) n)) : Subsingleton (CategoryTheory.Sheaf.H F n)

Closed-immersion step: if the kernel term of the closed-immersion short exact sequence and the pullback to the closed subset have subsingleton cohomology in degree n, then so does the ambient sheaf.