toSSetObjEquiv_map
plain-language theorem explainer
Naturality of the singular-simplex equivalence: the singular functor sends a continuous map f to postcomposition with f on n-simplices. Anyone building chain maps, prism operators, or injectivity of induced maps on singular simplices cites this. The proof is a one-line pointwise identity (ext; rfl).
Claim. Let $X,Y$ be topological spaces and $f:X\to Y$ continuous. For any singular $n$-simplex $\sigma$ of $X$, the singular-simplex equivalence on $Y$ applied to the image of $\sigma$ under the singular functor equals the composite $f\circ\sigma$.
background
The module develops singular prisms and chain-level identities for topological spaces in TopCat, aiming at Hatcher's prism cancellation (homotopy invariance of singular homology). Singular $n$-simplices of a space $X$ are packaged as Idx X n, the value of the singular simplicial set TopCat.toSSet.obj X at the opposite standard simplex $\Delta[n]^{\mathrm{op}}$.
The equivalence toSSetObjEquiv identifies that simplicial-set value with continuous maps $|\Delta^n|\to X$. The singular functor TopCat.toSSet acts on a morphism $f:X\to Y$ by postcomposition on those maps. This lemma records that the equivalence intertwines that functorial action with ordinary composition of continuous maps.
Local setting is Stage 4 of the singular-chain development: generator normal forms and prism face identities before forming the singular chain complex with $\mathbb{Z}$ coefficients.
proof idea
Term-mode proof by pointwise extensionality. After ext x, both sides are definitionally the same continuous map evaluated at $x$: the left applies the equivalence after the simplicial-set map induced by $f$, the right is $f$ composed with the continuous representative of the simplex. No auxiliary lemmas are needed; the equality is rfl once points are exposed.
why it matters
Feeds three parents. toSSet_map_app_injective rewrites both sides via this naturality to conclude that injective continuous maps induce injective maps on singular $n$-simplices. simplexEquiv_map is a one-line retyping that is literally this lemma under the subdivision equivalence. prism_sum_cancellation sits in the same prism pipeline (Hatcher 2.10 alternating double-sum collapse to $g_\sharp-f_\sharp$), where naturality of simplex representatives is the bookkeeping step that lets face and prism operators move past continuous maps.
In the Recognition foundation stack this is pure singular-homology scaffolding: it does not touch J-cost, $\phi$, or the T0–T8 forcing chain directly, but it underwrites the topological chain complex used when geometric or homotopy content is later attached to recognition structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.