faceMap_apply
plain-language theorem explainer
The i-th topological face map from the standard 1-simplex into the standard 2-simplex acts on points exactly by the affine map induced by the simplicial coface δ_i. Coordinate lemmas for singular faces cite this as the simp unfolding of that map. The proof is pure definitional equality (rfl).
Claim. For every index $i \in \{0,1,2\}$ and every point $x$ of the standard $1$-simplex $\Delta^1$, the continuous face map $\mathrm{face}_i:\Delta^1\to\Delta^2$ equals the affine map of standard simplices induced by the $i$-th coface $\delta_i:[1]\to[2]$ in the simplex category: $\mathrm{face}_i(x)=\Delta(\delta_i)(x)$.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex $F$, the alternating face sum of displacements vanishes. That identity is the chain-level half of the split injection $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$.
The face maps themselves are the continuous maps $\Delta^1\to\Delta^2$ induced by the cofaces $\delta_i:[1]\to[2]$. In code they are packaged as continuous maps of standard simplices whose underlying function is stdSimplex.map of the concrete coface. Singular faces of a $2$-simplex are then composition with these maps.
Coordinate identities on each face (which barycentric coordinates vanish or are preserved) are needed later for cone parameters such as $x_1/(1-x_2)$ in the telescoping homotopy inside the convex $2$-simplex.
proof idea
One-line definitional proof. The face map is defined as the continuous map whose underlying function is already stdSimplex.map of the concrete coface homomorphism, so applying it to a point is definitionally that map; rfl closes the goal. Marked @[simp] so later coordinate lemmas can rewrite the face map away in one step.
why it matters
This is the simp bridge from the packaged face map to the concrete affine action on barycentric coordinates. Every face-coordinate identity in the module rewrites with it first: the six theorems that pin coordinates $0,1,2$ on faces $\delta_0,\delta_1,\delta_2$, and the edge-path lemmas that build the boundary walk $v_0\to v_1\to v_2$.
Those coordinate facts feed the cone parameter and the rel-endpoint homotopy inside $\Delta^2$ used in simplexDisplacement_boundary, the kills-boundaries identity. Together with the fundamental-loop normalization, that identity supplies the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation (surjectivity) half still needs a simplicial prism or subdivision operator not yet in Mathlib singular homology; this lemma sits entirely on the already-proved side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.