map_map_eq_map_map
plain-language theorem explainer
When two composite vertex maps on finite types agree pointwise, the induced affine maps of standard simplices agree. Prism-operator lemmas in singular homology cite this to equate face composites without expanding barycentric coordinates. The argument is a two-line rewrite through composition of simplex maps plus functional extensionality on the vertex maps.
Claim. Let $a,b,b',c$ be finite types, and let $f:a\to b$, $g:b\to c$, $f':a\to b'$, $g':b'\to c$ satisfy $g(f(k))=g'(f'(k))$ for every vertex $k\in a$. Then for every point $x$ of the standard simplex on vertex set $a$ over $\mathbb{R}$, the induced simplex maps obey $\mathrm{map}(g)(\mathrm{map}(f)(x))=\mathrm{map}(g')(\mathrm{map}(f')(x))$.
background
The module builds prism operators for singular chains: continuous maps from a standard simplex times the unit interval into a space, used to compare the prism boundary $\partial P$ with $P\partial$. The standard simplex on a finite vertex type $a$ is the set of nonnegative real weights on $a$ summing to one. A function of vertex sets induces an affine map of simplices by pushforward of those weights (Mathlib's stdSimplex.map).
Composition of induced maps is the map induced by composition of vertex functions. Consequently, any two vertex composites that agree pointwise induce the same simplex map. That bookkeeping identity is exactly what the face-commutation proofs for the prism need when several succAbove/predAbove routes land on the same vertices.
proof idea
Rewrite each double application of the induced simplex map via the Mathlib identity that $\mathrm{map}(g)(\mathrm{map}(f)(x))=\mathrm{map}(g\circ f)(x)$. After both sides are written as a single induced map, replace $g\circ f$ by $g'\circ f'$ using functional extensionality on the given pointwise equality of vertex composites. No coordinate expansion is required.
why it matters
Local parent uses are the three prism face lemmas in the same module: adjacent prisms agree on their shared face (the cancelling terms of $\partial P$), and prism maps commute with high and low faces so the $(i,j)$ terms of $\partial P$ match those of $P\partial$. Those identities are the algebraic skeleton of the prism homotopy operator in singular homology.
In the Recognition Foundation layer this is pure chain-level infrastructure, not a forcing step. It does not touch T5 J-uniqueness, the Recognition Composition Law, $\varphi$, the eight-tick octave, or $D=3$. It simply keeps the singular-prism bookkeeping honest so later homology comparisons can cite face cancellation without re-proving simplex-map naturality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.