face_apply
plain-language theorem explainer
The j-th face operator on the standard real simplex is definitionally the pushforward of barycentric coordinates along the vertex map that skips index j. Algebraic topologists building prism operators or singular chain homotopies cite this as the simp normal form. The proof is pure reflexivity after unfolding the local definition of face.
Claim. For every index $j\in\{0,\ldots,n+1\}$ and every point $x$ of the standard $n$-simplex over $\mathbb{R}$, the $j$-th face of $x$ equals the image of $x$ under the affine map induced by the order-preserving vertex embedding that omits the $j$-th vertex.
background
The ambient module develops the singular prism operator used to prove homotopy invariance of singular homology (Hatcher, Thm 2.10). A standard $n$-simplex is the set of nonnegative barycentric coordinates on $n+1$ vertices summing to 1. The successor-above map on finite ordinals embeds the vertex set of an $n$-simplex into that of an $(n+1)$-simplex by skipping one index; stdSimplex.map pushes coordinates forward along any such vertex map.
Locally, face is the continuous map that realises the geometric $j$-th face of an $(n+1)$-simplex as an $n$-simplex. The surrounding section computes the four classical composites of prism maps with face inclusions (top face, bottom face, cancelling interior faces, and the factoring faces that match $P\partial$). Those identities need a clean normal form for face itself; this lemma supplies it.
Upstream Mathlib infrastructure supplies succAbove, stdSimplex.map, and the unit-interval topology; the Recognition-side prism and face constructions sit on top of that stack.
proof idea
Term-mode proof by rfl. The local definition of face is exactly stdSimplex.map composed with j.succAbove, so the stated equality is definitional and needs no further lemmas or rewriting.
why it matters
Stage 2 of the singular-prism development (face identities) relies on a simp-normal form for face so that the four classical prism-face composites can be computed by rewriting rather than by ad-hoc coordinate chasing. Those composites are the algebraic content of Hatcher's prism argument: top and bottom faces give the two ends of a homotopy, interior faces cancel in $\partial P$, and the remaining faces reproduce $P\partial$.
In the broader Recognition foundation this sits inside the singular-homology toolkit used to talk about continuous recognition maps and winding data; it does not itself touch the T0-T8 forcing chain, the J-cost, or the phi ladder. No downstream consumers are recorded yet, so the lemma is presently a local simp convenience inside the prism module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.