acone
plain-language theorem explainer
Affine cone with fixed apex b: the ℤ-linear map sending n-chains on α to (n+1)-chains by prepending b to every vertex tuple. Anyone building barycentric subdivision or the cone–boundary identities on affine chains cites it. Defined as domain reindexing of finitely supported functions via Fin.cons.
Claim. For a point $b \in \alpha$, there is a $\mathbb{Z}$-linear map $\mathrm{Cone}_b : C_n^{\mathrm{aff}}(\alpha) \to C_{n+1}^{\mathrm{aff}}(\alpha)$ on affine chains that sends each generator (ordered vertex tuple $w : \mathrm{Fin}(n+1) \to \alpha$) to the generator $\mathrm{cons}(b,w)$ obtained by prepending the apex $b$.
background
The ambient object is the group of affine $n$-chains on a type $\alpha$: finitely supported $\mathbb{Z}$-linear combinations of ordered vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. Generators are the formal simplices attached to those tuples; the boundary and augmentation operators act on this free module in the usual alternating way.
This module develops singular (barycentric) subdivision entirely in the affine-chain category, before passage to singular homology. The cone construction is the standard algebraic device that raises degree by one: fix an apex and join it to every simplex in a chain. The same pattern appears in classical singular homology when proving homotopy invariance and acyclicity of cones.
Upstream, the chain groups themselves are just the Finsupp abbreviation for those vertex maps. The geometric cone used elsewhere in the gravity/gluing stack is a different, combinatorial complex; here the name is purely the chain-level join.
proof idea
One-line definition: apply Finsupp.lmapDomain along the reindexing map $w \mapsto \mathrm{Fin.cons}, b, w$. That is the unique $\mathbb{Z}$-linear extension of “prepend apex $b$” from generators to all finitely supported chains. No further lemmas are invoked at the definition site; generator-level evaluation is recorded immediately afterward.
why it matters
This operator is the recursive engine of barycentric subdivision: the subdivision of an $(n+1)$-simplex is the cone, at the barycenter, of the already-subdivided boundary. It also supplies the two cone identities with the affine boundary (positive degree and degree zero), which are the chain-homotopy ingredients for proving that subdivision is chain-homotopic to the identity.
Downstream lemmas record that the cone of a generator is the obvious cons-simplex, that pushforward along a vertex map intertwines cones (apex pushed forward), and that the tee and subdivision operators are built from repeated cones. In the Recognition foundation stack this is pure algebraic topology scaffolding: it underwrites well-defined singular subdivision on affine chains, not a direct T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.