bounds_map
plain-language theorem explainer
Boundaries of singular 1-chains push forward under continuous maps: if a 1-chain on A is a boundary, its image under the induced chain map is a boundary on B. Algebraic topologists in the arc-complement acyclicity development would cite it. The proof is a short witness transfer via boundary/chain-map commutation.
Claim. Let $A,B$ be topological spaces and $f\colon A\to B$ continuous. If $z$ is a singular $1$-chain on $A$ with $z=\partial w$ for some singular $2$-chain $w$, then the induced chain-map image $f_\sharp(z)$ is a boundary on $B$.
background
The ambient setting is the singular chain complex of a space in TopCat, with integer coefficients. The degree-$n$ chain group is the coproduct $\coprod_{\sigma} \mathbb{Z}$ over singular $n$-simplices; the boundary $\partial$ is the usual alternating face sum, typed as a morphism out of degree $n+1$.
A continuous map $f\colon A\to B$ induces a chain map $f_\sharp$ in each degree. The key upstream fact is elementwise commutation of boundary and chain map: $\partial_B\circ f_\sharp = f_\sharp\circ\partial_A$ in every degree (the HomologicalComplex naturality identity specialized to these presentations).
The module develops acyclicity properties of arc complements; this lemma records that the property of being a boundary is preserved by pushforward along any continuous map, specialized here to 1-chains.
proof idea
Unpack the hypothesis to a witnessing 2-chain $w$ with $z=\partial_A w$. The candidate witness on $B$ is $f_\sharp(w)$ in degree 2. The required identity $\partial_B(f_\sharp w)=f_\sharp(z)$ is exactly the degree-1 case of the upstream commutation lemma chainMap_bnd, after substituting $z=\partial_A w$. No further diagram chase is needed.
why it matters
In the Foundation arc-complement acyclicity thread, one repeatedly moves chains along continuous maps (inclusions, retractions, homeomorphisms) while tracking whether they remain boundaries. This lemma is the pushforward half of that bookkeeping: bounding is functorial in the covariant direction for arbitrary continuous maps.
A sibling statement (bounding pulls back along retractions) handles the contravariant direction needed for deformation retracts and homeomorphisms. Together they let homology-vanishing statements transfer between spaces related by elementary maps, which is the standard route to showing certain low-degree singular homology of arc complements vanishes.
No downstream consumers are wired yet in the graph; the lemma sits as local infrastructure for that acyclicity argument rather than a direct step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.