face
plain-language theorem explainer
The j-th face inclusion of the standard simplex embeds Δⁿ continuously into Δ^{n+1} by skipping vertex j. Algebraic topologists and anyone building singular chains or prism homotopies cite it as the geometric face map. The definition packages Mathlib's stdSimplex.map along Fin.succAbove with the automatic continuity proof.
Claim. For each index $j \in \{0,\ldots,n+1\}$, there is a continuous map $\iota_j:\Delta^n\to\Delta^{n+1}$ given on vertices by the order-preserving injection that skips $j$ (i.e. the topological realization of the simplicial face operator $\delta_j$).
background
Singular homology and prism operators need the geometric face inclusions of standard simplices. The standard $n$-simplex $\Delta^n\subset\mathbb{R}^{n+1}$ is the set of nonnegative barycentric coordinates summing to 1. Mathlib supplies stdSimplex.map for any map on the vertex index type, together with a continuity lemma.
Here the vertex map is Fin.succAbove j: the unique order-preserving injection $\mathrm{Fin}(n+1)\to\mathrm{Fin}(n+2)$ that omits $j$. The resulting continuous map is exactly the topological face inclusion $\Delta^n\hookrightarrow\Delta^{n+1}$ opposite vertex $j$, i.e. the geometric realization of $\delta_j$ in the simplex category.
The module builds prism and singular-homology infrastructure on top of Mathlib's algebraic topology library; this face map is the basic geometric ingredient reused by face operators on singular simplices and by higher-dimensional prism constructions.
proof idea
One-line definitional wrapper. The continuous-map structure is the pair consisting of stdSimplex.map applied to j.succAbove and the Mathlib lemma stdSimplex.continuous_map that guarantees continuity of any such barycentric pushforward. No further proof work.
why it matters
Face inclusions are the geometric atoms of singular chains, prism homotopies, and any count of cube or simplex faces that later enters Recognition constants. Downstream, AlphaDerivation uses face structure of the 3-cube $Q_3$ to obtain passive edges $=11$ and the solid-angle identity $\mathrm{solid_angle}_{Q_3}=4\pi$ via Gauss–Bonnet on $\partial Q_3$; AlphaHigherOrder counts face–wallpaper pairs (102) and the sign of the curvature correction $\delta_1$; LambdaRecDerivation fixes $Q_3$ vertex/face counts; CrystalSymmetry names face-centered Bravais types. In the forcing chain these geometric face counts feed the $D=3$ and $\alpha$-band derivations rather than being imported as black-box topology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.