simplexEquiv_
plain-language theorem explainer
Face maps on singular simplices commute with the retyping equivalence that identifies abstract singular simplices of a space X with continuous maps out of the standard simplex. Anyone tracking naturality of singular chains under subdivision or prism operators will cite it. The proof is a one-line retyping of the corresponding naturality statement for the underlying TopCat-to-sSet equivalence.
Claim. For any topological space $X$, any $m\in\mathbb{N}$, any face index $j\in\mathrm{Fin}(m+2)$, and any singular $(m+1)$-simplex $a$ of $X$, the retyping equivalence applied to the $j$-th face of $a$ equals the composition of the retyped simplex of $a$ with the standard affine face map $\mathrm{face}_j:\Delta^m\to\Delta^{m+1}$.
background
Singular homology is built from the simplicial set of continuous maps $\Delta^n\to X$. In this module the abstract singular $n$-simplices of $X$ (the $n$-simplices of $\mathrm{TopCat.toSSet}.\mathrm{obj},X$) are identified with continuous maps out of the standard geometric simplex via a retyping equivalence, written here as the family of maps that send an abstract simplex to its underlying continuous representative.
Face operators $\delta_j$ on the simplicial set side restrict a singular $(m+1)$-simplex along the inclusion of the $j$-th face of $\Delta^{m+1}$. On the geometric side the same operation is ordinary precomposition with the affine face embedding $\mathrm{face}_j$. The present statement asserts that the retyping equivalence intertwines these two descriptions.
The surrounding module develops singular subdivision and prism operators (imported from SingularPrism) needed for chain-homotopy and subdivision arguments in the Recognition foundation layer.
proof idea
One-line term proof: the claim is exactly the face-naturality lemma already proved for the underlying TopCat-to-sSet object equivalence, applied to the same face index $j$ and simplex $a$, then retyped into the local simplexEquiv notation.
why it matters
Naturality of the simplex retyping under faces is the bookkeeping step that lets subdivision and prism constructions move freely between abstract singular chains and geometric maps. Without it, face-boundary identities and prism face relations cannot be transported across the equivalence. In the Recognition foundation stack this sits under SingularSubdivision, which supplies the topological scaffolding for discrete octave and eight-tick constructions (T7) once singular chains are compared with combinatorial subdivisions. No downstream consumers are recorded in the graph yet; the lemma is local infrastructure for later subdivision naturality and chain-homotopy identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.