amap_comp_abnd
plain-language theorem explainer
Pushforward of affine chains along a set-map f commutes with the boundary operator: f_* ∘ ∂ = ∂ ∘ f_*. Anyone proving naturality of barycentric subdivision or the prism homotopy on affine chains cites this. The argument is generator-wise: extend by the free-module universal property and match alternating face sums under pushforward.
Claim. For any function $f:\alpha\to\beta$ and any $n\in\mathbb{N}$, writing $f_*$ for the induced $\mathbb{Z}$-linear pushforward on affine chains and $\partial$ for the alternating-face boundary, one has $(f_*)_n\circ\partial_{n+1}=\partial_n\circ(f_*)_{n+1}$ as maps $\mathrm{AC}\,\alpha\,(n+1)\to\mathrm{AC}\,\beta\,n$.
background
The module SingularSubdivision develops affine singular chains on an arbitrary carrier type $\alpha$. Generators are maps $w:\mathrm{Fin}(n+1)\to\alpha$ (ordered vertex tuples); the free $\mathbb{Z}$-module they span is written $\mathrm{AC},\alpha,n$. The elementary generator is the Dirac chain on $w$.
The boundary $\partial:\mathrm{AC},\alpha,(n+1)\to\mathrm{AC},\alpha,n$ is the usual alternating sum of faces: on a generator $w$ one has $\partial w=\sum_i(-1)^i,w\circ i^{\mathrm{succAbove}}$, extended by linearity. The pushforward along $f:\alpha\to\beta$ is the unique $\mathbb{Z}$-linear map sending the generator $w$ to the generator $f\circ w$.
Upstream, the face formula for $\partial$ on generators is recorded as the evaluation lemma for the boundary on elementary simplices; the free-module extension property supplies uniqueness of maps out of $\mathrm{AC}$.
proof idea
Both sides are $\mathbb{Z}$-linear maps out of free modules on generators, so it is enough to check equality on elementary simplices (hom-extensionality for affine chains).
On a generator $w$, expand both compositions: the left applies $\partial$ then pushforward, the right pushforward then $\partial$. Substitute the face formula for $\partial$ on generators, pull the pushforward through the finite sum and through scalar multiplication by $(\pm 1)$, and use that pushforward of a face $w\circ i^{\mathrm{succAbove}}$ is the corresponding face of $f\circ w$. The two alternating sums agree termwise, hence the maps agree.
why it matters
Naturality of $\partial$ under pushforward is the first equivariance step in the subdivision package. It is consumed by the equivariance theorem for the barycentric subdivision operator (a map intertwining apex/barycenter functions intertwines subdivision) and by the matching equivariance theorem for the subdivision prism homotopy.
Those two results are the algebraic backbone that lets subdivision and its chain homotopy descend along continuous maps, which is the standard route to proving that subdivision is homotopic to the identity on singular chains. In the Recognition Science foundation layer this sits under the singular-homology scaffolding used to control discrete geometric constructions (prisms, cones, eight-tick style periodic complexes) rather than under the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.