Acyclicity of the singular chains of a contractible space

The singular homology of a contractible space vanishes in positive degrees, and the reduced homology of a path-connected space vanishes in degree zero. For chains with coefficients in a ring, this file states these facts on elements: a cycle of positive degree is a boundary, and a 0-chain of augmentation zero is a boundary. It also states them for the whole complex: the augmented singular chain complex of a contractible space is exact, that is, the augmentation onto the coefficient ring in degree 0 is a quasi-isomorphism (a QuasiIso instance).

Main results

• TauCeti.singularChains_exists_d_eq_of_d_eq_zero: positive-degree cycles of a contractible space are boundaries.
• TauCeti.singularChains_exists_d_eq_of_augment_eq_zero: 0-chains of augmentation zero of a path-connected space are boundaries.
• TauCeti.quasiIso_singularChainsAugmentation: the augmented singular chain complex of a contractible space is exact.

theorem TauCeti.singularChains_exists_d_eq_of_d_eq_zero {k : Type u} [Ring k] (X : TopCat) [ContractibleSpace ↑X] (q : ℕ) (z : ↑(((singularChains k).obj X).X (q + 1))) (hz : (CategoryTheory.ConcreteCategory.hom (((singularChains k).obj X).d (q + 1) q)) z = 0) : ∃ (b : ↑(((singularChains k).obj X).X (q + 2))), (CategoryTheory.ConcreteCategory.hom (((singularChains k).obj X).d (q + 2) (q + 1))) b = z

The positive-degree cycles of the simplicial singular chains of a contractible space are boundaries.

theorem TauCeti.singularChains_exists_d_eq_of_augment_eq_zero {k : Type u} [Ring k] (X : TopCat) [PathConnectedSpace ↑X] (z : ↑(((singularChains k).obj X).X 0)) (hz : (singularAugment k X) z = 0) : ∃ (b : ↑(((singularChains k).obj X).X 1)), (CategoryTheory.ConcreteCategory.hom (((singularChains k).obj X).d 1 0)) b = z

A 0-chain of augmentation zero of the simplicial singular chains of a path-connected space is a boundary.

instance TauCeti.quasiIso_singularChainsAugmentation (k : Type u) [Ring k] (X : TopCat) [ContractibleSpace ↑X] : QuasiIso (singularChainsAugmentation k X)

The augmented singular chain complex of a contractible space is exact: the augmentation is a quasi-isomorphism onto the coefficient ring in degree 0.