amap
plain-language theorem explainer
Pushforward of affine n-chains along a set map f:α→β: post-compose each vertex tuple with f and extend ℤ-linearly. Algebraic topologists cite it when transporting subdivision, cone, and boundary operators between point types. Defined as Finsupp domain-map on the free module of vertex maps.
Claim. For a map $f:\alpha\to\beta$ and $n\in\mathbb{N}$, there is a $\mathbb{Z}$-linear map sending an affine $n$-chain on $\alpha$ (a finitely supported integer combination of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$) to the affine $n$-chain on $\beta$ obtained by post-composing every vertex tuple with $f$.
background
Affine $n$-chains on a point type $\alpha$ are the free abelian group on vertex tuples $\mathrm{Fin}(n+1)\to\alpha$: finitely supported maps from those tuples into $\mathbb{Z}$. Generators are the elementary simplices attached to single tuples; general chains are integer linear combinations of them.
This module builds the affine subdivision calculus (boundary, cone from an apex, barycentric subdivision, and the prism homotopy) before pushing it into singular chains on a space. The pushforward along a bare map of point types is the naturality map for that calculus: it moves chains without changing coefficients, only the labels of vertices.
The construction sits in the Foundation layer that feeds singular homology comparisons used later in the Recognition forcing and continuum arguments.
proof idea
One-line definition: apply Mathlib's Finsupp.lmapDomain over $\mathbb{Z}$ to the function that sends a vertex tuple $w$ to $f\circ w$. That is exactly the unique $\mathbb{Z}$-linear extension of the generator map $\mathrm{asimplex},w\mapsto\mathrm{asimplex}(f\circ w)$.
why it matters
Naturality of the whole affine package rests on this map. Downstream lemmas prove it sends generators to generators, then that it intertwines boundary (amap_comp_abnd), cone (amap_comp_acone), subdivision (amap_comp_asub), and the subdivision homotopy (amap_comp_atee) whenever the apex (barycenter) functions commute with $f$.
toChain_amap further identifies the affine pushforward, under realization into a space $X$, with precomposition of singular simplices by the corresponding affine map. That bridge lets subdivision and prism identities descend from combinatorial affine chains to singular chains, which is the standard route to proving chain-homotopy equivalences used in continuum and homology arguments in the Foundation stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.