abnd_comp_acone_zero
plain-language theorem explainer
In degree zero, the affine boundary of the cone on a 0-chain c with apex b equals c minus the augmentation of c times the constant simplex at b. Algebraic topologists working with affine singular chains cite this as the base case of the cone homotopy identity. The proof evaluates both sides on a generator, expands the two-term boundary sum, and simplifies face maps via Fin.cons/succAbove identities.
Claim. For any apex $b\in\alpha$, the degree-$0$ cone identity holds as $\mathbb{Z}$-linear maps on affine $0$-chains: $\partial_0\circ(b\cdot\,{-})=\mathrm{id}-[b]\circ\varepsilon$, i.e. $\partial_0(b\cdot c)=c-\varepsilon(c)\,[b]$ for every $c$, where $\partial_0$ is the affine boundary, $b\cdot c$ is the cone of $c$ at $b$, $\varepsilon$ is the augmentation, and $[b]$ is the constant $0$-simplex at $b$.
background
Affine $n$-chains $\mathrm{AC}(\alpha,n)$ are finitely supported $\mathbb{Z}$-linear combinations of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. The generator attached to a tuple is the affine simplex. The affine boundary $\partial$, the cone operator with fixed apex $b$, and the augmentation $\varepsilon$ (sum of coefficients on $0$-chains) are the $\mathbb{Z}$-linear maps appearing in the identity.
This module builds singular subdivision for affine chains, importing Mathlib singular-homology infrastructure together with local prism and cone constructions. The cone identity is the algebraic statement that coning supplies a chain homotopy from the identity toward a constant map; the present result is the degree-$0$ specialization of that identity.
proof idea
Extend both sides by the free-module universal property and evaluate on a generator $w$. Rewrite the left side with the simplex formulas for cone and boundary, then expand the $\mathrm{Fin},2$ alternating sum. The two face compositions collapse by the companion lemmas: $\mathrm{cons},b,w\circ\mathrm{succAbove},0=w$ and $\mathrm{cons},b,w\circ\mathrm{succAbove},1=\mathrm{const},b$. The right side expands by identity, subtraction, span-singleton, and augmentation on a simplex. After matching signs ($(\pm 1)$ powers and $\mathrm{neg_smul}$), rewrite subtraction as addition of the negative to finish.
why it matters
Direct input to the chain-map property of barycentric subdivision ($\partial\circ S=S\circ\partial$) in the same module. That property is the algebraic engine for subdivision arguments in singular homology: it lets one replace singular chains by affine ones while preserving homology classes. In the Recognition Science foundation stack this sits under the singular-homology layer that supports discrete geometric control (eight-tick octave structure and dimensional forcing further up the chain). The degree-$0$ cone identity is the base case that lets the inductive subdivision argument close; without it the $n=0$ branch of the chain-map proof has no algebraic handle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.