toChain_asimplex_idTuple
plain-language theorem explainer
The standard affine identity n-simplex, transported along the continuous map of a singular simplex s, yields exactly the free generator of s in the singular chain group. Anyone relating affine support geometry to singular subdivision or prism operators cites this identification. The proof is three rewrites: the toChain/asimplex reduction, push of the identity tuple, and the simplex equivalence inverse.
Claim. Let $X$ be a topological space and $s$ a singular $n$-simplex on $X$. Writing $\sigma_s:\Delta^n\to X$ for the continuous map of $s$, and writing $\iota_n$ for the standard affine identity $n$-simplex on $\Delta^n$, one has $\mathrm{toChain}(\sigma_s)(\iota_n)=[s]$, the free generator of $s$ in the singular chain group $C_n(X)$.
background
The module builds singular subdivision and prism operators on the free singular chain groups of a space $X\in\mathbf{Top}$. Generators are indexed by singular simplices $\mathrm{Idx},X,n$; the symbol $\mathrm{gen},X,n,s$ is the corresponding basis element of $C_n(X)$.
On the affine side, $\mathrm{idTuple},n$ is the identity vertex tuple of the standard simplex $\Delta^n$, and $\mathrm{asimplex}$ turns a vertex tuple into an affine singular simplex. The equivalence $\mathrm{simplexEquiv},X,n$ identifies a singular simplex $s$ with its underlying continuous map $\sigma_s:\Delta^n\to X$. The operator $\mathrm{toChain},\sigma$ pushes an affine chain forward along $\sigma$ into the singular chain group of $X$.
Sibling lemmas record that faces and cones of affine simplices commute with this push, so the whole affine support calculus (barycentric subdivision, prisms) can be transferred to singular chains once the identity-tuple case is identified with a generator.
proof idea
One-line tactic proof by three rewrites. First apply the general reduction of $\mathrm{toChain}$ on an affine simplex (so the claim becomes a push of the identity tuple). Then rewrite by the lemma that pushing the identity tuple along $\sigma_s$ recovers $s$ itself. Finally apply $\mathrm{Equiv.symm_apply_apply}$ for $\mathrm{simplexEquiv}$, which cancels the equivalence and leaves the free generator $\mathrm{gen},X,n,s$.
why it matters
This is the base-case bridge between affine identity geometry and singular generators. Downstream, $\mathrm{gen_comp_sdOpIter}$ uses it to say that iterated singular subdivision of a generator equals $\mathrm{toChain}$ of the iterated affine barycentric subdivision of the identity tuple, tying the singular operator to stage-6 affine support geometry. The degree-zero identity $\mathrm{sdOp_zero}$ reduces to exactly this lemma after one subdivision step on $\mathrm{idTuple},0$. The positive-degree chain-homotopy identity $\mathrm{tOp_chain_homotopy_succ}$ ($\partial T+T\partial=\mathrm{id}-S$) likewise expands generators via the same identification.
In the Recognition foundation stack this sits under the singular-homology toolkit that supports prism and subdivision arguments, not under the T0–T8 forcing chain itself. It closes a purely algebraic bookkeeping gap so later operators can be checked on generators alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.