amap_comp_acone
plain-language theorem explainer
Pushforward of affine chains along a set map f intertwines the cone operators: coning at b then pushing equals pushing then coning at f(b). Anyone proving naturality of barycentric subdivision or the prism homotopy on affine chains cites this. The argument is generatorwise: extend by linearity, reduce to vertex tuples, and case-split the Fin index of the cone.
Claim. For any set map $f:\alpha\to\beta$, apex $b\in\alpha$, and degree $n$, the induced chain map $\mathrm{amap}(f)$ on affine chains satisfies $\mathrm{amap}(f)_{n+1}\circ C_b = C_{f(b)}\circ\mathrm{amap}(f)_n$, where $C_b$ is the cone operator that adjoins apex $b$ to an $n$-simplex.
background
In this module, affine $n$-chains $\mathrm{AC}(\alpha,n)$ are finitely supported $\mathbb{Z}$-linear combinations of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. Generators are the affine simplices attached to such tuples. The pushforward $\mathrm{amap}(f)$ postcomposes each vertex tuple with $f$ and extends by linearity, giving a degree-preserving map of chain groups.
The cone $C_b$ (written acone b) sends an $n$-simplex on vertices $w$ to the $(n+1)$-simplex whose $0$-th vertex is the apex $b$ and whose remaining vertices are those of $w$ (via $\mathrm{Fin}.\mathrm{cons}$). It is the algebraic cone used to build barycentric subdivision and the prism operator on affine chains, imported alongside Mathlib singular homology infrastructure and the local prism module.
The claim is the elementary naturality square: pushforward and coning commute once the apex is transported by $f$.
proof idea
Both sides are $\mathbb{Z}$-linear maps out of $\mathrm{AC}(\alpha,n)$, so it is enough to check equality on generators via the chain-group extensionality lemma. On a vertex tuple $w$, unfold composition of linear maps and the simplex-level formulas for cone and pushforward. The resulting $(n+1)$-tuples differ only by how $f$ is threaded through $\mathrm{Fin}.\mathrm{cons}$; a funext on the $\mathrm{Fin}(n+2)$ index, followed by Fin.cases on the zero versus successor slots, reduces each side to matching simp normal forms (cons_zero / cons_succ).
why it matters
This is the cone step in the naturality package for affine subdivision. Downstream, amap_comp_asub uses it to prove that a map intertwining apex (barycenter) functions intertwines the subdivision operator asub, and amap_comp_atee does the same for the subdivision homotopy atee. Those equivariance theorems are what make subdivision a natural chain-homotopy tool on affine chains rather than a one-space construction.
In the Recognition foundation stack, singular subdivision supplies the combinatorial chain-level scaffolding behind continuum and homology arguments that later interface with the forcing chain and geometric structure. The lemma itself is pure affine-chain algebra; its value is that the subdivision and prism naturality proofs factor cleanly through this one commuting square.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.