AC
plain-language theorem explainer
Affine n-chains on a vertex set α are the free abelian group on ordered (n+1)-tuples: finitely supported integer combinations of maps Fin(n+1)→α. Every boundary, cone, and subdivision operator in the SingularSubdivision module is a ℤ-linear map on this type. The declaration is a one-line type synonym for Finsupp, so downstream proofs reduce to generator checks via AC.hom_ext.
Claim. For a type $\alpha$ and $n\in\mathbb{N}$, write $AC(\alpha,n)$ for the free abelian group of finitely supported functions $(Fin(n+1)\to\alpha)\to_0\mathbb{Z}$. Elements are finite $\mathbb{Z}$-linear combinations of ordered vertex $(n+1)$-tuples in $\alpha$ (affine $n$-chains).
background
Singular homology needs a chain complex before geometric realization. Here the generators are purely combinatorial: an ordered list of $n+1$ points of an ambient type $\alpha$, written as a function $w:Fin(n+1)\to\alpha$. The group of affine $n$-chains is the free $\mathbb{Z}$-module on those tuples, implemented as finitely supported functions to $\mathbb{Z}$.
The module builds the affine chain complex used for barycentric subdivision and Mayer–Vietoris arguments. The generator map asimplex sends a tuple $w$ to the Dirac chain with coefficient $1$ at $w$. Boundary abnd, cone acone, and subdivision operators are then defined by $\mathbb{Z}$-linear extension from generators.
Upstream arithmetic facts (mul_one and related) only appear as ambient ring infrastructure; the mathematical content of $AC$ is the free abelian group on vertex tuples.
proof idea
One-line type abbreviation: $AC(\alpha,n)$ is defined to be the Mathlib type of finitely supported maps from $Fin(n+1)\to\alpha$ into $\mathbb{Z}$. No proof obligations. Generator embedding and linear-map extensionality are supplied immediately afterward by asimplex and AC.hom_ext.
why it matters
This is the carrier type for the entire affine singular complex in Foundation.SingularSubdivision. Boundary $\partial:AC(\alpha,n+1)\to AC(\alpha,n)$, the cone identity $\partial(b\cdot c)=c-b\cdot(\partial c)$, and $\partial\partial=0$ (abnd_comp_abnd) are all maps on $AC$. Downstream, SingularMayerVietoris evaluates affine chains along continuous simplices and places them in small spans; CPM coercivity lemmas sit further out on the same chain-level infrastructure.
In the Recognition Science stack this is scaffolding for singular homology of recognition spaces, not a forcing-chain step (T0–T8). It supplies the algebraic language in which subdivision and excision arguments are stated before geometric or physical content is attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.