stdSimplexHomeomorphUnitInterval_coe
plain-language theorem explainer
For any point of the standard 1-simplex, Mathlib's homeomorphism to the unit interval recovers exactly the second barycentric coordinate as a real. Anyone tracking singular 1-simplices or face parameters on Δ² cites this. The proof is a short term argument: apply the known second-coordinate identity for the inverse map, unfold, simplify, and reverse the equality.
Claim. If $x$ lies in the standard $1$-simplex $\Delta^1=\mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,2)$, then the real number underlying Mathlib's homeomorphism $\Delta^1\xrightarrow{\sim}I$ at $x$ equals the second barycentric coordinate $x_1$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact behind a left inverse $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$. Displacement of a singular $1$-simplex is defined by reparameterising $\Delta^1$ to the unit interval and taking path displacement.
Mathlib supplies stdSimplexHomeomorphUnitInterval : stdSimplex ℝ (Fin 2) ≃ₜ I. The local inverse is the continuous map intervalToSimplex : C(I, stdSimplex ℝ (Fin 2)) sending $t\mapsto(1-t,t)$. Its second barycentric coordinate is tautologically $t$ (intervalToSimplex_coord_one). The present lemma is the dual reading: after the homeomorphism, the unit-interval parameter is again $x_1$.
That coordinate is the affine parameter used when faces of a $2$-simplex are identified with paths on the base edge, which is exactly where the telescoping argument for simplexDisplacement_boundary needs a clean comparison of parameters.
proof idea
Term-mode, four steps. Instantiate intervalToSimplex_coord_one at stdSimplexHomeomorphUnitInterval x. Unfold the definition of intervalToSimplex (the continuous package of the homeomorphism inverse). Simplify; the second coordinate identity becomes an equality between the unit-interval coe of $x$ and $x,1$ after the inverse-forward composition cancels. Take the symmetric form to match the goal.
why it matters
Feeds the face-parameter lemmas twoSimplexCoordOneParam_face_two and twoSimplexCoordOneParam_face_zero, which identify the base-edge parameter of a $2$-simplex after the face maps $\delta_2$ and $\delta_0$ with the unit-interval homeomorphism (resp. its reverse). Those identities are the bookkeeping step in the $2$-simplex telescoping that proves displacement kills boundaries.
In the module's programme that gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ once combined with the fundamental-loop normalisation. The result is pure coordinate algebra on $\Delta^1$; it does not itself touch the Recognition forcing chain (T0–T8), but it is infrastructure for the circle-winding half of the continuum bridge used later in the foundation stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.