intervalToSimplex
plain-language theorem explainer
Continuous reparameterisation of the unit interval onto the standard 1-simplex by t ↦ (1−t, t). Anyone converting path-level circle data into singular 1-simplices cites it. The definition is Mathlib's standard homeomorphism inverse, packaged as a ContinuousMap.
Claim. There is a continuous map $\iota:I\to\Delta^1$ given by $t\mapsto(1-t,t)$, equal to the inverse of the standard homeomorphism $\Delta^1\cong I$.
background
The module lifts path-level winding and displacement on the circle to singular simplices of $S^1$, then proves that displacement vanishes on boundaries of 2-simplices. That identity is the chain-level fact making winding a homology invariant, and (with the generator evaluation) the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The standard 1-simplex $\Delta^1=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},2)$ is the set of barycentric pairs $(x_0,x_1)$ with $x_i\ge 0$ and $x_0+x_1=1$. Mathlib supplies a homeomorphism from $\Delta^1$ to the unit interval $I$; the map here is its continuous inverse, so endpoints go to the two vertices and the second barycentric coordinate is the interval parameter itself.
proof idea
Definitional one-liner: package Mathlib's stdSimplexHomeomorphUnitInterval.symm as an element of $C(I,\Delta^1)$ by pairing the underlying function with its continuity proof. No local argument is needed beyond the homeomorphism already in Mathlib.
why it matters
This is the bridge from path language to singular-simplex language in the winding chain. Downstream, oneSimplexPath and simplexDisplacement reparameterise a singular edge through this map and then call path displacement; endpoint lemmas pin vertices; cone constructions (base-face restriction, terminal side lifts) compose with it when building 2-simplex telescopes.
Module-level payoff is simplexDisplacement_boundary: alternating face sum of displacement on any singular 2-simplex is zero, via convex homotopy in $\Delta^2$ plus path additivity and homotopy invariance. Together with the once-around generator evaluating to 1, that yields the left-inverse half of the integer comparison on $H_1(S^1)$. Surjectivity still needs a prism/subdivision operator Mathlib singular homology does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.