toChain
plain-language theorem explainer
Linear evaluation of affine m-chains on the standard n-simplex as singular m-chains of X, pushed along a continuous simplex σ : Δⁿ → X. Algebraic topologists cite it to move barycentric subdivision and prism homotopies from affine support geometry onto singular chains. Defined as the Finsupp linear combination of singular generators of the pushed vertex tuples.
Claim. Fix a continuous map $\sigma:\Delta^n\to X$ and a degree $m$. There is a $\mathbb{Z}$-linear map sending each affine $m$-chain $c$ on $\Delta^n$ (a finitely supported integer combination of vertex tuples $\mathrm{Fin}(m+1)\to\Delta^n$) to the morphism $\mathbb{Z}\to C_m(X;\mathbb{Z})$ given by the corresponding combination of singular generators of the simplices $\sigma\circ\mathrm{aff}(w)$.
background
The module works in singular homology with integer coefficients. The singular chain group $C_m(X)$ is the coproduct of a copy of $\mathbb{Z}$ over each continuous simplex $\Delta^m\to X$; its generators are the canonical inclusions of those summands.
Affine chains $\mathrm{AC}(\alpha,m)$ are finitely supported $\mathbb{Z}$-combinations of vertex tuples $\mathrm{Fin}(m+1)\to\alpha$. On the standard simplex $\Delta^n$, each such tuple determines an affine map $\Delta^m\to\Delta^n$. Precomposing a singular $n$-simplex $\sigma$ with that affine map yields a singular $m$-simplex of $X$ (the push of the tuple along $\sigma$).
This evaluation is the bridge between the purely affine barycentric subdivision calculus developed earlier in the module and the singular operators used for Mayer–Vietoris and excision.
proof idea
One-line definition: apply Finsupp.linearCombination over $\mathbb{Z}$ to the family that sends each vertex tuple $w$ to the singular generator of the pushed simplex $\sigma\circ\mathrm{aff}(w)$. No further lemmas are invoked at the definition site; linearity is inherited from the Finsupp combinator.
why it matters
This is the transport map that lets singular subdivision and the prism homotopy act by evaluating affine subdivision data along each generator. Downstream it appears in the small-span closure lemmas for the subdivision operator and the prism operator in SingularMayerVietoris, and in the identities that identify singular subdivision of a generator with evaluation of iterated affine subdivision of the identity tuple.
Those identities are the stage-6 link between affine support geometry and singular chain operators needed for the Mayer–Vietoris argument in the foundation layer. The definition itself carries no Recognition-Science forcing content (T0–T8); it is pure singular-homology scaffolding that those later geometric claims sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.