SC_eq
plain-language theorem explainer
The singular chain complex of a space X with integer coefficients is definitionally the alternating-face-map complex of the free simplicial ℤ-module on singular simplices of X. Cite it when switching between the Mathlib singular-chain functor and the simplicial-object presentation. The proof is pure reflexivity.
Claim. For every topological space $X$, the singular chain complex $C_*(X;\mathbb{Z})$ equals the chain complex obtained by applying the alternating face-map construction to the simplicial $\mathbb{Z}$-module of singular simplices of $X$.
background
In this module the singular chain complex of a space $X$ (with $\mathbb{Z}$ coefficients) is packaged two ways. One abbreviation is the direct image of $X$ under Mathlib's singular-chain-complex functor valued in $\mathbb{Z}$-modules. The other is the free simplicial $\mathbb{Z}$-module on the singular simplicial set of $X$, obtained by whiskering the constant-sigma functor with $\mathrm{Top}\to\mathrm{sSet}$.
The alternating-face-map complex is the standard passage from a simplicial object in an abelian category to a chain complex: differentials are alternating sums of face maps. Mathlib's singular-chain functor is built so that these two routes agree on the nose.
The surrounding file develops prism operators and face maps on singular chains (siblings such as the prism map and its face restrictions), so a clean identification of the two presentations is needed before those operators can be stated on either side.
proof idea
One-line term proof by rfl. Unfolding the two abbreviations shows they are the same Mathlib construction: the singular-chain functor applied to $X$ is definitionally the alternating-face-map complex of the free simplicial $\mathbb{Z}$-module on the singular simplices of $X$. No lemmas are invoked.
why it matters
Infrastructure lemma inside Foundation.SingularPrism. It locks the singular chain complex to the simplicial-object presentation so later prism and face constructions can be written against either interface without transport. No downstream consumers are recorded yet in the dependency graph; the immediate audience is the prism-operator development in the same module (continuous prism second-coordinate maps, face restrictions, and related simplicial identities).
This is pure algebraic-topology scaffolding for the Recognition foundation layer. It does not touch the forcing chain (T0–T8), the Recognition Composition Law, or any physical constant. Its value is that subsequent singular-homology arguments in the monolith can quote a single named equality rather than re-unfolding functor definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.