sdOpIter_bnd_elem
plain-language theorem explainer
The k-fold singular subdivision operator commutes with the boundary on individual chains: subdividing then taking boundary equals boundary then subdividing. Algebraic topologists assembling Mayer-Vietoris exactness for open covers cite this when moving boundaries through iterated barycentric subdivision. The argument is a pure elementwise specialization of the already-proved morphism-level chain-map identity for the iterate.
Claim. For a space $X$, degrees $n,k\in\mathbb{N}$, and any singular chain $w\in C_{n+1}(X)$, $$\partial_n(\mathrm{sd}^{k}_{n+1}(w))=\mathrm{sd}^{k}_{n}(\partial_n w),$$ where $\mathrm{sd}^{k}$ is the $k$-fold iterate of the singular subdivision operator and $\partial_n:C_{n+1}(X)\to C_n(X)$ is the singular boundary.
background
Singular chains on a space $X$ are packaged degreewise as the coproduct group $C_n(X)=\coprod_{\sigma}\mathbb{Z}$ over singular $n$-simplices. The boundary $\partial_n:C_{n+1}(X)\to C_n(X)$ is the usual alternating face operator, typed on that coproduct presentation.
The singular subdivision operator is an endomorphism of each $C_n(X)$. Its iterate is defined by $\mathrm{sd}^{0}=\mathrm{id}$ and $\mathrm{sd}^{k+1}=\mathrm{sd}^{k}\circ\mathrm{sd}$. Upstream work already records the morphism identity $\mathrm{sd}^{k}{n}\circ\partial_n=\partial_n\circ\mathrm{sd}^{k}{n+1}$ (the chain-map property of the iterate).
This module develops the singular Mayer-Vietoris apparatus: chains small on an open cover $(U,V)$ with $U\cup V=X$, the inclusion of the small subcomplex into the ambient singular complex, and the injectivity/surjectivity inputs needed for the long exact sequence.
proof idea
Start from the morphism-level identity that the $k$-fold subdivision iterate commutes with the boundary as arrows $C_{n+1}(X)\to C_n(X)$. Apply congruence of evaluation at the fixed chain $w$ to both sides. A single simplification step with the module-category composition rule rewrites the resulting morphism equality as the stated elementwise equality. No new chain-level algebra is proved; the lemma is a pure specialization from arrows to elements.
why it matters
Two parent lemmas in the same module consume this identity. The injectivity input for small chains (every degree, with boundary from degree $n+1$) and the surjectivity input in positive degrees both move boundaries across iterated subdivision while tracking membership in the small span of an open cover. Without elementwise commutation, $\partial(\mathrm{sd}^{k}w)=\mathrm{sd}^{k}(\partial w)$ cannot be used inside those existence arguments.
In the Recognition foundation stack, singular Mayer-Vietoris is the gluing mechanism for local chain data on open covers of a space. This lemma is the routine bridge between the chain-map subdivision theory and the elementwise small-chain calculus those exactness inputs require. It does not itself touch the forcing chain (T0-T8) or the Recognition Composition Law; it sits strictly in the singular-homology scaffolding underneath.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.