faceMap
plain-language theorem explainer
The i-th continuous face embedding of the standard 1-simplex into the standard 2-simplex, induced by the simplicial coface δ_i. Cited throughout the singular-simplex winding development whenever a 2-simplex is restricted to a boundary edge. Definition packages the affine stdSimplex map of SimplexCategory.δ i together with its continuity witness.
Claim. For each index $i\in\{0,1,2\}$, there is a continuous map $\mathrm{face}_i:\Delta^1\to\Delta^2$ equal to the affine map of standard simplices induced by the $i$-th coface $\delta_i:[1]\to[2]$ in the simplex category.
background
The ambient module lifts the path-level winding/displacement invariant on $S^1$ to singular simplices and proves the chain identity that makes it a homology invariant: for every singular 2-simplex $F:C(\Delta^2,S^1)$, the alternating face sum of displacements vanishes.
Standard simplices $\Delta^n=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},(n+1))$ carry the usual affine structure. Face operators on singular chains are induced by cofaces $\delta_i:[n-1]\to[n]$ in the simplex category; on geometric realizations these become continuous affine inclusions of $\Delta^{n-1}$ into $\Delta^n$. Here $n=2$, so the domain is $\Delta^1$ and the codomain is $\Delta^2$.
The three faces of a 2-simplex are the edges of the boundary walk $v_0\to v_1\to v_2$ versus the direct edge $v_0\to v_2$. Those restrictions are exactly what the telescoping argument in the module doc needs before pushing a convex homotopy through $F$.
proof idea
Pure definition, not a proof. The body is the continuous-map constructor whose underlying function is stdSimplex.map applied to the concrete morphism of SimplexCategory.δ i, paired with the library continuity lemma for that affine map. No tactics or intermediate lemmas.
why it matters
This is the geometric face operator used by every cone-restriction lemma in the module: base-face and side-face evaluations of cone base parameters, pointwise $S^1$ values of the lifted cone, and the path-parametric identity that the base face of the cone recovers the original 1-simplex of a path.
Those identities feed the 2-simplex telescoping that proves displacement of the alternating boundary is zero (the "winding kills boundaries" statement). Together with the fact that the invariant sends the once-around generator to 1, that vanishing supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module notes that the converse generation half still needs a simplicial prism/subdivision operator not yet in Mathlib singular homology; this definition sits entirely on the proved side of that split.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.