simplexEquiv_map
plain-language theorem explainer
Naturality of the retyped singular-simplex equivalence: pushing an m-simplex of X along a continuous map f:X→Y, then reading it as a map from the standard simplex, equals postcomposing the original continuous map with f. Cited wherever singular chains are transported under continuous maps (Mayer–Vietoris push/lift, arc-complement push, sphere point extraction, subdivision naturality). Proof is a one-line retyping of the underlying toSSet object equivalence naturality.
Claim. Let $f:X\to Y$ be a morphism of topological spaces and let $a$ be a singular $m$-simplex of $X$. Writing $\mathrm{simplexEquiv}$ for the identification of singular $m$-simplices with continuous maps $\Delta^m\to X$, one has $\mathrm{simplexEquiv}_Y\bigl((\mathrm{toSSet}\,f)_m(a)\bigr)=f\circ\mathrm{simplexEquiv}_X(a)$.
background
In the singular-set pipeline, Idx X m is the set of singular $m$-simplices of a space $X$ (the index set of the degree-$m$ singular chain group). The Mathlib equivalence TopCat.toSSetObjEquiv identifies each such simplex with a continuous map out of the standard simplex, but its domain is written in an awkward normal form that blocks rewriting.
simplexEquiv X m is exactly that equivalence, retyped so the domain is literally $C(\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin}(m+1)),X)$. The local module builds singular subdivision and the operators needed for chain-level arguments (barycentric subdivision, prism operators, Mayer–Vietoris).
Upstream, toSSetObjEquiv_map already records the naturality law: the functorial action of TopCat.toSSet on a continuous map $f$ is postcomposition with $f$. The present lemma is the same identity under the retyped name.
proof idea
One-line term proof: apply the upstream lemma toSSetObjEquiv_map f a. Because simplexEquiv is definitionally toSSetObjEquiv at op [m], no further rewriting or extensionality is required.
why it matters
This is the workhorse naturality step for every place singular simplices are pushed or lifted along continuous maps or subspace inclusions. Downstream it discharges the key equalities in arc-complement acyclicity (cPush_cLift, range_cPush), in the singular Mayer–Vietoris push/lift pair (pushIdx_liftIdx, range_pushIdx), in sphere point extraction (pointOf_map), and in naturality of the subdivision and prism operators (sdOp_natural, tOp_natural).
Within Recognition Science foundation work, those operators feed homology computations (acyclicity of complements, sphere homology, MV exactness) that underwrite topological forcing arguments. The lemma itself is pure singular-set infrastructure: it does not invoke J-cost, the forcing chain T0–T8, or the phi ladder, but it keeps the chain-level bookkeeping definitionally clean so those later arguments can rewrite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.