noncomputable def ContractibleHomology.singularHomologyIsoOfHomotopyEquiv {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] (e : ContinuousMap.HomotopyEquiv X Y) (n : ℕ) : ((AlgebraicTopology.singularHomologyFunctor AddCommGrpCat n).obj (AddCommGrpCat.of ℤ)).obj (TopCat.of X) ≅ ((AlgebraicTopology.singularHomologyFunctor AddCommGrpCat n).obj (AddCommGrpCat.of ℤ)).obj (TopCat.of Y)

Homotopy invariance of singular homology: a homotopy equivalence $X \simeq Y$ induces an isomorphism $H_n(X; \mathbb{Z}) \cong H_n(Y; \mathbb{Z})$ for every $n$.

noncomputable def ContractibleHomology.singularHomologyZeroIsoZ_of_contractible (X : Type) [TopologicalSpace X] [ContractibleSpace X] : ((AlgebraicTopology.singularHomologyFunctor AddCommGrpCat 0).obj (AddCommGrpCat.of ℤ)).obj (TopCat.of X) ≅ AddCommGrpCat.of ℤ

For a contractible space $X$, the augmentation gives an isomorphism $H_0(X; \mathbb{Z}) \cong \mathbb{Z}$. Used in the proof of Corollary 5.7.

theorem ContractibleHomology.singularHomology_isZero_of_contractible (X : Type) [TopologicalSpace X] [ContractibleSpace X] (n : ℕ) (hn : n ≠ 0) : CategoryTheory.Limits.IsZero (((AlgebraicTopology.singularHomologyFunctor AddCommGrpCat n).obj (AddCommGrpCat.of ℤ)).obj (TopCat.of X))

For a contractible space $X$ and $n \neq 0$, the singular homology $H_n(X; \mathbb{Z})$ vanishes. Combined with singularHomologyZeroIsoZ_of_contractible, this yields Corollary 5.7.

structure ContractibleHomology.SingularHomologyOfContractible (X : Type) [TopologicalSpace X] [ContractibleSpace X] : Type

Packaged data of singular homology for a contractible space: an isomorphism $H_0(X; \mathbb{Z}) \cong \mathbb{Z}$ together with a proof that $H_n(X; \mathbb{Z}) = 0$ for $n \neq 0$.

• isoZero : ((AlgebraicTopology.singularHomologyFunctor AddCommGrpCat 0).obj (AddCommGrpCat.of ℤ)).obj (TopCat.of X) ≅ AddCommGrpCat.of ℤ
• isZero_pos (n : ℕ) : n ≠ 0 → CategoryTheory.Limits.IsZero (((AlgebraicTopology.singularHomologyFunctor AddCommGrpCat n).obj (AddCommGrpCat.of ℤ)).obj (TopCat.of X))

noncomputable def ContractibleHomology.singularHomologyOfContractible (X : Type) [TopologicalSpace X] [ContractibleSpace X] : SingularHomologyOfContractible X

Corollary 5.7. The singular homology of a contractible space $X$ is given by $H_0(X; \mathbb{Z}) \cong \mathbb{Z}$ and $H_n(X; \mathbb{Z}) = 0$ for $n \neq 0$.

noncomputable def ContractibleHomology.augmentationH₀ (Z : Type) [TopologicalSpace Z] : ((AlgebraicTopology.singularHomologyFunctor AddCommGrpCat 0).obj (AddCommGrpCat.of ℤ)).obj (TopCat.of Z) ⟶ AddCommGrpCat.of ℤ

The augmentation map $\varepsilon : H_0(Z; \mathbb{Z}) \to \mathbb{Z}$, defined as the composition of the map induced by $Z \to \mathrm{pt}$ with the canonical identification $H_0(\mathrm{pt}; \mathbb{Z}) \cong \mathbb{Z}$.