sChainMap
plain-language theorem explainer
A continuous map of spaces induces a morphism of singular chain complexes with integer coefficients. Algebraic topologists cite it whenever pushforwards of cycles, boundaries, or homology classes are needed. It is a one-line abbreviation: apply Mathlib's singular chain complex functor to the map.
Claim. For topological spaces $X,Y$ and a continuous map $f:X\to Y$, write $SC(X)$ for the singular chain complex of $X$ with $\mathbb{Z}$ coefficients. Then $f$ induces a chain-complex morphism $SC(X)\to SC(Y)$.
background
In this module, $SC(X)$ is the singular chain complex of a space $X\in\mathbf{Top}$ with coefficients in $\mathbb{Z}$-modules: the value of Mathlib's singularChainComplexFunctor at $X$. Degree-$n$ chains are finite formal $\mathbb{Z}$-linear combinations of continuous maps $\Delta^n\to X$.
The companion construction is the prism operator (affine maps $\Delta^{n+1}\to\Delta^n\times I$), used later to turn homotopies of continuous maps into chain homotopies. The present abbreviation is the covariant functoriality half of that package: every arrow $f:X\to Y$ in $\mathbf{Top}$ becomes a chain map $SC(X)\to SC(Y)$.
The local setting is classical singular homology infrastructure, imported from Mathlib's algebraic topology and homotopy libraries, and reused throughout the Foundation layer for Mayer–Vietoris and acyclicity arguments.
proof idea
One-line abbreviation. Evaluate Mathlib's singular chain complex functor (with coefficient object $\mathbb{Z}$ in $\mathbf{Mod}_{\mathbb{Z}}$) on the continuous map $f:X\to Y$. No extra proof obligations: functoriality and chain-map axioms are inherited from the Mathlib construction.
why it matters
This is the standard induced chain map that every later singular-homology argument in the Foundation layer applies. Downstream, ArcComplementAcyclic uses it for elementwise boundary commutation, functoriality, identity, and naturality of homology classes, and for the MV injectivity statement that a 1-cycle of $U\cap V$ whose pushforwards bound in $U$ and $V$ bounds in the intersection (under $H_2(X)=0$). SingularMayerVietoris builds the Mayer–Vietoris pair map $H_n(U\cap V)\to H_n(U)\oplus H_n(V)$ by applying homology of these induced maps on the two inclusions.
In the Recognition Science stack this is pure topological scaffolding: it does not encode J-cost, $\varphi$, or the forcing chain T0–T8, but it underwrites the singular-homology tools used when the framework reasons about covers, complements, and vanishing of low-degree homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.