chainMap_bnd
plain-language theorem explainer
Singular chain maps commute with boundaries, elementwise: the boundary of a pushed chain equals the push of its boundary. Homology and arc-complement arguments cite this whenever continuous maps act on chains. The proof evaluates the HomologicalComplex naturality square of the induced chain map at a single chain.
Claim. Let $A,B$ be topological spaces and $f:A\to B$ continuous. For every $n\in\mathbb{N}$ and every singular $(n+1)$-chain $x$ on $A$ with $\mathbb{Z}$ coefficients, $\partial_B^n(f_\#(x))=f_\#(\partial_A^n(x))$, where $f_\#$ is the induced map on singular chain groups and $\partial$ is the singular boundary.
background
The ambient module develops arc-complement acyclicity in singular homology: every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement (Hatcher 2B.1, arc case). Chains live in the coproduct presentation Cgrp X n, the degree-$n$ singular chain group $\coprod_{\sigma}\mathbb{Z}$ of $X$. The boundary bnd X n is the differential $(SC X).d(n+1),n$ out of degree $n+1$. A continuous map $f:A\to B$ induces chainMap f n on those groups, coming from the singular chain complex morphism sChainMap f.
Commutation of $f_#$ with $\partial$ is the elementary naturality fact that makes pushforwards of cycles cycles and pushforwards of boundaries boundaries. Upstream, bnd and Cgrp are the typed interfaces from SingularPrism; the proof leans on Mathlib's HomologicalComplex.Hom.comm for that morphism.
proof idea
Term-mode extraction of a naturality square. Take HomologicalComplex.Hom.comm (sChainMap f) (n+1) n, which equates the two composite morphisms $C_{n+1}(A)\to C_n(B)$: boundary-then-push versus push-then-boundary. Apply congrArg by evaluating both sides at the given chain $x$. Finish with simpa using ModuleCat.comp_apply so composition of module morphisms becomes function application. No case split; pure diagram chase at one degree.
why it matters
Local workhorse for the arc-complement package. Immediate children: chainMap_cycle (pushforwards of cycles are cycles), bounds_map (bounding chains push forward), and bounds_of_retract (bounding pulls back along a retraction). Those feed arcComplementsAcyclic, the formal Hatcher 2B.1 arc case: every embedded arc in $S^D$ has $H_1$-acyclic complement in every dimension $D$.
In the Recognition foundation this is plumbing for linking-vanishing and high-dimensional topology that underwrites the spatial-dimension forcing (T8, $D=3$) and related acyclicity claims. It does not itself mention $\varphi$ or the J-cost; it is pure singular-homology infrastructure the later chain needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.