asimplex
plain-language theorem explainer
The standard generator of affine n-chains: the Dirac mass at a vertex tuple w : Fin(n+1) → α, written as the finitely supported integer function with value 1 at w. Anyone building boundaries, cones, or subdivision on affine chains cites it as the free basis element. The body is a one-line Finsupp.single constructor.
Claim. For a type $\alpha$ and $n \in \mathbb{N}$, and any vertex tuple $w : \mathrm{Fin}(n+1) \to \alpha$, the affine simplex generator is the affine $n$-chain that is the finitely supported $\mathbb{Z}$-valued function with value $1$ at $w$ and $0$ elsewhere.
background
Affine chains live in the free abelian group on ordered vertex tuples. The module AC α n is defined as finitely supported maps (Fin(n+1) → α) →₀ ℤ, so every chain is a finite integer linear combination of such tuples.
This generator is the unit basis vector at a single tuple: the chain that records one oriented affine simplex with those vertices. All subsequent operators in the module (boundary, cone, subdivision, augmentation) are specified by their values on these generators and extended by linearity.
The surrounding development is the affine half of singular subdivision: one builds a prism/cone calculus on free chains before transporting it to singular chains via the usual realization maps. Mathlib singular homology is imported; the affine layer is the combinatorial engine underneath.
proof idea
Pure definitional constructor: Finsupp.single w 1. No proof obligations beyond the type of finitely supported functions. Downstream lemmas such as AC.hom_ext immediately rewrite scalar multiples of these generators back to general Finsupp.single terms so linear maps are determined by their values on generators.
why it matters
This is the free generator that every affine operator is defined against. The boundary abnd is the linear combination that sends each generator to the alternating sum of face generators; abnd_asimplex is exactly that evaluation. Cone identities (abnd_comp_acone_zero), the chain-complex law ∂∂ = 0 (abnd_comp_abnd), and the subdivision/homotopy small-span lemmas in SingularMayerVietoris (sdOp_mem_smallSpan, tOp_mem_smallSpan) all reduce to checking generators via this object.
In the Recognition foundation stack, singular subdivision and Mayer–Vietoris on small spans are the topological scaffolding that later supports forcing and continuum arguments. The generator itself is pure linear algebra; its role is to make those operator identities checkable by AC.hom_ext on basis elements rather than on arbitrary chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.