quotMap
plain-language theorem explainer
Induced ℤ-linear map on concrete homology for a morphism of short complexes of ℤ-modules: cycles modulo boundaries in the source map to those in the target. Anyone building explicit left-homology data or Mayer-Vietoris comparison maps for singular chains cites it. The body is the standard quotient map induced by the cycle-level restriction once boundaries are shown to land in boundaries.
Claim. Let $\psi:S\to T$ be a morphism of short complexes of $\mathbb{Z}$-modules. Write $Z(S)=\ker(g_S)$ and $B(S)=\operatorname{im}(S\text{'s map into cycles})$, and likewise for $T$. The cycle-level restriction of $\psi$ sends $B(S)$ into $B(T)$, and therefore descends to a $\mathbb{Z}$-linear map $Z(S)/B(S)\to Z(T)/B(T)$ on concrete homology.
background
The ambient module is singular Mayer-Vietoris for short complexes of $\mathbb{Z}$-modules in ModuleCat. A short complex $S$ has differentials $f_S:X_1\to X_2$ and $g_S:X_2\to X_3$ with $g_S\circ f_S=0$. Concrete cycles are $\ker(g_S)$; concrete boundaries are the image of the canonical map from $X_1$ into those cycles. Homology is the quotient of cycles by boundaries.
A morphism $\psi:S\to T$ supplies component maps compatible with the differentials. The sibling definition kerMap restricts the middle component of $\psi$ to a $\mathbb{Z}$-linear map on cycles (using that $\psi$ sends $\ker g_S$ into $\ker g_T$). The lemma kerMap_range_le records that this restriction sends source boundaries into target boundaries, which is exactly the hypothesis needed to descend to the quotient.
That descent is the standard Submodule.mapQ construction: a linear map that preserves a submodule pair induces a map of quotients.
proof idea
One-line definition. Apply Submodule.mapQ to the cycle map kerMap ψ, discharging the range-inclusion side condition with the lemma kerMap_range_le ψ. No further rewriting: the resulting linear map is the induced map on concrete homology by construction of mapQ.
why it matters
This is the homology component of the concrete left-homology map data. Downstream, lhMapData packages it as $\varphi_H$ (with kerMap as $\varphi_K$), so that Mathlib's homologyMap_eq identifies the abstract ShortComplex.homologyMap with this explicit quotient map.
Elementwise criteria then read off bijectivity: quotMap_surjective and quotMap_injective convert cycle-lifting and boundary-lifting hypotheses into surjectivity and injectivity of this map; those feed epi_homologyMap_of_elementwise and the main concrete criterion isIso_homologyMap_of_elementwise (a morphism of short complexes of $\mathbb{Z}$-modules induces an isomorphism on homology once the two elementwise conditions hold). In the Recognition foundation stack this is the algebraic engine for comparing singular chain complexes under covers, the input layer for Mayer-Vietoris arguments that later support geometric forcing (eight-tick structure, spatial dimension).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.