Flasque sheaves are acyclic #

A sheaf of abelian groups on a topological space is flasque when all of its restriction maps are surjective. This file proves that a flasque sheaf has no higher cohomology.

Main declarations #

TauCeti.Topology.isFlasque_of_injective: an injective object in the category of abelian sheaves is flasque;
TauCeti.Topology.subsingleton_H'_succ_of_isFlasque: a flasque sheaf has vanishing cohomology in every positive degree over every open subset;
TauCeti.Topology.subsingleton_H_succ_of_isFlasque: the same statement for the cohomology of the whole space;
TauCeti.Topology.isFlasque_skyscraperSheaf: skyscraper sheaves are flasque, and hence acyclic.

The proof is the classical dimension shift. Embedding a flasque sheaf F in an injective sheaf I gives a short exact sequence 0 ⟶ F ⟶ I ⟶ Q ⟶ 0, and the covariant long exact sequence of Ext presents Hⁿ⁺¹(U, F) as a quotient of Hⁿ(U, Q). In degree zero, the sections of Q over U lift to sections of I because F is flasque, so the quotient vanishes; in higher degrees Q is again flasque, because I is, and induction applies. That I is flasque is the point at which TauCeti/CategoryTheory/Sites/SheafCohomology/FreeYoneda.lean enters: an inclusion of open subsets induces a monomorphism of the free abelian sheaves they generate, and Hom(-, I) turns it into the restriction map of I.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer B, "coherent sheaves and cohomology Hⁱ(X, ℱ): acyclicity of affines, …, vanishing above dimension": it is the first acyclicity theorem of the lane, and the acyclic skyscraper sheaves are the coefficients in which the Riemann-Roch induction over the points of a divisor reads the additivity of TauCeti/AlgebraicGeometry/Cohomology/EulerCharacteristic.lean.

No formalization is vendored: flasqueness, the surjectivity of sections out of a flasque subsheaf, the stability of flasqueness under quotients and the flasqueness of skyscraper sheaves are Mathlib's Mathlib/Topology/Sheaves/Flasque.lean, and the long exact sequence is Mathlib's CategoryTheory.Abelian.Ext.covariant_sequence_exact₁.