Positive Cech exactness for injective abelian sheaves

For an open cover of a topological space, the Cech complex of an injective abelian sheaf is exact in every positive degree.

The proof constructs the chain complex of free abelian sheaves represented by the finite intersections in the Cech nerve. Around a point in one member of the cover, intersecting the whole cover with that member gives an extra degeneracy. The comparison back to the original free Cech chain complex is an isomorphism on that stalk, by stalk-locality of free representable sheaves. Hence the free Cech chain complex is exact stalkwise, and therefore exact as a complex of sheaves.

Applying Hom(-, I) to this exact chain complex is exact when I is injective. The free abelian Yoneda equivalence identifies the resulting cochain complex degreewise, including its differential, with Mathlib's ordinary Cech complex.

theorem TopologicalSpace.Opens.iicHasTerminal' {X : Type u_1} [TopologicalSpace X] (V : Opens X) : CategoryTheory.Limits.HasTerminal ↑(Set.Iic V)

theorem TopologicalSpace.Opens.iicHasLimitPair' {X : Type u_1} [TopologicalSpace X] (V : Opens X) {U W : ↑(Set.Iic V)} : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair U W)

theorem TopologicalSpace.Opens.iicHasBinaryProducts' {X : Type u_1} [TopologicalSpace X] (V : Opens X) : CategoryTheory.Limits.HasBinaryProducts ↑(Set.Iic V)

theorem TopologicalSpace.Opens.iicHasFiniteProducts' {X : Type u_1} [TopologicalSpace X] (V : Opens X) : CategoryTheory.Limits.HasFiniteProducts ↑(Set.Iic V)

theorem CategoryTheory.Sheaf.cechComplex_exactAt_succ_of_injective {X : TopCat} {I : Type u} (U : I → TopologicalSpace.Opens ↑X) (hU : (Opens.grothendieckTopology ↑X).CoversTop U) (A : TopCat.Sheaf AddCommGrpCat X) [Injective A] (n : ℕ) : HomologicalComplex.ExactAt ((cechComplexFunctor U).obj A.obj) (n + 1)

The Cech complex of an injective abelian sheaf on a topological space is exact in every positive degree.

theorem CategoryTheory.Sheaf.cechComplex_exactAt_succ_of_injective' {X : TopCat} {I : Type u} (U : I → TopologicalSpace.Opens ↑X) (A : TopCat.Sheaf AddCommGrpCat X) [Injective A] (n : ℕ) : HomologicalComplex.ExactAt ((cechComplexFunctor U).obj A.obj) (n + 1)

The Cech complex of an injective abelian sheaf is exact in every positive degree for an arbitrary family of opens. At a point outside the union all terms of the stalk complex vanish; inside the union any member containing the point supplies the usual extra degeneracy.