toSSetObjEquiv_
plain-language theorem explainer
Naturality of the singular-simplex identification: the simplicial face operator δ_j on singular simplices equals precomposition with the topological face inclusion of the standard simplex. Cited by anyone building prism operators or singular chain boundaries in this foundation layer. Proof is pointwise extensionality followed by definitional equality.
Claim. Let $X$ be a topological space, $n\in\mathbb{N}$, $j\in\{0,\ldots,n+1\}$, and $a$ a singular $(n+1)$-simplex of $X$. Under the standard identification of singular $n$-simplices with continuous maps $\Delta^n\to X$, the face $\delta_j(a)$ corresponds exactly to the composite of the map for $a$ with the face inclusion $\mathrm{face}_j:\Delta^n\hookrightarrow\Delta^{n+1}$.
background
The singular simplicial set of a space $X$ has, in degree $n$, the set of continuous maps from the standard topological $n$-simplex $\Delta^n$ into $X$. In this module that set is abbreviated as the index type of singular $n$-simplices (the generators of the degree-$n$ singular chain group with $\mathbb{Z}$ coefficients).
The face operators $\delta_j$ of the singular simplicial set are induced by the coface maps of the simplex category. On the topological side those cofaces become continuous face inclusions $\mathrm{face},j:\Delta^n\hookrightarrow\Delta^{n+1}$. The lemma records that the canonical equivalence between the two presentations intertwines these two actions: simplicial face equals precomposition with topological face.
The surrounding module develops prism operators (products of a simplex with the unit interval) used to compare singular chains under homotopies; face naturality is the elementary compatibility needed before those prism maps can be written down.
proof idea
After applying the identification on both sides, both expressions are continuous maps $\Delta^n\to X$. Extensionality reduces the goal to equality at an arbitrary point of $\Delta^n$. At each point the two sides unfold to the same composite by the definitions of the singular face operator, the identification, and the topological face inclusion, so rfl closes the goal. No external lemmas are required.
why it matters
This is elementary naturality infrastructure inside Foundation.SingularPrism. Prism constructions for singular chains repeatedly move face operators past the identification with continuous maps; without this equality those rewrites would be ad hoc. Downstream prism and homotopy arguments in the same module rely on faces commuting with the equivalence in exactly this form.
In the broader Recognition Science stack the singular-homology layer supports the topological side of the forcing chain (octave structure, dimensional constraints). The lemma itself is pure algebraic topology and does not encode a Recognition-specific constant or forcing step; it simply keeps the singular-set presentation usable when prism operators are later assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.