amap_asimplex
plain-language theorem explainer
Pushforward of affine chains sends the generator simplex on a vertex tuple w to the generator on the image tuple f∘w. Anyone proving that amap intertwines boundary, cone, subdivision, or prism operators cites this on generators. The proof is a short rewrite through Finsupp.lmapDomain and mapDomain_single.
Claim. For any map $f:\alpha\to\beta$, dimension $n$, and vertex tuple $w:\mathrm{Fin}(n+1)\to\alpha$, the pushforward of affine $n$-chains along $f$ sends the generator simplex on $w$ to the generator simplex on $f\circ w$: $\mathrm{amap}(f,n)(\mathrm{asimplex}(w))=\mathrm{asimplex}(f\circ w)$.
background
The module builds affine singular chains and barycentric subdivision operators used to transport subdivision and prism homotopies onto continuous singular chains. An affine $n$-chain on a point type $\alpha$ is a finitely supported $\mathbb{Z}$-linear combination of vertex tuples $w:\mathrm{Fin}(n+1)\to\alpha$; the free generator on $w$ is written $\mathrm{asimplex}(w)=\mathrm{single}(w,1)$.
The pushforward $\mathrm{amap}(f,n):\mathrm{AC},\alpha,n\to_{\mathbb{Z}}\mathrm{AC},\beta,n$ is the linear map induced by postcomposition of tuples, $w\mapsto f\circ w$, via $\mathrm{Finsupp.lmapDomain}$. Because every chain is a linear combination of generators, identities of chain maps are routinely reduced to evaluation on $\mathrm{asimplex}$ (via $\mathrm{AC.hom_ext}$).
This lemma is the generator-level computation that makes that reduction work for $\mathrm{amap}$.
proof idea
Unfold $\mathrm{amap}$ and $\mathrm{asimplex}$. The definition of $\mathrm{amap}$ is $\mathrm{Finsupp.lmapDomain}$ along $w\mapsto f\circ w$, so $\mathrm{lmapDomain_apply}$ reduces the claim to $\mathrm{mapDomain}$ of a single. Then $\mathrm{Finsupp.mapDomain_single}$ yields $\mathrm{single}(f\circ w,1)$, which is again $\mathrm{asimplex}(f\circ w)$. Pure definitional rewrite; no induction.
why it matters
This is the generator identity behind all equivariance statements for affine operators under pushforward. Downstream it is used in $\mathrm{amap_comp_abnd}$ (pushforward commutes with boundary), $\mathrm{amap_comp_acone}$ (commutes with cone at a pushed apex), and the equivariance theorems $\mathrm{amap_comp_asub}$ and $\mathrm{amap_comp_atee}$ for subdivision and the subdivision homotopy when apex maps intertwine.
Those feed the transport lemmas $\mathrm{gen_pushSimplex_comp_sdOp}$ and $\mathrm{gen_pushSimplex_comp_tOp}$, which identify subdivision and prism operators on pushed singular generators with affine subdivision of the vertex tuple. In the Recognition foundation stack this is pure algebraic topology scaffolding: it lets singular subdivision and prism data move cleanly under continuous maps of spaces, without new physics content at this layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.