sChainMap_augTo
plain-language theorem explainer
Naturality of the degree-zero augmentation: for a continuous map f : X → Y, the singular chain map C_*(f) followed by the augmentation of Y equals the augmentation of X. Anyone identifying H_0 via total coefficient sum cites this. The proof is a short generator chase on the coproduct presentation of C_0, using that every 0-simplex lands in the universal clopen.
Claim. Let $f : X \to Y$ be a continuous map of topological spaces. Writing $C_*(-)$ for the singular chain complex with $\mathbb{Z}$ coefficients and $\varepsilon_Z : C_*(Z) \to \mathbb{Z}[0]$ for the augmentation that sums coefficients of $0$-simplices (relative to the universal clopen $\mathrm{univ}$), one has $C_*(f) \circ \varepsilon_Y = \varepsilon_X$ as morphisms of homological complexes.
background
The ambient module builds singular homology of spheres from the coproduct presentation of singular chains developed in SingularPrism. In degree $n$, the chain group $C_n(X)$ is the coproduct, over all singular $n$-simplices of $X$, of copies of $\mathbb{Z}$. The generator attached to a simplex $a$ is the corresponding coproduct inclusion.
A continuous map $f : X \to Y$ induces a chain map by postcomposition on simplices. Upstream, gen_map records the generator-level fact: the image of the generator of $a$ is the generator of $f \circ a$. The augmentation in degree zero sends each $0$-simplex generator to $1 \in \mathbb{Z}$ when the simplex lands in a fixed clopen; here the clopen is always $\mathrm{univ}$, so every generator augments to $1$. The complex-level augmentation is the unique map into the single complex $\mathbb{Z}[0]$ with that degree-zero component.
The local goal is naturality of that augmentation under continuous maps, as a morphism of homological complexes.
proof idea
Reduce to a single degree by HomologicalComplex.to_single_hom_ext. After unfolding the composite, it remains to check equality of the two degree-zero maps $C_0(X) \to \mathbb{Z}$. Both sides are determined by their values on coproduct summands, so apply Sigma.hom_ext and fix a $0$-simplex $s$ of $X$. Reassociate, replace the left leg by gen_map (the chain map sends the generator of $s$ to the generator of $f\circ s$), then apply the generator-level augmentation formula on both sides. Each simplex meets $\mathrm{univ}$, so both conditionals fire and both composites equal the identity on $\mathbb{Z}$.
why it matters
The sole downstream consumer is homologyMap_augH, which lifts this chain-level square to homology: the induced map on $H_0$ intertwines the two augmentations $H_0(X) \to \mathbb{Z}$ and $H_0(Y) \to \mathbb{Z}$. That naturality is the bridge from abstract singular $H_0$ to the coefficient-sum isomorphism used when spaces are path-connected (or when working relative to $\mathrm{univ}$).
In the Recognition foundation stack this sits under SingularSphere, which computes singular homology of spheres after the prism, pair, subdivision, and Mayer–Vietoris layers. Sphere homology feeds topological invariants that the forcing chain later ties to the eight-tick octave (T7) and $D=3$ (T8). The lemma itself is pure algebraic topology bookkeeping; its value is that it closes the naturality step without sorry so the $H_0$ comparison can be cited cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.