chainMap_unitOf
plain-language theorem explainer
The singular chain map of a continuous map f sends the free generator of an n-simplex s on A to the free generator of the pushed simplex f∘s on B. Anyone tracking generators through Mayer–Vietoris inclusions or compact-support pushforwards cites this. The proof is a short rewrite through composition-on-units and the generator-map identity.
Claim. Let $A,B$ be topological spaces and $f:A\to B$ continuous. For any singular $n$-simplex $s$ on $A$, writing $e_s$ for the canonical generator of the free $\mathbb{Z}$-summand indexed by $s$, the induced chain map satisfies $C_n(f)(e_s)=e_{f\circ s}$.
background
This module builds singular chain complexes over TopCat as free $\mathbb{Z}$-modules on singular simplices, then sets up the Mayer–Vietoris short complex for an open cover. Each index $s\in\mathrm{Idx}(A,n)$ labels a singular $n$-simplex on $A$; the free summand $\mathbb{Z}\cdot e_s$ is generated by a unit element unitOf s.
A continuous map $f:A\to B$ induces a simplicial-set map on singular simplices and thence a degreewise chain map $C_n(f)$. The companion lemma comp_unitOf records that any module map out of a coproduct of $\mathbb{Z}$'s evaluates on a unit by reading the corresponding component at $1\in\mathbb{Z}$ (via ev1). The identity gen_map says the component of $C_n(f)$ along $s$ is exactly the generator map of the image simplex.
Local setting: foundation-layer singular homology infrastructure used to prove Mayer–Vietoris exactness and arc-complement acyclicity, not yet the Recognition forcing chain itself.
proof idea
Rewrite the left-hand side by comp_unitOf, which turns evaluation of the chain map on unitOf s into ev1 of the composite of the coproduct inclusion at $s$ with $C_n(f)$. That composite equals the generator map of the image simplex by gen_map f n s. Apply ev1_apply (evaluation at $1\in\mathbb{Z}$) and finish by rfl. Four-step rewrite; no induction or homology diagram chase.
why it matters
Generator tracking is the bookkeeping step that makes Mayer–Vietoris exactness computable on free bases. Downstream, mv_middle_exact ("the heart of the Mayer–Vietoris exactness: a pair of chains on $U$ and $V$ whose images cancel comes from a chain on $U\cap V$") applies this when lifting cancelled pairs back along the two inclusions. Independently, chainMap_cVal_unitOf in ArcComplementAcyclic is the one-line specialization to the compact-support valuation map on arc complements, feeding acyclicity arguments for complements in the ambient space.
In the broader Recognition stack this sits in Foundation singular homology scaffolding: it does not itself force $\varphi$, the eight-tick octave, or $D=3$, but it is the elementwise identity those geometric exactness lemmas rest on when they move free generators across continuous maps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.