chainMap_comp_genRetract
plain-language theorem explainer
For an injective continuous map $f:A\to X$, the induced degree-$n$ singular chain map splits: composing it with the generator retraction recovers the identity on $C_n(A)$. Anyone proving monomorphisms of singular chain complexes or Mayer–Vietoris exactness for pairs cites this split. The proof lifts the generator-level retraction identity through a coproduct extensionality argument.
Claim. Let $f:A\to X$ be an injective continuous map of topological spaces and let $n\in\mathbb{N}$. Write $C_n(-)$ for the degree-$n$ singular chain group (coproduct of $\mathbb{Z}$ over singular $n$-simplices) and $C_n(f)$ for the induced chain map. There is a retraction $r_n:C_n(X)\to C_n(A)$ on generators such that $C_n(f)\circ r_n=\mathrm{id}_{C_n(A)}$.
background
In the singular-prism setup, the degree-$n$ singular chain group $C_n(X)$ is the coproduct $\coprod_{\sigma\in\mathrm{Idx}(X,n)}\mathbb{Z}$ of integer coefficients indexed by singular $n$-simplices of $X$. The chain map $C_n(f)$ is the degree-$n$ component of the singular chain complex functor applied to a continuous map $f:A\to X$.
The generator retraction $r_n=\mathrm{genRetract}(f,n)$ sends a singular simplex of $X$ in the image of $f$ to a chosen preimage generator in $C_n(A)$, and sends everything else to zero. Its defining property on generators (for injective $f$) is the sibling lemma: applying $C_n(f)$ then $r_n$ recovers each generator of $C_n(A)$.
This module builds the relative singular pair $(X,A)$ and the short exact sequence of chain complexes used for Mayer–Vietoris and relative homology. The split identity is the algebraic engine behind degreewise monicity of $C_\bullet(f)$.
proof idea
Extensionality for morphisms out of a coproduct (Sigma.hom_ext) reduces the identity $C_n(f)\circ r_n=\mathrm{id}$ to a check on each generator of $C_n(A)$. After rewriting the identity composite and the action of the chain map on generators (gen_map), the goal is exactly the generator-level retraction lemma gen_comp_genRetract, which holds because $f$ is injective (so the chosen preimage is unique and the dite branch is the generator itself).
why it matters
This split is the direct input to chainMap_mono: monicity of $C_n(f)$ is obtained from the standard fact that a morphism with a left inverse is mono (mono_of_mono_fac). Downstream, SingularMayerVietoris.chainMap_injective reuses the same retraction to get elementwise injectivity of the chain map, feeding the singular Mayer–Vietoris and relative-pair exact sequences.
In the Recognition foundation layer, singular pairs and their SES supply the homological scaffolding around the eight-tick and prism constructions (T7-adjacent topology). The lemma closes the algebraic half of “injective continuous maps induce monomorphisms of singular chains,” with no remaining sorry on this path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.