pathSimplex
plain-language theorem explainer
A continuous path between two points of a space yields a singular 1-simplex in the singular chain complex. Algebraic topologists in the Recognition foundation layer cite it to turn path data into degree-1 generators. The body is a one-line retyping: compose the path map with the standard homeomorphism Δ¹ ≃ I, then apply the inverse simplex equivalence.
Claim. Let $X$ be a topological space and $\gamma$ a path from $x$ to $y$ in $X$. There is an associated singular $1$-simplex $[\gamma]$ in the index set of degree-$1$ singular simplices of $X$, obtained by composing the continuous map of $\gamma$ with the homeomorphism $\Delta^1 \simeq I$ and transporting the result into the singular-simplex type.
background
The SingularSphere module builds singular-homology infrastructure for spheres and related spaces in the Recognition foundation layer. Singular $n$-simplices of a space $X$ are continuous maps from the standard simplex $\Delta^n$ into $X$; the type $\mathrm{Idx}(X,n)$ is their index set and generates the degree-$n$ singular chain group with integer coefficients.
Upstream, the simplex equivalence retypes the standard simplicial-set object equivalence so a singular $m$-simplex is literally a continuous map $\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin}(m+1))\to X$, avoiding definitional noise that blocks rewriting. The map $\mathrm{simplexToI}$ is the homeomorphism $\Delta^1\simeq_t I$ packaged as a continuous map. A Mathlib path already supplies a continuous map $I\to X$ with fixed endpoints $x$ and $y$.
Together these pieces convert ordinary path data into the language of singular chains used throughout the module.
proof idea
One-line definition, not a tactic proof. Start from the continuous map of the given path $\gamma:I\to X$. Compose on the right with $\mathrm{simplexToI}:\Delta^1\to I$ to obtain a continuous map $\Delta^1\to X$. Apply the inverse of the degree-$1$ simplex equivalence to land in $\mathrm{Idx}(X,1)$. No further lemmas are invoked in the body.
why it matters
This definition is the bridge from path geometry to chain-level generators. Downstream, the boundary of a path simplex is exactly the difference of constant point simplices: $\partial[\gamma]=[y]-[x]$. That identity feeds the existence lemma that joined points have homologous point chains, and it supplies the degree-$1$ data for the chain homotopy between point-inclusion maps built from a path.
In the broader foundation stack these facts underwrite $H_0$ computations and connectedness arguments for singular complexes of spheres and related spaces. The construction sits below the Mayer–Vietoris and subdivision machinery imported by the module; it does not itself touch the forcing chain (T0–T8) or the $J$-cost, but it is part of the topological substrate those later layers rely on when homology of configuration spaces appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.