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;TopCat.Presheaf.isFlasque_compandTopCat.Presheaf.isFlasque_comp_iff: flasqueness is preserved by composing with a functor that preserves epimorphisms, and reflected when the functor also reflects them, such as forgetting a module structure;TopCat.Sheaf.IsFlasque.epi_cokernel_π_appandTopCat.Sheaf.IsFlasque.exact_cokernel_π_app: if0 ⟶ A ⟶ B ⟶ Cis exact withAandBflasque, then taking sections over an openUgives an exact sequenceB(U) ⟶ C(U) ⟶ (coker (B ⟶ C))(U) ⟶ 0.
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₁.
References #
- R. Hartshorne, Algebraic Geometry, III.2.4–2.5.
- The Stacks Project, tag 09SY, Lemma 20.12.3, Flasque sheaves.
An injective object in the category of sheaves of abelian groups is flasque.
A flasque sheaf of abelian groups has vanishing cohomology in every positive degree over every open subset.
A flasque sheaf of abelian groups has vanishing cohomology in every positive degree.
A skyscraper sheaf of abelian groups is flasque.
Composing a flasque presheaf with a functor that preserves epimorphisms gives a flasque presheaf.
A presheaf is flasque exactly when its composite with a functor that preserves and reflects epimorphisms is flasque.
A zero presheaf is flasque: each of its restriction maps lands in a zero object.
If 0 ⟶ A ⟶ B ⟶ C is an exact sequence of sheaves of abelian groups with A and B flasque,
then every section of the cokernel of B ⟶ C lifts to a section of C.
If 0 ⟶ A ⟶ B ⟶ C is an exact sequence of sheaves of abelian groups with A flasque, then a
section of C maps to zero in the cokernel of B ⟶ C exactly when it comes from a section of
B.