affineMap_comp_face
plain-language theorem explainer
Composing the affine map of a vertex tuple with a topological face inclusion equals the affine map of the restricted tuple (one vertex skipped). Used by anyone pushing singular simplices through faces in subdivision or prism constructions. Proof is pointwise ContinuousMap extensionality, reducing via the face-as-affine-map identity and vertex evaluation.
Claim. Let $v:\mathrm{Fin}(n+2)\to\Delta^{d}$ be a tuple of vertices in the standard $d$-simplex and let $j\in\mathrm{Fin}(n+2)$. Then the continuous affine map determined by $v$, composed with the $j$-th face inclusion $\Delta^{n}\hookrightarrow\Delta^{n+1}$, equals the affine map determined by the restricted tuple $v\circ j^{\uparrow}$ (skipping index $j$).
background
The module builds singular subdivision and prism operators on continuous maps out of standard simplices $\Delta^{k}\subset\mathbb{R}^{k+1}$. An affine map here is the unique continuous map $\Delta^{n}\to\Delta^{d}$ sending the standard vertices to a prescribed tuple $v$.
The topological face inclusion (from SingularPrism) is the continuous map $\Delta^{n}\to\Delta^{n+1}$ induced by $\mathrm{Fin}.\mathrm{succAbove},j$, i.e. the geometric realization of the simplicial face $\delta_{j}$. It embeds the $n$-simplex as the face opposite vertex $j$.
Upstream, face is defined as $\langle\mathrm{stdSimplex}.\mathrm{map},j.\mathrm{succAbove},\ldots\rangle$. The companion lemma affineMap_comp says affine maps compose by composing vertex tuples; affineMap_vertex evaluates an affine map at a standard vertex.
proof idea
Pointwise ContinuousMap.ext. After unfolding composition, the left side is affineMap $v$ applied to stdSimplex.map $j.\mathrm{succAbove},x$. Rewrite that map as an affine map via stdSimplex_map_eq_affineMap, then apply affineMap_comp so both sides are affine maps of vertex tuples. The vertex functions agree by affineMap_vertex (funext), hence the maps agree.
why it matters
Needed to move face restrictions through affine pushforwards when building singular chains. Downstream, toChain_asimplex identifies the chain of an affine simplex with the generator of the pushed vertex tuple; face-restriction of pushed simplices is the companion fact that uses this identity. In the Recognition foundation stack this is pure simplicial plumbing supporting singular homology of recognition complexes (prism and subdivision operators), not a physics forcing step (T5–T8). It closes a small algebraic gap so chain-level face identities hold definitionally on generators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.