ZsingleH0Iso
plain-language theorem explainer
Canonical isomorphism identifying the degree-0 homology of the chain complex with ℤ concentrated in degree 0 with the module ℤ itself. Cited wherever singular homology needs an augmentation target or a generator for H₀ of a point. The body is a one-line application of Mathlib's single-object homology self-isomorphism for complexes shaped by ℕ downward.
Claim. There is a canonical isomorphism $H_0(\mathbb{Z}[0]) \cong \mathbb{Z}$ in the category of $\mathbb{Z}$-modules, where $\mathbb{Z}[0]$ denotes the chain complex with $\mathbb{Z}$ placed in degree $0$ and zero elsewhere.
background
In this module, singular homology of a topological space is built from the singular chain complex with coefficients in $\mathbb{Z}$-modules. The auxiliary complex Zsingle is the chain complex that is $\mathbb{Z}$ in degree $0$ and zero in every other degree: the standard coefficient object against which one augments $H_0$ and from which one pushes the class of a point.
Degree-0 homology of a space classifies connected components (with integer coefficients). To pair a homology class against a clopen subset, or to insert the class of a basepoint, one needs a fixed identification of $H_0(\mathbb{Z}[0])$ with $\mathbb{Z}$. That identification is exactly this abbreviation.
The ambient setting is the singular-homology toolkit for spheres and related spaces (imports include single complexes, contractibility, and Mayer–Vietoris scaffolding).
proof idea
One-line wrapper. Apply Mathlib's HomologicalComplex.singleObjHomologySelfIso at degree $0$ for the downward complex shape on $\mathbb{N}$. That lemma states that the homology of a complex concentrated in a single degree is canonically isomorphic to the object sitting in that degree; specializing to $\mathbb{Z}$ in degree $0$ yields the claimed iso.
why it matters
This iso is the coefficient bridge used by the two immediate consumers in the same module: the degree-0 homology augmentation against a clopen set (postcomposes the homology map of the augmentation chain map with the forward map of this iso), and the degree-0 homology class of a point (precomposes the homology map of the point inclusion with the inverse of this iso).
Without a fixed $H_0(\mathbb{Z}[0]) \cong \mathbb{Z}$, those maps would land in an abstract homology object rather than in $\mathbb{Z}$, blocking integer-valued pairings and component-counting arguments later in the singular-sphere development. It is pure homological algebra scaffolding inside the Foundation layer; it does not itself invoke Recognition forcing steps T0–T8, but it underwrites the topological side of any later argument that needs $H_0$ of spheres or points.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.