face
plain-language theorem explainer
Extracts the i-th edge of a singular 2-simplex on S¹ by precomposing with the standard coface embedding Δ¹ ↪ Δ². Anyone building the alternating face sum for the chain-level winding invariant cites this. The body is pure continuous composition: F ∘ faceMap(i).
Claim. Given a continuous map $F:\Delta^2\to S^1$ and an index $i\in\{0,1,2\}$, the $i$-th face is the singular $1$-simplex $F\circ\delta_i:\Delta^1\to S^1$, where $\delta_i$ is the affine coface map induced by the simplicial coface $\delta^i:[1]\to[2]$.
background
This module lifts path winding on $S^1$ to singular simplices and proves that displacement vanishes on boundaries. A singular $1$-simplex is a continuous map $\Delta^1\to S^1$; a singular $2$-simplex is a continuous map $\Delta^2\to S^1$, with $\Delta^n=\mathrm{stdSimplex},\mathbb{R}(\mathrm{Fin},(n+1))$.
The face maps are the standard affine embeddings $\Delta^1\hookrightarrow\Delta^2$ coming from the simplicial cofaces $\delta^i$. Precomposing a $2$-simplex with the $i$-th face map yields its geometric edge as a $1$-simplex. The module then assigns a real displacement (equal to $2\pi$ times winding) to every $1$-simplex and shows the alternating face sum on any $2$-simplex is zero.
Upstream, faceMap realises those cofaces as continuous maps of standard simplices; the path-level invariants live in CircleWinding.
proof idea
Definitional one-liner: return the continuous composition of the given $2$-simplex with the $i$-th face map. No lemmas, no tactics; the type checker only needs that composition of continuous maps $\Delta^1\to\Delta^2\to S^1$ is a continuous map $\Delta^1\to S^1$.
why it matters
This is the elementary face operator that feeds the boundary walk on a $2$-simplex. The module's central theorem is the kills-boundaries identity: for every singular $2$-simplex $F$, $\mathrm{disp}(\partial_0 F)-\mathrm{disp}(\partial_1 F)+\mathrm{disp}(\partial_2 F)=0$, proved by telescoping the edge path $v_0\to v_1\to v_2$ against the direct edge $v_0\to v_2$ inside the convex (hence simply connected) standard $2$-simplex, then pushing the homotopy through $F$.
Together with the fact that the fundamental loop has winding $1$, that identity supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Surjectivity still needs a prism/subdivision operator Mathlib does not yet provide. Downstream name collisions (crystal face-centering, alpha face-wallpaper counts) are unrelated string matches; the mathematical consumers are the displacement-boundary lemmas in this foundation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.