abnd
plain-language theorem explainer
Defines the affine-chain boundary ∂ : AC_α(n+1) → AC_α(n) as the ℤ-linear map sending each vertex (n+2)-tuple to the alternating sum of its face tuples. Anyone building cone identities, ∂∂=0, or barycentric subdivision chain maps on affine chains cites this. The body is the standard Finsupp.linearCombination of signed face generators.
Claim. For each $n\in\mathbb{N}$, the affine boundary is the $\mathbb{Z}$-linear map $\partial_n:\mathrm{AC}_\alpha(n+1)\to\mathrm{AC}_\alpha(n)$ determined on generators by $\partial_n[w]=\sum_{i\in\mathrm{Fin}(n+2)}(-1)^i\,[w\circ i^{\uparrow}]$, where $w:\mathrm{Fin}(n+2)\to\alpha$ is a vertex tuple and $i^{\uparrow}$ omits the $i$-th coordinate.
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 $w$ is the Dirac chain $\mathrm{asimplex}(w)=\mathbf{1}_w$.
This module develops the affine singular complex used for subdivision arguments (barycentric subdivision, prism/cone operators) without passing through topological singular simplices. The boundary is the algebraic face operator on those free generators: each face is the composition of $w$ with $\mathrm{Fin.succAbove},i$, which drops the $i$-th vertex.
Upstream, $\mathrm{AC}$ and $\mathrm{asimplex}$ fix the free $\mathbb{Z}$-module structure; maps out of $\mathrm{AC}$ are determined by values on generators via the module's extensionality lemma.
proof idea
Definition, not a proved theorem. It is the unique $\mathbb{Z}$-linear extension (via $\mathrm{Finsupp.linearCombination}$) of the classical alternating face formula on generators: on each $(n+2)$-tuple $w$, sum $(-1)^i$ times the generator of the face $w\circ i.\mathrm{succAbove}$. No further lemmas are invoked in the body; evaluation on generators is recovered later by $\mathrm{abnd_asimplex}$ via $\mathrm{lift_asimplex}$.
why it matters
This is the boundary operator that makes $(\mathrm{AC}_\alpha\bullet,\partial)$ a chain complex of affine chains. Downstream it is the left factor in $\partial\partial=0$ ($\mathrm{abnd_comp_abnd}$), in the cone identities $\partial(b\cdot c)=c-b\cdot\partial c$ and the degree-zero variant with augmentation $\varepsilon$ ($\mathrm{abnd_comp_acone}$, $\mathrm{abnd_comp_acone_zero}$), and in the chain-map properties of barycentric subdivision and its iterates ($\mathrm{abnd_comp_asub}$, $\mathrm{abnd_comp_asubIter}$).
In the Recognition foundation stack this supplies the algebraic $\partial$ needed for singular-subdivision and prism arguments that underwrite discrete geometric comparisons; it is pure chain-level scaffolding rather than a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.