chainMap
plain-language theorem explainer
Continuous maps of spaces induce degree-n maps on singular chain groups with integer coefficients, presented as coproducts over singular simplices. Anyone pushing cycles or boundaries along inclusions, retractions, or embeddings in the arc-complement acyclicity development cites this. The body is a thin unpack of Mathlib's singular chain complex functor evaluated in degree n.
Claim. For topological spaces $X,Y$ and a continuous map $f:X\to Y$, and for each degree $n\in\mathbb{N}$, there is an induced $\mathbb{Z}$-linear map $C_n(X)\to C_n(Y)$ on the degree-$n$ singular chain groups (each realized as the coproduct $\coprod_{\sigma} \mathbb{Z}$ over singular $n$-simplices).
background
The ambient module builds singular chains on TopCat with a coproduct presentation suited to generator-wise arguments. The degree-$n$ chain group of a space $X$ is the coproduct $\coprod_{\sigma\in\mathrm{Idx}(X,n)}\mathbb{Z}$ of one copy of $\mathbb{Z}$ per singular $n$-simplex; that is the domain and codomain of the induced map.
Mathlib already supplies the singular chain complex functor from spaces to chain complexes of $\mathbb{Z}$-modules. Evaluating that functor on a continuous map and reading the degree-$n$ component yields the classical pushforward on chains. The local convention is to keep that map typed on the coproduct groups rather than on an opaque Mathlib carrier, so later lemmas can talk about generators, faces, and boundaries elementwise.
Upstream, the only essential dependency is that coproduct chain-group abbreviation; the induced map is then the standard functorial action of singular homology.
proof idea
One-line definitional unpack: apply Mathlib's singularChainComplexFunctor (with coefficients in ModuleCat ℤ) to the continuous map $f$, then take the degree-$n$ component of the resulting chain-complex morphism. No extra algebraic work; the abbrev only retypes that component onto the local coproduct chain groups.
why it matters
This is the workhorse pushforward used throughout the arc-complement acyclicity development (Hatcher 2B.1, arc case). Downstream lemmas commute it with the boundary (chainMap_bnd), show that bounding chains push forward (bounds_map), and pull bounding back along retractions (bounds_of_retract). Those facts feed the elementwise Mayer–Vietoris injectivity step and the bisection argument that every embedded arc in $S^D$ has $H_1$-acyclic complement.
In the Recognition foundation stack, arc-complement acyclicity is topological infrastructure for high-dimensional linking and vanishing statements that support the dimensional forcing side of the program (including the $D=3$ landmark in the T0–T8 chain). The declaration itself is pure classical singular homology; its place in the monorepo is as the typed interface those later vanishing theorems call.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.