toChain_amap
plain-language theorem explainer
Composing the singular-to-affine chain map of a continuous simplex σ with the chain map induced by an affine vertex map equals the chain map of the precomposed simplex σ∘affineMap(v). Algebraic topologists working the barycentric subdivision transport cite this naturality. The proof is a short AC-hom extension: reduce to generators, inject via simplexEquiv, and finish with ContinuousMap.comp_assoc plus affineMap_comp.
Claim. Let $\sigma:\Delta^n\to X$ be continuous and let $v:\mathrm{Fin}(n'+1)\to\Delta^n$ determine an affine map $A_v:\Delta^{n'}\to\Delta^n$. For every degree $m$, the composition of the chain map $\mathrm{toChain}(\sigma,m)$ with the affine-chain map induced by $A_v$ equals $\mathrm{toChain}(\sigma\circ A_v,m)$.
background
The module builds affine singular chains and barycentric subdivision operators on a topological space $X$. An affine $n$-chain in a type $\alpha$ is a finitely supported $\mathbb{Z}$-linear combination of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$ (abbreviated AC). The generator attached to a single tuple is the affine simplex.
Given a vertex tuple $v:\mathrm{Fin}(n+1)\to\Delta^m$, affineMap produces the continuous affine map $\Delta^n\to\Delta^m$ sending the $i$-th standard vertex to $v(i)$. The induced map on affine chains (amap) pushes those vertex tuples forward. Separately, toChain $\sigma$ $m$ turns a continuous singular simplex $\sigma:\Delta^n\to X$ into an $m$-chain in $X$ by pushing affine $m$-simplices along $\sigma$.
The lemma is the naturality square relating these two constructions: affine pushforward on the domain of $\sigma$ becomes precomposition of $\sigma$ itself.
proof idea
Extend by the universal property of AC: it is enough to check equality on a single affine generator $w$. Unfold LinearMap.comp_apply together with the generator rules amap_asimplex and toChain_asimplex on both sides. The resulting singular simplices agree after applying simplexEquiv, so injectivity of simplexEquiv reduces the goal to an equality of continuous maps. Rewrite with simplexEquiv_pushSimplex twice, ContinuousMap.comp_assoc, and affineMap_comp; both sides become identical and rfl closes.
why it matters
This naturality is the algebraic step that lets subdivision and prism operators move past a push of a generator. Downstream, gen_pushSimplex_comp_sdOp uses it as "the heart of the transport": sdOp on a pushed generator equals the subdivision of the pushed vertex tuple, and gen_pushSimplex_comp_tOp does the same for the prism homotopy operator tOp.
In the Recognition foundation layer the singular-subdivision package supplies the chain-level infrastructure for discrete recognition geometry (eight-tick octave structure, T7). Without commuting toChain past affine maps, the barycentric operators would not descend cleanly to singular chains on $X$, blocking later comparison maps and homology identities used by the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.