toChain_comp_abnd
plain-language theorem explainer
The map sending an affine simplex through a continuous singular simplex σ to a singular chain intertwines the affine boundary with the singular boundary: post-composing by ∂ equals pre-composing by the affine ∂. Cited by anyone proving that singular subdivision is a chain map or building the prism homotopy. Proof is pointwise on affine generators via AC.hom_ext, then termwise face comparison.
Claim. For a continuous map $\sigma:\Delta^{n}\to X$ and any $m\in\mathbb{N}$, the induced chain map $\mathrm{toChain}(\sigma)$ intertwines boundaries: $\partial_{m}\circ\mathrm{toChain}(\sigma)_{m+1}=\mathrm{toChain}(\sigma)_{m}\circ\partial^{\mathrm{aff}}_{m}$, where $\partial^{\mathrm{aff}}$ is the affine-simplex boundary and $\partial$ is the singular boundary on $C_{\bullet}(X)$.
background
The module builds singular subdivision and prism operators on the singular chain complex of a topological space $X$, in the style of classical algebraic topology (Eilenberg–Steenrod / Hatcher). An affine $m$-simplex is a map from the standard simplex that is affine on vertices; abnd is its alternating face-sum boundary. A continuous singular simplex $\sigma:\Delta^{n}\to X$ pushes affine simplices forward by composition (pushSimplex), and toChain σ is the induced linear map from the free module on affine simplices into the singular chain group of $X$.
The singular boundary bnd X m is the usual alternating sum of face restrictions. postComp (bnd X m) is post-composition of chain maps by that boundary. The lemma is the naturality / intertwining identity that makes pushforward of affine data compatible with both boundaries.
Sibling facts used nearby include toChain_asimplex (evaluation on a generator), abnd_asimplex (explicit face formula), and δ_pushSimplex (faces commute with pushforward).
proof idea
Term-mode argument by generator extension. Apply AC.hom_ext so it suffices to check equality on each affine generator $w$. Unfold both linear-map compositions and toChain_asimplex, reducing to an identity of singular chains on the pushed simplex.
Rewrite the left side by gen_d (singular boundary on a generator) and the right by abnd_asimplex, then map_sum to compare alternating face sums termwise. For each face index $k$, use map_smul, toChain_asimplex again, and δ_pushSimplex (pushforward commutes with the $k$-th face) to match coefficients and simplices.
why it matters
This is the naturality hinge between affine combinatorics and singular chains. Downstream, sdOp_comp_bnd quotes it (via the subdivision generator) to prove the singular subdivision operator is a chain map: $\partial\circ S=S\circ\partial$. The same intertwining feeds tOp_chain_homotopy_succ, the positive-degree prism identity $\partial T+T\partial=\mathrm{id}-S$ on $C_{n+1}(X)$.
In the Recognition foundation stack these are the standard tools that make singular homology well-defined and homotopy-invariant before any physics-facing forcing (T0–T8) is attached. Without the affine/singular boundary match, subdivision would not descend to homology and the prism homotopy would fail to cancel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.