toChain_asimplex
plain-language theorem explainer
Evaluating the affine-to-singular chain map on an affine generator returns the singular generator of the pushed simplex. Algebraic topologists proving subdivision, boundary, and chain-map intertwining cite this generator rule. The proof is a one-line application of the lift identity for affine generators.
Claim. Let $\sigma:\Delta^n\to X$ be continuous and let $w:\mathrm{Fin}(m+1)\to\Delta^n$ be a vertex tuple. Then the affine-to-singular chain map sends the affine generator of $w$ to the singular chain generator of the pushed simplex $\mathrm{pushSimplex}(\sigma,w)$: $\mathrm{toChain}(\sigma,m)(\mathrm{asimplex}\,w)=\mathrm{gen}_X(m,\mathrm{pushSimplex}(\sigma,w))$.
background
Module Foundation.SingularSubdivision builds the affine chain complex on vertex tuples in a convex set and the comparison map into singular chains of a space $X$. Affine $n$-chains AC α n are finitely supported $\mathbb{Z}$-combinations of maps $\mathrm{Fin}(n+1)\to\alpha$. The generator asimplex w is the Dirac basis element $Finsupp.single,w,1$.
On the singular side, gen X m a (from SingularPrism) is the canonical inclusion of the free summand indexed by a singular $m$-simplex $a$ into the singular chain group. The comparison toChain σ m is the $\mathbb{Z}$-linear map that, on generators, pushes an affine simplex through the fixed continuous map $\sigma:\Delta^n\to X$ via pushSimplex.
Upstream, lift_asimplex records exactly this generator evaluation; affineMap_comp_face controls how faces restrict vertex tuples and is used in sibling face lemmas for pushed simplices.
proof idea
One-line wrapper: the goal is definitionally the statement of lift_asimplex applied to $\sigma$ and the vertex tuple $w$. No further rewriting or case analysis is required.
why it matters
This is the generator evaluation that every intertwining lemma for toChain reduces to via AC.hom_ext. Downstream it is applied in toChain_amap (affine pushforward becomes precomposition of $\sigma$), toChain_asimplex_idTuple (identity tuple recovers the original singular generator), toChain_comp_abnd (affine boundary matches singular boundary), toChain_comp_chainMap (postcomposition with a map of spaces), and toChain_comp_sdOp (affine barycentric subdivision matches the singular subdivision operator).
In the Recognition foundation stack these identities underwrite prism and subdivision arguments that move between combinatorial affine data and singular chains on topological spaces. They sit below the forcing and continuum constructions rather than stating a T0–T8 landmark themselves; they are the algebraic-topology glue those landmarks rely on when chains appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.