Vanishing H¹ makes global sections surjective #
For a short exact sequence of abelian sheaves whose first term has vanishing degree-one cohomology, global sections of the second term surject onto global sections of the third.
Why this is stated here rather than in the geometry #
Sheaf.H F n is Ext (constantSheaf ℤ) F n, so this is the covariant Ext
long exact sequence read at n = 0 and nothing else. Nothing about schemes,
affines, or quasi-coherence enters, and the geometric consumer supplies only the
vanishing hypothesis. Keeping the generic statement generic is what lets the
affine-vanishing calculation and the quasi-coherence argument stay in separate
files.
Main results #
Degree-zero cohomology is surjective when H¹ of the sub vanishes.
The tail of the covariant Ext long exact sequence,
H F₂ 0 → H F₃ 0 → H F₁ 1,
read with the last term subsingleton. Ext.covariant_sequence_exact₃ is the
exactness; the connecting composite is forced to zero because there is nowhere
for it to land.
Global sections are surjective when H¹ of the sub vanishes.
H.equiv₀ identifies degree-zero cohomology with evaluation at a terminal
object, and H.equiv₀_naturality says that identification is natural, so
surjectivity transports across it.