isIso_homologyMap_augTo
plain-language theorem explainer
For any path-connected topological space X, the degree-0 homology map induced by the augmentation chain map is an isomorphism, so H₀(X) ≅ ℤ. Algebraic topologists and anyone building singular-homology foundations in the Recognition stack cite this. The proof reduces to a chain-level iso criterion: surjectivity via constant simplices, injectivity via path-connected boundaries.
Claim. Let $X$ be a path-connected topological space. The map on singular homology in degree $0$ induced by the augmentation chain map $C_\bullet(X) \to \mathbb{Z}[0]$ (augmentation onto the single complex concentrated in degree $0$) is an isomorphism: $H_0(X) \cong \mathbb{Z}$.
background
Singular homology $H_n(X)$ is computed from the chain complex of singular simplices in $X$ with integer coefficients. The augmentation sends a $0$-chain $\sum n_i x_i$ to the total coefficient sum $\sum n_i \in \mathbb{Z}$, and vanishes in positive degrees; it is a chain map into the complex $\mathbb{Z}$ concentrated in degree $0$.
On a path-connected space every pair of points can be joined by a continuous path, so any two $0$-simplices differ by a boundary (the path supplies a $1$-chain). The module therefore records only the total mass of a $0$-cycle, which is exactly what the augmentation reads.
The local setting is the SingularSphere foundation layer: constant simplices, point extraction, the augmentation functor on open sets, and the Mayer–Vietoris toolkit. The key upstream lemma is the chain-level criterion that a degree-$0$ homology map out of a complex with vanishing differential into $\mathbb{Z}[0]$ is an iso once it is surjective on chains and has kernel equal to the image of $d_1$.
proof idea
Path-connectedness gives a basepoint $x_0$. Apply the upstream chain-zero iso criterion isIso_homologyMap_chain_zero.
Surjectivity: for each integer $y$, take $y$ times the constant $0$-simplex at $x_0$. The augmentation of that generator is $y$ (membership in the universe is automatic), and the differential out of degree $1$ on the target vanishes, so the homology class hits $y$.
Injectivity: if a $0$-cycle $z$ maps to zero under augmentation, path-connectedness supplies a $1$-chain $v$ with $d v = z$ (via exists_bnd_of_pathConnected at $x_0$). Thus $z$ is a boundary, so its homology class is zero.
why it matters
This is the computational engine behind isIso_augH_of_pathConnected, which packages the same statement at the level of the named augmentation homology map $H_0(X)\to\mathbb{Z}$ and is obtained by unfolding plus typeclass inference once this iso is in hand.
In the Recognition foundation stack, identifying $H_0$ of path-connected spaces with $\mathbb{Z}$ is the first nontrivial homology computation. It underwrites later sphere and prism arguments (singular subdivision, Mayer–Vietoris) that feed dimensional and connectivity claims in the forcing chain, including the $D=3$ spatial step and the eight-tick octave topology. Without a clean $H_0\cong\mathbb{Z}$ for path-connected carriers, higher singular-homology comparisons cannot normalize coefficients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.