toChain_comp_chainMap
plain-language theorem explainer
Post-composition by the degree-m chain map of a continuous map f equals sending the singular simplex through f first, then converting to a chain. Algebraic topologists cite this when checking that subdivision and prism operators are natural. The proof is a short generator-wise identity: extend by linearity, reduce via the generator map lemma, and match the pushed simplex.
Claim. For a continuous singular $n$-simplex $\sigma:\Delta^n\to X$, a continuous map $f:X\to Y$, and any degree $m$, post-composition with the induced chain map $f_\#$ on $m$-chains sends the chain associated to $\sigma$ to the chain associated to $f\circ\sigma$: $f_\#\circ\mathrm{toChain}(\sigma)=\mathrm{toChain}(f\circ\sigma)$.
background
The module builds singular subdivision and prism operators on the free module of continuous singular simplices, in the style of classical singular homology (Mathlib's singular complex, plus local affine-simplex generators). A continuous map of spaces induces a chain map by post-composition on simplices; toChain packages an affine combinatorial simplex (or a continuous singular simplex) as an element of that free module.
The local setting is naturality bookkeeping for subdivision: one must know that converting a simplex to a chain commutes with pushing the simplex forward along $f$. Upstream, the generator map identity records how the free-module generators transform under the induced chain map: the generator of a pushed simplex is the image of the original generator. Affine pushforward of simplices is the geometric counterpart of precomposing the continuous representative with $f$.
Sibling constructions (affine boundary, cone, and barycentric operators) live in the same free-module language; this lemma is the pure naturality step that those operators inherit.
proof idea
Term-mode proof by free-module extensionality on generators. After AC.hom_ext, both sides are evaluated on a generator $w$. Unfolding toChain on affine simplices reduces the claim to an equality of generators: the chain-map image of the generator of the push of $\sigma$ along $w$ equals the generator of the push of $f\circ\sigma$ along $w$. The generator-map lemma rewrites the left-hand side; a one-step congruence finishes because pushforward of simplices is strictly functorial in the continuous map.
why it matters
Naturality of the singular subdivision operator and of the subdivision homotopy both call this identity when they move a continuous map past toChain on generators. Downstream, sdOp_natural states $f_#\circ\mathrm{sd}=\mathrm{sd}\circ f_#$, and tOp_natural states the corresponding intertwining for the prism/homotopy operator in adjacent degrees; both proofs reduce to generator-wise comparisons that need exactly this commutation.
In the Recognition foundation stack this is plumbing, not a forcing-chain landmark: it keeps the singular-complex side of the eight-tick / discrete-evolution story functorial under continuous maps of spaces, so later comparison maps and homology-level statements inherit naturality for free. No open scaffold remains; the lemma is fully proved and only closes a naturality square.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.