simplexEdge
plain-language theorem explainer
For each coface index i in {0,1,2}, this builds the geometric edge of the standard 2-simplex Δ² as a continuous path I → Δ² by composing the affine face map δ_i : Δ¹ → Δ² with the unit-interval reparameterization of Δ¹. Anyone working the singular-simplex winding chain or the cone homotopy on S¹ cites it. The body is a one-line continuous composition.
Claim. For each $i \in \{0,1,2\}$, the map $\mathrm{simplexEdge}(i) : I \to \Delta^2$ is the continuous path obtained by sending $t \in I$ first to the standard $1$-simplex via $t \mapsto (1-t,t)$, then through the affine face inclusion $\delta_i : \Delta^1 \hookrightarrow \Delta^2$ induced by the $i$-th coface in the simplex category.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex $F : \Delta^2 \to S^1$, the alternating face sum of displacements vanishes. That identity is the chain-level reason winding descends to a homology invariant and supplies the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
Two upstream maps are composed here. intervalToSimplex reparameterizes the unit interval onto $\Delta^1$ by $t \mapsto (1-t,t)$, the inverse of Mathlib's stdSimplexHomeomorphUnitInterval. faceMap i is the continuous affine map $\Delta^1 \to \Delta^2$ induced by the coface $\delta i : [1] \to [2]$ in the simplex category. Their composite is the geometric edge of $\Delta^2$ selected by that face, written as a path from $I$.
Sibling infrastructure includes OneSimplex, TwoSimplex, path/simplex conversion, and the displacement/winding assignments on singular $1$-simplices that feed the kills-boundaries theorem.
proof idea
Pure definition: continuous composition (faceMap i).comp intervalToSimplex. No tactics, no lemmas beyond the already-constructed continuous maps. The type is $C(I, \mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},3))$.
why it matters
This is the standard geometric edge used throughout the cone and face calculations that prove winding kills boundaries. Downstream facts pin the cone on each edge: on the base edge ($i=2$) the lifted cone angle recovers the original path lift and the cone circle point recovers $\gamma$; on the $\delta_1$ side the cone is constant at the initial value; on the $\delta_0$ side it is constant once lifted endpoints agree (zero-winding). Related lemmas identify the cone base parameter along the base edge with the unit-interval coordinate, and edge01 is built from this map.
In the module narrative, the $2$-simplex telescoping (boundary walk $v_0 \to v_1 \to v_2$ homotopic rel endpoints inside convex $\Delta^2$ to the direct edge $v_0 \to v_2$) is pushed through $F$ and combined with path-displacement additivity and homotopy invariance. Having explicit continuous edge paths $I \to \Delta^2$ is what makes those face restrictions and cone formulas type-check and compute. The generation/surjectivity half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$ remains open pending a simplicial prism/subdivision operator Mathlib does not yet supply; this definition sits entirely on the proved injective side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.