sdOp_comp_bnd
plain-language theorem explainer
The singular subdivision operator S on the singular chain complex of a topological space is a chain map: it intertwines the boundary, ∂S = S∂ in every degree. Algebraic topologists cite this when building barycentric subdivision and the prism/homotopy operators that prove homotopy invariance of singular homology. The proof reduces on generators to the affine boundary–subdivision identity, then matches faces via the push-simplex formula.
Claim. For every topological space $X$ and every $n \in \mathbb{N}$, the singular subdivision operator $S_{n+1}$ on degree $n+1$ chains of $X$ commutes with the singular boundary: $\partial_n \circ S_{n+1} = S_n \circ \partial_n$.
background
The module builds barycentric subdivision of singular chains in the coproduct presentation of the singular chain groups $C_\bullet(X)$. The boundary out of degree $n+1$ is the standard alternating-face map of the singular complex, written here as the morphism $\mathrm{bnd},X,n : C_{n+1}(X) \to C_n(X)$. On generators it is the alternating sum of faces (lemma gen_d).
Affine chains $AC_\alpha,n$ are free $\mathbb{Z}$-modules on tuples $Fin(n+1)\to\alpha$. Their boundary abnd is the alternating sum of faces $w\circ i.\mathrm{succAbove}$, and abnd_asimplex records that identity on generators. Subdivision of an affine simplex is induced by the barycentric map baryFn; the singular operator sdOp is obtained by transporting that affine construction along the simplex equivalence and summing over generators.
The local goal is the chain-map identity $\partial\circ S=S\circ\partial$, the algebraic backbone for iterated subdivision and for the prism chain homotopy that compares $S^k$ to the identity.
proof idea
Apply Sigma.hom_ext and work generatorwise. After rewriting with gen_sdOp and gen_d, the left composite on a generator becomes the image under toChain of the affine subdivided boundary. The key commutation is toChain_comp_abnd together with abnd_comp_asub (baryFn), which moves abnd past affine subdivision. Expand abnd_asimplex, push the sum and scalar multiplications through the morphisms (map_sum, Preadditive.sum_comp, map_smul, zsmul_comp), and finish each summand by δ_eq_pushSimplex plus gen_pushSimplex_comp_sdOp, matching the face of a subdivided generator with the subdivision of the face.
why it matters
Without $\partial S=S\partial$, iterated subdivision is not a chain map and the prism operator cannot telescope. Downstream, sdOpIter_comp_bnd lifts the identity to every iterate $S^k$ by induction on $k$, quoting this theorem in the successor step. That iterate chain-map property is then fed into tOpIter_chain_homotopy_succ, which proves the telescoped homotopy $\partial T_k+T_k\partial=\mathrm{id}-S^k$ in positive degrees.
In the Recognition Science foundation stack this sits inside SingularSubdivision / SingularPrism: the singular apparatus that supports observer and forcing constructions on chain-level data. It is pure algebraic topology scaffolding rather than a T0–T8 forcing step, but it is required infrastructure for any later argument that moves homology classes by subdivision or prism homotopies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.