gen_map
plain-language theorem explainer
The induced singular chain map of a continuous map f sends the free generator of a singular n-simplex σ to the free generator of the postcomposed simplex f∘σ. Algebraic topologists proving Mayer–Vietoris identities, prism chain homotopies, or splitting of inclusions cite this when reducing maps on free chain groups to generators. The argument is a two-line rewrite through the coproduct presentation of the degree-n chain groups.
Claim. Let $X,Y$ be topological spaces, $f:X\to Y$ continuous, $n\in\mathbb{N}$, and $a$ a singular $n$-simplex of $X$. Writing $\iota_X(a):\mathbb{Z}\to C_n(X;\mathbb{Z})$ for the generator attached to $a$, and $C_n(f)$ for the induced chain map on free $\mathbb{Z}$-modules of singular simplices, one has $\iota_X(a)\,;\,C_n(f)=\iota_Y(f_*a)$, where $f_*a$ is the singular simplex obtained by postcomposing $a$ with $f$.
background
Singular chain groups here are presented as coproducts of copies of $\mathbb{Z}$, one per singular simplex. The index type $\mathrm{Idx}(X,n)$ is the set of singular $n$-simplices of $X$, i.e. the $n$-simplices of the singular simplicial set of $X$. The generator map attached to a simplex $a$ is the coproduct inclusion $\Sigma.\iota_a:\mathbb{Z}\hookrightarrow C_n(X;\mathbb{Z})$.
The induced chain map in degree $n$ is the degree-$n$ component of the image of $f$ under the singular chain-complex functor with $\mathbb{Z}$ coefficients; on the coproduct presentation it is the map of coproducts reindexing summands by postcomposition with $f$ and acting as the identity on each $\mathbb{Z}$.
The local setting is the SingularPrism module, which builds prism operators and chain homotopies for singular chains in preparation for homotopy invariance and Mayer–Vietoris arguments.
proof idea
Unfold the induced chain map to its coproduct form $\Sigma.\mathrm{map}'$ that reindexes by the simplicial-set map of $f$ and applies $\mathrm{id}{\mathbb{Z}}$ on each summand. The goal becomes the standard coproduct identity $\iota_a,;,\Sigma.\mathrm{map}'(f*,\mathrm{id})=\iota_{f_*a},;,\mathrm{id}$. Rewrite with $\Sigma.\iota_\mathrm{comp}_\mathrm{map}'$ and cancel the identity by $\mathrm{Category.id_comp}$. No further lemmas are needed.
why it matters
This is the generator-level naturality of singular chains under continuous maps. Downstream it is the workhorse for elementwise chain-map identities in SingularMayerVietoris (e.g. action on units, agreement of the two routes through $U$ and $V$ from the intersection, and the compositions of the small inclusions with the sum inclusion). SingularPair uses it to prove that an injective continuous map splits on chains after composing with the generator retract. Inside SingularPrism it feeds the prism chain-homotopy identities and the theorem that a homotopy equivalence induces an isomorphism on singular homology.
In the Recognition stack this is pure foundation: it underwrites the singular-homology toolkit (prism operators, Mayer–Vietoris, homotopy invariance) rather than a forcing-chain step T0–T8. Without generator naturality, the later chain-level comparisons do not reduce.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.