abnd_comp_asub
plain-language theorem explainer
Barycentric subdivision of affine chains is a chain map: the boundary operator commutes with subdivision in every degree. Anyone assembling the subdivision homotopy or lifting to singular chains cites this affine-level commutation. The argument is induction on degree, reducing via the cone formula for subdivision and the cone/boundary identities already proved in the module.
Claim. Fix a barycenter assignment $b$. For every degree $n$, writing $\partial$ for the affine boundary and $S$ for barycentric subdivision on affine chains, one has $\partial_n \circ S_{n+1} = S_n \circ \partial_n$ as $\mathbb{Z}$-linear maps on affine $n$-chains (finitely supported integer combinations of vertex tuples).
background
Affine $n$-chains in a type $\alpha$ are the free abelian group on vertex tuples $\mathrm{Fin}(n+1)\to\alpha$: finitely supported $\mathbb{Z}$-linear combinations of those generators. The affine boundary $\partial$ is the usual alternating face sum, extended linearly. Barycentric subdivision $S$ is defined from a choice of barycenters by the standard cone recursion on generators: subdivide faces, then cone from the barycenter of the simplex.
The module builds the affine subdivision package before lifting to singular chains (via the prism and singular-homology imports). Two prior identities are used constantly: the cone commutes with boundary in the usual way ($\partial C + C\partial = \mathrm{id}-\varepsilon$ in degree $0$, and the higher-degree cone formula), and $\partial^2=0$. The doc-comment states the claim directly as the chain-map property $\partial\circ S=S\circ\partial$.
proof idea
Induction on degree $n$, after extending both sides by the universal property of free chains (hom-ext on generators).
Base $n=0$: evaluate on a generator $w$. Rewrite $S$ via its degree-$0$ formula, then apply the degree-$0$ cone/boundary identity at the barycenter of $w$. The augmentation term vanishes by $\varepsilon\circ\partial=0$, leaving equality of the two composites.
Successor step: invoke the inductive hypothesis. On a generator, expand $S$ by the cone formula, push $\partial$ through the cone via the higher cone/boundary identity, replace the inner $\partial\circ S$ by $S\circ\partial$ from IH, and cancel the remaining double-boundary term with $\partial^2=0$.
why it matters
This is the affine engine for the whole subdivision package. Downstream, it lifts by induction on the iterate count to $\partial\circ S^k=S^k\circ\partial$, and it is the chain-map input to the telescoped homotopy identity $\partial T_k+T_k\partial=\mathrm{id}-S^k$ in positive degrees. Those two results are exactly Stage 4 of the module (chain homotopy $T$ with $\partial T+T\partial=\mathrm{id}-S$, and its iterate).
At the singular level, the same commutation becomes $\partial\circ S=S\circ\partial$ for the singular subdivision operator, which is how the construction enters singular homology. In the Recognition foundation stack this is pure algebraic topology scaffolding: it underwrites chain-level comparisons used when the forcing chain and discrete octave structure are later matched to continuum homology, not a direct T5–T8 step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.