simplexEquiv
plain-language theorem explainer
Equates the index type of singular m-simplices on a space X with continuous maps from the standard geometric m-simplex into X. Anyone writing singular-chain arguments that need range membership, face restrictions, or subspace lifts cites this bridge. It is a one-line retyping of the standard singular-set object equivalence, chosen so the domain is literally the geometric simplex rather than a rewrite-blocking normal form.
Claim. For a topological space $X$ and $m \in \mathbb{N}$, the set of singular $m$-simplices of $X$ is in canonical bijection with the set of continuous maps $\Delta^m \to X$, where $\Delta^m = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}(m+1))$ is the standard geometric $m$-simplex.
background
In singular homology, an $m$-simplex of a space $X$ is a continuous map from the standard geometric simplex $\Delta^m$ into $X$. The Recognition foundation packages the index set of those simplices as Idx X m, defined as the value of the singular simplicial set of $X$ at the opposite of the simplex category object of dimension $m$. The free abelian group on that index set is the degree-$m$ singular chain group.
Mathlib already supplies an equivalence between that simplicial-set value and continuous maps out of a definitionally equal presentation of $\Delta^m$. The equal presentation uses the normal form $\mathrm{Fin}((\mathrm{unop}(\mathrm{op},[m])).\mathrm{len}+1)$, which is definitionally $\mathrm{Fin}(m+1)$ but blocks ordinary rewriting and composition lemmas that expect the geometric simplex written with $\mathrm{Fin}(m+1)$.
Upstream face maps (topological realizations of $\delta_j$ via $\mathrm{Fin.succAbove}$) and the prism infrastructure assume the geometric form. This equivalence is the local bridge that makes those face maps and chain operations talk to the same objects.
proof idea
One-line wrapper: apply the Mathlib singular-set object equivalence TopCat.toSSetObjEquiv at op [m]. No extra algebraic work; the entire content is the retyping of the domain of the continuous map to stdSimplex ℝ (Fin (m + 1)).
why it matters
This is plumbing, but it is load-bearing plumbing. Downstream, arc-complement acyclicity (Hatcher 2B.1, arc case) lifts ambient simplices into complement subtypes, checks that ranges miss closed sets, and pushes chains back; every one of those steps applies the equivalence or its inverse (cLift, cPush_cLift, range_cPush, exists_chain_lift). The singular Mayer–Vietoris development uses the same pattern to lift simplices whose range lies in an open set (liftIdx, pushIdx_liftIdx, middle exactness).
Those homology facts sit under the foundation layer that feeds dimensional and linking arguments in the Recognition forcing chain (spatial dimension $D=3$, eight-tick structure, and related topological constraints). Without a rewrite-friendly identification of singular simplices with geometric maps, the subspace-lift and support-control lemmas do not compose cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.