lift_asimplex
plain-language theorem explainer
Any ℤ-linear map out of affine n-chains, when evaluated on the generator attached to a vertex tuple w, returns the coefficient function at w. Algebraic topologists and anyone reducing chain identities (boundary, cone, subdivision, augmentation) to generators cite this. The proof is three rewrites: unfold the single-support generator, apply the Finsupp single identity, cancel the unit scalar.
Claim. Let $M$ be an abelian group with a $\mathbb{Z}$-module structure, let $f$ assign to each vertex $(n+1)$-tuple in $\alpha$ an element of $M$, and let $w$ be such a tuple. Then the $\mathbb{Z}$-linear combination of $f$ against the affine simplex generator at $w$ equals $f(w)$: $\mathrm{linComb}_{\mathbb{Z}}(f)\,(\mathrm{asimplex}\,w)=f(w)$.
background
Affine $n$-chains $\mathrm{AC},\alpha,n$ are finitely supported $\mathbb{Z}$-valued functions on vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. The generator attached to a tuple $w$ is the Dirac mass $\mathrm{asimplex},w:=\mathrm{Finsupp.single},w,1$.
Maps out of $\mathrm{AC},\alpha,n$ into a $\mathbb{Z}$-module $M$ are routinely defined by $\mathrm{Finsupp.linearCombination},\mathbb{Z},f$ for a coefficient function $f$ on tuples. Evaluating such a map on a generator is the basic sanity check that the linear extension really extends $f$.
The module builds affine singular subdivision (boundary, cone, barycentric subdivision, and realization into continuous singular chains). This lemma is the evaluation step used whenever those operators are checked on generators.
proof idea
Term-mode rewrite chain. Unfold $\mathrm{asimplex}$ to $\mathrm{Finsupp.single},w,1$, apply $\mathrm{Finsupp.linearCombination_single}$ (linear combination on a single-support Finsupp is scalar multiplication of the coefficient), then $\mathrm{one_smul}$ cancels the unit coefficient. No induction or case split.
why it matters
This is the generator-evaluation lemma for the whole affine-chain calculus in SingularSubdivision. Downstream one-liners all reduce to it: $\mathrm{abnd_asimplex}$ (boundary of a generator is the alternating face sum), $\mathrm{eps_asimplex}$ (augmentation sends a $0$-simplex to $1$), $\mathrm{asub_asimplex}$ and $\mathrm{atee_asimplex}$ (barycentric subdivision and the prism/tee operators on generators), and $\mathrm{toChain_asimplex}$ (realization of an affine generator as a continuous singular simplex).
In the Recognition foundation layer this underwrites the discrete chain complex used for singular subdivision and prism arguments, which sit upstream of continuum limits and homology comparisons. It is pure linear algebra over $\mathbb{Z}$; no forcing-chain step (T0–T8) is invoked here, but the chain complex it services is part of the geometric scaffolding those steps later use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.