kerMap_range_le
plain-language theorem explainer
A morphism of short complexes sends boundaries into boundaries under the induced map on cycles, so that map descends to homology. Anyone constructing concrete singular homology functors or Mayer–Vietoris maps cites this containment. The argument is a one-step chase of the middle commuting square of the chain map.
Claim. Let $\psi:S\to T$ be a morphism of short complexes of $\mathbb{Z}$-modules. Write $Z(S)=\ker(S.g)$ and $B(S)=\mathrm{im}(S.f)$ (and likewise for $T$), and let $\mathrm{kerMap}(\psi):Z(S)\to Z(T)$ be the restriction of $\psi$ to cycles. Then $B(S)\subseteq \mathrm{kerMap}(\psi)^{-1}(B(T))$, i.e. $\mathrm{kerMap}(\psi)$ carries boundaries of $S$ into boundaries of $T$.
background
The module SingularMayerVietoris builds a concrete singular Mayer–Vietoris sequence from short complexes of modules (degree-1 fragments $X_1\xrightarrow{f}X_2\xrightarrow{g}X_3$ with $g\circ f=0$). Cycles are the kernel of $g$; boundaries are the image of $f$. Homology is the quotient $Z/B$.
Given a morphism $\psi:S\to T$ of such complexes, the component $\tau_2$ restricts to cycles because $\psi$ commutes with $g$; that restriction is kerMap. The companion map from generators into cycles is moduleCatToCycles (the boundary inclusion $B\hookrightarrow Z$).
To induce a map on homology one still needs $\mathrm{kerMap}(\psi)(B(S))\subseteq B(T)$. That is exactly the range/comap containment proved here. Downstream, quotMap feeds this lemma into Submodule.mapQ to obtain the map on $Z/B$.
proof idea
Term-mode element chase. Take a general element of $\mathrm{range}(S.\mathrm{moduleCatToCycles})$, written as the class of $S.f(a)$. Propose the preimage witness $\psi.\tau_1(a)$ in $T.X_1$. Equality of the two paths $T.f(\psi.\tau_1(a))$ and $\psi.\tau_2(S.f(a))$ is the middle square $\psi.\mathrm{comm}_{12}$ evaluated at $a$, rewritten with ModuleCat.comp_apply. Subtype extensionality closes the membership in the comap.
why it matters
This is the boundary-compatibility half of “chain maps induce homology maps,” specialized to the concrete short-complex presentation used for singular Mayer–Vietoris. It is the side condition passed to Submodule.mapQ in quotMap (“the induced map on concrete homology”), and it is reused by quotMap_injective when proving that the induced homology map is mono under a lifting hypothesis on cycles.
In the Recognition foundation stack this sits under singular prism/pair/subdivision machinery: once homology maps are well-defined on the nose, one can assemble the MV long exact sequence that controls how recognition complexes glue. It is pure homological algebra scaffolding, not a forcing-chain (T0–T8) step, but without it the concrete singular homology functor is not even a functor on morphisms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.