abnd_comp_acone
plain-language theorem explainer
Cone identity for affine chains in positive degree: the boundary of the cone on a chain equals the chain minus the cone of its boundary. Algebraic topologists building barycentric subdivision or prism operators cite this as the basic homotopy relation for the cone operator. The proof extends by linearity to generators, expands the alternating face sum, and matches coefficients via face-map identities.
Claim. Fix a vertex $b$ and a degree $n\ge 0$. Let $\partial$ be the affine boundary on integer chains of vertex tuples, and let $b\cdot(-)$ be the cone operator that adjoins $b$ as a new initial vertex. Then for every affine $(n+1)$-chain $c$, $\partial(b\cdot c)=c-b\cdot(\partial c)$ as an equality of $\mathbb{Z}$-linear maps on affine chains.
background
The ambient object is the group $\mathrm{AC},\alpha,n$ of affine $n$-chains: finitely supported $\mathbb{Z}$-linear combinations of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. Generators are the affine simplices attached to such tuples. The affine boundary $\partial$ is the usual alternating sum of face restrictions; the cone operator $b\cdot(-)$ sends an $n$-simplex to the $(n+1)$-simplex obtained by prepending the fixed vertex $b$.
This module develops the affine (combinatorial) model of singular chains needed for barycentric subdivision and the prism/homotopy operators that prove subdivision is chain-homotopic to the identity. The cone identity is the elementary algebraic relation that makes those constructions work, in the same role as Hatcher's cone formula for singular simplices.
Composition and identity here are ordinary composition of $\mathbb{Z}$-linear maps on chain groups, not the $J$-automorphism composition from the cost algebra.
proof idea
Extend both sides by the universal property of free chains (AC.hom_ext) and evaluate on a generator $w$. Unfold composition, the cone on a simplex, and the boundary formula. Split the boundary sum with Fin.sum_univ_succ: the $j=0$ face contributes the original simplex (via cons_comp_succAbove_zero and the sign $+1$), while the remaining faces are rewritten with cons_comp_succAbove_succ, pow_succ, and neg_smul into exactly the cone of the lower boundary. A Finset.sum_congr finishes the match after moving the overall minus sign inside the sum.
why it matters
This is the positive-degree cone identity that the subdivision package rests on. Downstream, abnd_comp_asub uses the same boundary calculus to prove that barycentric subdivision is a chain map ($\partial\circ S=S\circ\partial$), and abnd_comp_atee uses the cone relation to establish the chain-homotopy identity $\partial\circ T+T\circ\partial=\mathrm{id}-S$ in positive degrees (Hatcher, proof of Prop. 2.21).
In the Recognition foundation layer, these facts underwrite the singular-homology toolkit (subdivision, prism operators, homotopy invariance) that later geometric and forcing arguments can quote without re-deriving classical chain algebra. It is pure algebraic topology infrastructure, not a forcing-chain step (T0–T8), but it is load-bearing for any argument that needs well-behaved affine chains on vertex sets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.