chainMap_cycle
plain-language theorem explainer
Pushforwards of singular 1-cycles along continuous maps remain 1-cycles: if ∂z = 0 in A, then ∂(f_# z) = 0 in B. Algebraic topologists cite it whenever induced maps on H₁ are formed elementwise. The proof is a three-step rewrite: commute boundary past the chain map, apply the cycle hypothesis, then use that morphisms send zero to zero.
Claim. Let $A,B$ be topological spaces and $f\colon A\to B$ continuous. If $z$ is a singular $1$-chain on $A$ with $\partial_A z=0$, then $\partial_B(f_\# z)=0$, where $f_\#$ is the induced map on singular chains with $\mathbb{Z}$ coefficients.
background
The module works in the singular chain complex of spaces in TopCat, with integer coefficients. Chain groups $C_n(X)$ are presented as coproducts of $\mathbb{Z}$ indexed by singular $n$-simplices; the boundary $\partial\colon C_{n+1}(X)\to C_n(X)$ is the usual alternating face sum, and a continuous map $f$ induces degreewise chain maps $f_#$.
A $1$-cycle is a degree-$1$ chain with vanishing boundary. The sibling lemma on boundary/chain-map commutation states elementwise that $\partial_B\circ f_#=f_#\circ\partial_A$. That identity is the only nontrivial input here: once boundaries commute with pushforward, cycles are visibly preserved.
Locally this sits inside the arc-complement acyclicity development (Hatcher 2B.1, arc case): one repeatedly pushes $1$-cycles of open pieces of $S^D\setminus\mathrm{im}(a)$ along inclusions and needs those images to stay cycles.
proof idea
Term-mode rewrite in three steps. First apply the elementwise commutation lemma: $\partial_B(f_# z)=f_#(\partial_A z)$. Second substitute the hypothesis $\partial_A z=0$. Third use that the chain-map morphism sends zero to zero (map_zero). No case splits or homology-class machinery.
why it matters
This is the cycle-preservation half of induced maps on $H_1$, used throughout the arc-complement package. Downstream, naturality of the homology class of a $1$-cycle quotes it to justify that $f_# z$ is still a cycle before forming $[f_# z]$. The segment-restriction lemma for arcs in $S^D$ is literally an application: restricting a cycle off the full arc to a smaller parameter interval stays a cycle.
It also feeds the elementwise Mayer–Vietoris injectivity and bisection steps (bounds_of_mv, bounds_of_halves), which assemble into the main theorem that every embedded arc in $S^D$ has $H_1$-acyclic complement in every dimension $D$. That formal Hatcher 2B.1 arc case is foundation infrastructure for linking-vanishing arguments in the Recognition chain (high-dimensional topology supporting the $D=3$ forcing landscape), not a physics identity itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.