genRetract
plain-language theorem explainer
Degree-n retraction on singular chains: each simplex of X in the image of a continuous map f : A → X is sent to a chosen preimage generator in A, and all other generators go to zero. Cited by anyone splitting the induced chain map of an inclusion or proving that injective continuous maps induce injective chain maps. Built as a Sigma.desc out of the coproduct of ℤ-summands with a classical existence check.
Claim. For a continuous map $f : A \to X$ and $n \in \mathbb{N}$, define a $\mathbb{Z}$-linear map $r_n : C_n(X;\mathbb{Z}) \to C_n(A;\mathbb{Z})$ on the singular chain groups by its values on generators: if a singular $n$-simplex $\sigma$ of $X$ lies in the image of the singular-set map induced by $f$, send $\sigma$ to (a choice of) a preimage generator in $C_n(A)$; otherwise send $\sigma$ to $0$. When $f$ is injective this $r_n$ splits the induced chain map $f_\#$.
background
Singular chains here are packaged as in SingularPrism. The index set $\mathrm{Idx}(X,n)$ is the set of singular $n$-simplices of a space $X$ (the value of the singular simplicial set at $[n]$). The degree-$n$ chain group $C_n(X;\mathbb{Z})$ is the coproduct $\coprod_{\sigma \in \mathrm{Idx}(X,n)} \mathbb{Z}$ in $\mathbf{Mod}_{\mathbb{Z}}$, and each simplex $a$ contributes a generator via the coproduct inclusion.
SingularPair develops the relative theory for a continuous map $f : A \to X$: the induced chain map on generators pushes simplices of $A$ forward along $f$, and the pair short exact sequence needs a splitting when $f$ is injective (classically, a subspace inclusion). The present definition supplies that candidate retraction on each degree.
Upstream abbreviations fix the notation: $\mathrm{Cgrp},X,n$ is the coproduct chain group, and $\mathrm{gen},X,n,a$ is the inclusion of the $\mathbb{Z}$ summand at simplex $a$.
proof idea
Pure definitional construction, not a proved identity. The map out of the coproduct $C_n(X)$ is specified by Sigma.desc: on the summand indexed by a simplex $x$ of $X$, check whether there exists a simplex $a$ of $A$ with $f_#(a)=x$. If so, take the generator inclusion of a classical choice of such $a$; if not, take the zero map $\mathbb{Z}\to C_n(A)$. No lemmas are invoked in the body; noncomputability comes only from Exists.choose.
why it matters
This is the splitting data for induced singular chain maps of injective continuous maps. Immediately downstream, the generator-level identity (retract after pushforward recovers the original generator) and its lift to $f_# \circ r_n = \mathrm{id}$ on all of $C_n(A)$ are proved in the same module. SingularMayerVietoris then applies the retraction via congruence to obtain elementwise injectivity of the chain map of an injective continuous map, which feeds the Mayer–Vietoris and pair SES machinery.
In the Recognition foundation layer this is algebraic-topology scaffolding rather than a direct physics claim: it underwrites relative singular homology used by later geometric arguments, not a step of the T0–T8 forcing chain, the RCL, or the constants ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.