abnd_comp_atee
plain-language theorem explainer
On affine chains of positive degree, boundary of the prism operator plus prism of the boundary equals identity minus barycentric subdivision. Algebraic topologists cite this as the chain-homotopy half of Hatcher's Prop. 2.21 for affine simplices. The argument is induction on degree: each step reduces to the cone identity and ∂² = 0, then cancels by abelian-group arithmetic.
Claim. Fix a barycenter assignment $\mathrm{bary}$. For every $n\ge 0$, as $\mathbb{Z}$-linear endomorphisms of the affine chain group $AC(\alpha,n+1)$, $$\partial_{n+1}\circ T_{n+1}+T_n\circ\partial_n=\mathrm{id}-S_{n+1},$$ where $\partial$ is the affine boundary, $T$ is the prism (chain-homotopy) operator built from $\mathrm{bary}$, and $S$ is barycentric subdivision.
background
Affine $n$-chains $AC(\alpha,n)$ are finitely supported $\mathbb{Z}$-linear combinations of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. The affine boundary $\partial$ is the usual alternating face sum; barycentric subdivision $S$ replaces each simplex by the sum of simplices obtained by iteratively inserting barycenters; the prism operator $T$ is the chain homotopy that cones each simplex onto its barycenter (Hatcher's $T$ in the proof of Prop. 2.21).
The module develops these operators entirely on affine chains before transporting them to singular chains. A key prior identity is the cone relation $\partial\circ C+C\circ\partial=\mathrm{id}-\varepsilon$ (cone versus augmentation), recorded in-module as the composition of affine boundary with the affine cone.
The present statement is the positive-degree chain-homotopy identity $\partial T+T\partial=\mathrm{id}-S$ on $AC(\alpha,n+1)$, exactly as in Hatcher's write-up of barycentric subdivision.
proof idea
Proof by induction on degree $n$, after extending both sides as maps on generators via $AC$-hom extensionality.
Base $n=0$: expand $\partial T+T\partial$ on a $1$-simplex; the $T$ on degree $0$ vanishes, and the remaining term is identified with $\mathrm{id}-S$ by the cone identity applied to the barycenter of the vertices.
Successor: write the generator as $\sigma$, form $\sigma-T\partial\sigma$, and apply the cone identity at the barycenter of $\sigma$. The inductive hypothesis on $\partial\sigma$ gives $\partial T(\partial\sigma)+T\partial(\partial\sigma)=\partial\sigma-S(\partial\sigma)$. Nilpotence $\partial\circ\partial=0$ kills the double-boundary term, so $\partial(\sigma-T\partial\sigma)=S\partial\sigma$. Substituting and rearranging with $\mathrm{map_sub}$ yields $\partial T\sigma+T\partial\sigma=\sigma-S\sigma$; the final cancellation is pure abelian-group arithmetic (abel).
why it matters
This is the single-step chain homotopy that makes barycentric subdivision homotopic to the identity on affine chains. Downstream, the iterate form telescopes it to $\partial T^{(k)}+T^{(k)}\partial=\mathrm{id}-S^k$, which is how one proves $S$ is a chain-homotopy equivalence. The same identity is re-packaged on singular chain groups as the positive-degree half of the singular prism homotopy, feeding the comparison between singular and simplicial homology.
Inside Recognition Science this sits in the Foundation layer that imports Mathlib singular homology and the in-house prism calculus: it is pure algebraic topology scaffolding, not a forcing-chain (T0–T8) step, but it underwrites any later argument that needs subdivision operators or acyclic-model style comparisons on chain complexes built from recognition data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.