stdSimplex_map_eq_affineMap
plain-language theorem explainer
The standard-simplex map induced by a vertex reindexing equals the affine map on the corresponding image vertices. Anyone proving face-restriction or subdivision identities for singular simplices will cite this. The argument is a pointwise finite-sum identity: barycentric coordinates filtered by the image index match the Pi.single expansion of the affine combination.
Claim. Let $g:\{0,\ldots,n\}\to\{0,\ldots,m\}$ and let $x$ lie in the standard $n$-simplex over $\mathbb{R}$. Then the pushforward of $x$ under the induced simplex map equals the affine combination of the standard vertices $e_{g(i)}$ with barycentric weights $x_i$.
background
The ambient setting is singular simplices and their affine realizations, as developed in SingularSubdivision with face inclusions from SingularPrism. The standard simplex consists of nonnegative barycentric coordinates on Fin (k+1) summing to one. A vertex map $g$ induces a continuous simplex map by pushing coordinates forward: the $j$-th coordinate of the image is the sum of $x_i$ over $g(i)=j$.
Separately, an affine map on a simplex is the unique continuous map sending each point to the convex combination of a prescribed vertex tuple. The topological face inclusion (from SingularPrism.face) is the special case of the simplex map along Fin.succAbove j, skipping one vertex; that is the geometric realization of the simplicial face operator $\delta_j$.
This lemma identifies the two constructions when the vertex tuple is the standard basis vectors reindexed by $g$.
proof idea
Extend equality of simplex points and compare coordinates at each $j$. The left-hand side is the filtered sum $\sum_{g(i)=j} x_i$ by the finite linear-map evaluation lemma. Rewrite the filter as a full sum of indicators, then match termwise against $\sum_i x_i\cdot(\mathrm{Pi.single}(g(i),1))_j$. Case-split on $g(i)=j$: the matching index contributes $x_i\cdot 1$, the others $x_i\cdot 0$.
why it matters
The sole recorded consumer is affineMap_comp_face, which states that composing a general affine map with a topological face inclusion restricts the vertex tuple along Fin.succAbove. That identity is the algebraic engine for moving affine realizations past face operators in singular subdivision and prism constructions.
In the Recognition foundation stack this sits under the singular-homology scaffolding (imports from Mathlib singular homology and the local prism module). It does not itself touch the forcing chain T0–T8, the J-cost, or the eight-tick octave; it is pure geometric bookkeeping that keeps face and subdivision diagrams commuting when simplices are realized affinely.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.