homologyMap_augH
plain-language theorem explainer
For any continuous map f : X → Y of topological spaces, the degree-0 singular homology map induced by f, postcomposed with the universal augmentation of Y, recovers the universal augmentation of X. Algebraic topologists cite this when relating H₀-augmentations under continuous maps. The proof unfolds the augmentation and rewrites via the chain-level identity sChainMap_augTo.
Claim. Let $f : X \to Y$ be a continuous map of topological spaces. Then $\mathrm{H}_0(f)$ followed by the degree-$0$ universal augmentation of $Y$ equals the degree-$0$ universal augmentation of $X$: $\mathrm{H}_0(f) \circ \varepsilon_Y = \varepsilon_X$, where $\varepsilon_Z : H_0(Z) \to \mathbb{Z}$ is the augmentation against the whole space.
background
The module develops singular homology of topological spaces in the Recognition foundation layer, with emphasis on degree-0 augmentations and Mayer–Vietoris pairs on spheres and related spaces.
The singular chain map $sChainMap(f)$ is the chain-complex morphism induced by a continuous map $f$, obtained by applying the singular-chain-complex functor. The degree-0 homology augmentation $augH(X,A,hA)$ against a clopen set $A \subseteq X$ is the composite of the homology map of the chain-level augmentation $augTo$ with the identification of $H_0$ of a single complex with $\mathbb{Z}$.
Upstream, $sChainMap_augTo$ records that $sChainMap(f)$ intertwines the chain-level universal augmentations: $sChainMap(f) \circ augTo_Y = augTo_X$ on the whole space. The present lemma is the homology-level shadow of that identity.
proof idea
One short tactic proof. Unfold $augH$ on both sides, so each side is a composite of a degree-0 homology map with the $H_0\simeq\mathbb{Z}$ iso. Reassociate, apply naturality of homology maps under composition ($homologyMap_comp$), and discharge the resulting chain-level equality by $sChainMap_augTo$.
why it matters
Feeds $mono_mvPair_zero$, which asserts that the Mayer–Vietoris pair map is monic in degree 0 whenever $U \cap V$ is path-connected, by splitting its first component against the augmentation. That mono is part of the singular-homology toolkit used to control $H_0$ of sphere and prism constructions in the foundation layer.
In the broader Recognition chain this sits under the topological scaffolding that supports the eight-tick octave and $D=3$ forcing (T7–T8): degree-0 connectivity and augmentation exactness are the algebraic input to those geometric uniqueness arguments. The lemma itself is pure algebraic topology; it closes no open RS physics claim, but it is a proved building block for the mono used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.