intervalToSimplex_apply
plain-language theorem explainer
Pointwise evaluation of the continuous map that reparameterizes the unit interval onto the standard 1-simplex equals Mathlib's inverse homeomorphism. Cited whenever one reduces simplex-endpoint or path-reparameterization goals to the homeomorphism API. Proof is pure definitional equality (rfl), marked @[simp].
Claim. For every $t$ in the unit interval $I$, the continuous reparameterization $\mathrm{intervalToSimplex}(t)$ equals $\mathrm{stdSimplexHomeomorphUnitInterval}^{-1}(t)$.
background
The module lifts path-level winding and displacement on $S^1$ to singular simplices, proving that displacement vanishes on boundaries of 2-simplices and thereby yields a homology invariant. The standard 1-simplex $\Delta^1 = \mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},2)$ is homeomorphic to the unit interval $I$ via Mathlib's stdSimplexHomeomorphUnitInterval.
The local definition intervalToSimplex packages the inverse homeomorphism as a continuous map $C(I,\Delta^1)$, sending $t\mapsto(1-t,t)$. That map is the bridge from path language (unit-interval domains) to singular-simplex language used by simplexDisplacement and the kills-boundaries identity.
proof idea
One-line definitional proof: intervalToSimplex is defined as the continuous map whose underlying function is exactly stdSimplexHomeomorphUnitInterval.symm, so evaluation at any $t$ is rfl. The @[simp] attribute makes the unfolding automatic in downstream endpoint lemmas.
why it matters
Feeds the endpoint identities intervalToSimplex_zero and intervalToSimplex_one, which identify the images of $0$ and $1$ with the two vertices of $\Delta^1$. Those facts pin the boundary of a singular 1-simplex so that simplexDisplacement (reparameterize then take path displacement) is well-defined and compatible with face maps.
In the module's larger program this is scaffolding for the chain-level statement that winding kills boundaries, the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not itself touch the Recognition forcing chain (T0–T8) or the J-cost; it is pure topological infrastructure for the circle's first homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.