Injective abelian sheaves are flasque

For a topological space, every injective sheaf of abelian groups is flasque. The proof uses the free abelian sheaves represented by opens: a section over an open V is a map from the corresponding free representable, and an inclusion V ⊆ U induces a monomorphism between those representables. Injectivity extends the map from V to U, which is exactly surjectivity of the restriction map.

This is the first input to the injective-row half of the Cech-to-derived comparison. It is kept as a theorem rather than a global instance so that callers opt into the relatively expensive injectivity argument explicitly.

theorem CategoryTheory.Sheaf.isFlasque_of_injective {X : TopCat} (I : TopCat.Sheaf AddCommGrpCat X) [hI : Injective I] : I.IsFlasque

An injective sheaf of abelian groups on a topological space is flasque.