acone_asimplex
plain-language theorem explainer
Coning an affine generator simplex at apex b yields the generator on the vertex tuple with b prepended. Algebraic topologists working the affine chain complex in SingularSubdivision cite this when reducing cone identities to generators. The proof is a short rewrite through the Finsupp mapDomain definitions of cone and simplex.
Claim. For any apex $b\in\alpha$ and vertex tuple $w:\mathrm{Fin}(n+1)\to\alpha$, the cone operator with apex $b$ applied to the generator simplex on $w$ equals the generator simplex on the prepended tuple $\mathrm{Fin.cons}\,b\,w$.
background
SingularSubdivision builds an affine chain complex used for barycentric subdivision and prism homotopies. An affine $n$-chain in a type $\alpha$ is a finitely supported $\mathbb{Z}$-linear combination of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$ (notation $AC,\alpha,n$). The generator attached to a tuple $w$ is the Dirac chain with coefficient $1$ at $w$.
The cone with apex $b$ is the $\mathbb{Z}$-linear map $AC,\alpha,n\to AC,\alpha,(n+1)$ that prepends $b$ to every support tuple via $\mathrm{Fin.cons}$. Upstream docs state it as "prepend $b$ to every vertex tuple," implemented by Finsupp.lmapDomain along that prepending map. Evaluating the cone on generators is the natural first check before proving operator identities by extensionality on generators.
proof idea
Definitional rewrite only. Unfold the cone as domain-map of finitely supported functions along $\mathrm{Fin.cons},b$, and the generator as a single with coefficient $1$. Push the single through lmapDomain / mapDomain_single, then reassemble as the generator on the prepended tuple. No induction and no appeal to boundary or augmentation.
why it matters
Parent results are the cone identities: in positive degree, $\partial(b\cdot c)=c-b\cdot(\partial c)$; in degree $0$, $\partial(b\cdot c)=c-\varepsilon(c)\cdot[b]$. Both proofs reduce via generator extensionality and rewrite with this lemma first. It also feeds the naturality statement that chain pushforward commutes with coning (apex pushed forward). Those identities are the algebraic engine for prism operators and subdivision homotopies in the foundation stack. Not itself a T0–T8 landmark; it is local chain-level scaffolding under singular homology infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.