bounds_of_retract
plain-language theorem explainer
If A is a retract of B and a degree-1 chain on A becomes a boundary after pushforward to B, then it was already a boundary on A. Algebraic topologists use this when transferring bounding relations along inclusions that split. The proof is a four-line calc using chain-map functoriality, identity, and boundary commutation.
Claim. Let $A,B$ be topological spaces and $f:A\to B$, $g:B\to A$ continuous maps with $g\circ f=\mathrm{id}_A$ (so $A$ is a retract of $B$). If $z$ is a singular $1$-chain on $A$ and $f_\sharp(z)$ is a boundary in $B$, then $z$ is a boundary in $A$.
background
The module works in the singular chain complex of spaces in TopCat, with chain groups written as the coproduct presentation Cgrp X n and boundary bnd X n : Cgrp X (n+1) → Cgrp X n. A continuous map induces a degreewise chain map chainMap f n, which commutes with boundaries and is functorial.
A retraction pair is a section-retraction $f:A\to B$, $g:B\to A$ with $g\circ f=\mathrm{id}_A$. The lemma says that being a boundary in degree 1 pulls back along such a retraction: if the image of $z$ bounds in $B$, then $z$ bounds in $A$. Upstream, elementwise commutation chainMap_bnd, composition chainMap_chainMap, and the identity law chainMap_id supply the three algebraic identities used in the calc.
proof idea
Unpack the witness $w$ with $f_\sharp(z)=\partial w$ in $B$. The candidate preimage boundary is $g_\sharp(w)$ in degree 2 on $A$. Then rewrite:
- $z=(\mathrm{id}A)\sharp(z)$ by
chainMap_id; - $(\mathrm{id}A)\sharp(z)=g_\sharp(f_\sharp(z))$ by
chainMap_chainMapand $g\circ f=\mathrm{id}_A$; - substitute $f_\sharp(z)=\partial w$;
- $g_\sharp(\partial w)=\partial(g_\sharp w)$ by the inverse of
chainMap_bnd.
So $z=\partial(g_\sharp w)$. Purely formal; no topology beyond the chain-map axioms.
why it matters
Feeds the bisection step bounds_of_halves (elementwise two-arc Mayer–Vietoris on complements of closed halves) and the main theorem arcComplementsAcyclic: 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 foundation stack this is scaffolding for linking-vanishing in high dimension, which underwrites the geometric side of the forcing chain (spatial dimension $D=3$ at T8, eight-tick structure). Without retract-stability of bounding, the inductive bisection on arc complements cannot close. The lemma itself is classical homological algebra; its value is as a reusable transfer step inside the formal arc-complement argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.