eps_asimplex
plain-language theorem explainer
The augmentation of any generator affine 0-simplex equals 1. Algebraic topologists and anyone verifying that the augmentation is a chain map, or that the degree-0 cone identity holds, will cite this. The proof is a one-line application of the generator-lift lemma for the augmentation.
Claim. For every vertex assignment $w:\mathrm{Fin}\,1\to\alpha$, the augmentation of the corresponding generator affine $0$-simplex equals one: $\varepsilon_\alpha([w])=1$.
background
This module builds the affine singular chain complex used in the Recognition foundation layer. The free $\mathbb{Z}$-module $\mathrm{AC},\alpha,n$ is generated by vertex tuples $w:\mathrm{Fin}(n+1)\to\alpha$; the generator attached to $w$ is the Dirac mass $\mathrm{asimplex}(w)=\mathrm{Finsupp.single},w,1$.
The augmentation $\varepsilon_\alpha:\mathrm{AC},\alpha,0\to\mathbb{Z}$ is the unique linear map that sums coefficients of $0$-chains (points). On generators it is forced by the lift-on-generators construction: a linear map out of $\mathrm{AC},\alpha,n$ is determined by its values on $\mathrm{asimplex}$ tuples.
Upstream face and prism maps supply the simplicial operators that later interact with $\varepsilon$ (boundaries, cones). The local goal is the standard augmented chain-complex package: $\varepsilon\circ\partial=0$ and the cone identities in low degree.
proof idea
One-line term proof. Apply the generator-lift lemma for the augmentation (lift_asimplex) at the given $0$-tuple $w$. That lemma states that $\varepsilon$ evaluates to $1$ on every $\mathrm{asimplex}$ generator, which is exactly the claim.
why it matters
This is the base evaluation that makes the augmentation a genuine chain-map unit. Downstream, eps_comp_abnd uses it (via simp on the two-term boundary sum) to prove $\varepsilon\circ\partial=0$. The degree-0 cone identity abnd_comp_acone_zero likewise needs $\varepsilon([w])=1$ so that $\partial(b\cdot c)=c-\varepsilon(c)\cdot[b]$ holds on generators.
In the Recognition foundation stack, singular chains and their augmentations sit under the prism/subdivision calculus that interfaces with the eight-tick and Clifford bridge layers. The lemma itself is pure algebraic topology bookkeeping, but without it the augmented complex (and therefore any homology-level forcing argument that quotes $\varepsilon$) does not typecheck.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.