pushSimplex
plain-language theorem explainer
Given a continuous map σ from the standard n-simplex into a space X and a vertex tuple w in that simplex, form the singular m-simplex obtained by composing σ with the affine map determined by w. Algebraic topologists cite this when transporting barycentric subdivision from affine chains on the model simplex to singular chains on X. The body is a one-line retyping: invert the simplex equivalence after continuous composition with the affine map.
Claim. For a continuous map $\sigma:\Delta^n\to X$ and a vertex tuple $w:\mathrm{Fin}(m+1)\to\Delta^n$, the pushed singular $m$-simplex is the unique element of the index set of degree-$m$ singular simplices of $X$ corresponding (under the standard equivalence with continuous maps $\Delta^m\to X$) to the composite $\sigma\circ A_w$, where $A_w:\Delta^m\to\Delta^n$ is the affine map sending the $i$-th vertex of $\Delta^m$ to $w(i)$.
background
This module builds barycentric subdivision and the small-simplices theorem for singular chains, feeding Mayer–Vietoris. The index type Idx X m is the set of singular $m$-simplices of a topological space $X$ (the generators of the degree-$m$ singular chain group). The retyped equivalence simplexEquiv identifies each such generator with a continuous map $\Delta^m\to X$, avoiding awkward simplex-category normal forms that block rewriting.
The companion map affineMap sends a vertex tuple $v:\mathrm{Fin}(n+1)\to\Delta^m$ to the continuous affine map $\Delta^n\to\Delta^m$ determined by those vertices. Pushing a singular simplex along such a piece is the standard way to evaluate an affine subdivision of the model simplex inside an arbitrary singular simplex on $X$.
proof idea
One-line definitional wrapper. Compose $\sigma$ with affineMap w to get a continuous map $\Delta^m\to X$, then apply the inverse of simplexEquiv X m to land back in Idx X m. No tactics or intermediate lemmas beyond those two building blocks.
why it matters
This is the transport map that turns affine subdivision of the standard simplex into singular subdivision on $X$. Downstream, gen_pushSimplex_comp_sdOp shows that the subdivision operator on a pushed generator equals the chain image of the affine subdivision of the vertex tuple; small_pushSimplex records that smallness (range in $U$ or $V$) is inherited under push; and toChain_one_mem_smallSpan uses that inheritance to place affine evaluations in the small span.
The Stage 7 payoff exists_sdOpIter_small (the small-simplices theorem for an open cover $U\cup V=X$) is stated entirely in terms of ranges of pushed pieces pushSimplex σ u after iterated barycentric subdivision. That theorem is the classical engine for the singular Mayer–Vietoris sequence developed in the sibling module. Within Recognition Science this is pure foundation scaffolding: it equips the chain-level topology used by later forcing and continuum arguments, not a T0–T8 landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.