simplexToI
plain-language theorem explainer
Packages the standard homeomorphism Δ¹ ≃ₜ I as a continuous map from the geometric 1-simplex to the unit interval. Singular-homology constructions cite it when turning a path into a singular 1-simplex. The body is a one-line ContinuousMap constructor around Mathlib's existing homeomorphism.
Claim. There is a continuous map $\mathrm{simplexToI}:\Delta^1\to I$ equal to the standard homeomorphism $\Delta^1\simeq_t I$ between the geometric $1$-simplex $\Delta^1=\mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,2)$ and the unit interval $I=[0,1]$.
background
In singular homology one needs continuous maps $\Delta^n\to X$ as generators of the chain groups. For $n=1$, the geometric simplex $\Delta^1$ is homeomorphic to the unit interval $I$, so any path $\gamma:I\to X$ becomes a singular $1$-simplex after precomposition with that homeomorphism.
The ambient module builds singular homology of spheres and related spaces (prisms, pairs, subdivisions, Mayer–Vietoris). Mathlib already supplies stdSimplexHomeomorphUnitInterval; this definition only re-exports it as an element of the continuous-map type C(Δ¹,I) used by the rest of the singular-chain API.
Sibling notation in the module includes constant simplices, the vertex v0, and the point-extraction map pointOf, all of which interact with face maps on $\Delta^1$.
proof idea
Definitional one-liner: form the ContinuousMap pair whose underlying function is Mathlib's stdSimplexHomeomorphUnitInterval and whose continuity proof is that homeomorphism's continuity field. No extra lemmas are proved here.
why it matters
Immediate consumer is pathSimplex: given a path $\gamma:x\leadsto y$ in a space $X$, it builds the singular $1$-simplex $(\gamma\circ\mathrm{simplexToI})$ via the simplex equivalence. The face lemma simplexToI_face_v0 records that the two vertices of $\Delta^1$ land at the endpoints $1$ and $0$ of $I$, which is needed to match path endpoints with singular boundaries.
In the Recognition foundation stack this sits under the singular-sphere / prism / Mayer–Vietoris layer that supports topological forcing arguments (contractibility, homology of spheres) rather than the T5–T8 algebraic forcing chain itself. It is pure scaffolding for path-to-chain conversion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.