quotMap_surjective
plain-language theorem explainer
If a morphism of short complexes of ℤ-modules lifts every target cycle up to a boundary, the induced map on concrete homology is surjective. Homological algebraists cite it when turning elementwise cycle conditions into epi statements on H_*. The proof lifts a quotient class to a cycle, applies the hypothesis, and checks the two cycles differ by a boundary.
Claim. Let $\psi:S\to T$ be a morphism of short complexes of $\mathbb{Z}$-modules. Suppose that for every $y\in T_2$ with $d_T(y)=0$ there exist a cycle $x\in S_2$ and a chain $w\in T_1$ such that $\psi_2(x)=y+d_T(w)$. Then the induced map on concrete homology (cycles modulo boundaries) is surjective.
background
The module SingularMayerVietoris builds a concrete singular Mayer–Vietoris apparatus over short complexes of $\mathbb{Z}$-modules (degree pattern $X_1\xrightarrow{f}X_2\xrightarrow{g}X_3$). Concrete homology is the quotient module $\ker g,/,\mathrm{im},f$, realized via Mathlib submodules rather than the abstract ShortComplex.homology API alone.
A morphism $\psi:S\to T$ of short complexes induces a map on cycles that preserves boundaries. The definition quotMap packages that induced map as a linear map of the two concrete homology quotients, via Submodule.mapQ applied to the kernel map of $\psi$.
The hypothesis here is the elementwise surjectivity half of the usual “homology iso criterion”: every target cycle is homologous to the image of a source cycle. The companion injectivity half appears only in the stronger iso lemma downstream.
proof idea
Term-mode with a short tactic block. Fix a homology class $q$ in the target quotient. Lift it by Submodule.mkQ_surjective to a representative cycle $\langle y,hy\rangle$ in $\ker T.g$. Feed $y$ to the elementwise hypothesis to obtain a source cycle $x$ and a chain $w$ with $\psi_2(x)=y+T.f(w)$.
Send the class of $x$ forward under quotMap. After unfolding quotMap and Submodule.mapQ_apply, the two classes agree in the quotient precisely when their difference lies in the boundary submodule; the witness is $w$, and the identity $T.f(w)=\psi_2(x)-y$ is the rearranged hypothesis (closed by abel).
why it matters
This is the surjectivity half of the concrete homology criterion in the singular Mayer–Vietoris stack. Downstream, epi_homologyMap_of_elementwise rewrites the abstract ShortComplex.homologyMap through the left-homology map data and invokes this lemma to conclude the homology map is an epimorphism. The stronger isIso_homologyMap_of_elementwise pairs it with an elementwise injectivity hypothesis to get a full isomorphism on homology.
In the Recognition foundation layer this supplies the algebraic engine for comparing singular chain complexes on covers (prism, pair, and subdivision imports), so that Mayer–Vietoris gluing can be checked on cycles rather than on abstract derived functors. It does not itself invoke the forcing chain (T0–T8) or the J-cost; it is pure homological scaffolding those geometric arguments sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.