chainMap_chainMap
plain-language theorem explainer
Singular chain maps are functorial on elements: pushing an n-chain along f then g equals pushing along the composite morphism. Arc-complement and Mayer–Vietoris arguments cite this whenever they rewrite nested pushforwards. The proof is a short term extraction of degree-n components from the singular-chain-complex functor’s composition law, then ModuleCat composition.
Claim. Let $A,B,C$ be topological spaces and $f:A\to B$, $g:B\to C$ continuous. For every $n\in\mathbb{N}$ and every singular $n$-chain $x$ on $A$ with $\mathbb{Z}$ coefficients, $g_\#(f_\#(x))=(g\circ f)_\#(x)$, where $(\cdot)_\#$ denotes the induced map on the degree-$n$ singular chain group.
background
The ambient module builds singular homology with $\mathbb{Z}$ coefficients on TopCat in order to formalize arc-complement acyclicity (Hatcher 2B.1, arc case). The degree-$n$ singular chain group of a space $X$ is the coproduct $\coprod_{\sigma}\mathbb{Z}$ over singular $n$-simplices; the singular chain complex assembles these groups with the usual boundary.
A continuous map $f:X\to Y$ induces a chain-complex morphism, and the degree-$n$ component of that morphism is the chain map $f_#$. The present lemma is the elementwise form of functoriality of those degree-$n$ maps under composition of continuous maps.
Upstream, the singular-chain-complex functor supplies map_comp, so the complex-level composite equals the map of the composite; the only remaining step is to read off the degree-$n$ arrow and evaluate it on an element.
proof idea
Apply CategoryTheory.Functor.map_comp to the singular-chain-complex functor to obtain equality of chain-complex morphisms: the complex map of $f\gg g$ equals the composite of the complex maps of $f$ and of $g$.
Congruence on the degree-$n$ component yields equality of the corresponding ModuleCat arrows: the chain map of the composite equals the composite of the chain maps. Rewrite the goal with that equality and finish by ModuleCat.comp_apply, which evaluates a composite module morphism as successive application.
why it matters
Elementwise composition is the rewrite used whenever nested pushforwards appear in the arc-complement development. Downstream, zSeg_restrict rewrites restriction of a segment cycle along a composite inclusion; bounds_of_retract pulls bounding chains back along a retraction by composing chain maps with the section; bounds_of_halves and ultimately arcComplementsAcyclic rely on the same bookkeeping in the two-arc Mayer–Vietoris bisection.
The parent theorem arcComplementsAcyclic states that every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement in every dimension $D$ (Hatcher 2B.1, arc case). In the Recognition forcing chain this is part of the topological substrate for linking-vanishing in high dimensions and the $D=3$ spatial step (T8), not a mass or coupling computation itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.