epi_homologyMap_of_elementwise
plain-language theorem explainer
If a short-complex morphism lifts every target cycle modulo boundaries from a source cycle, the induced map on homology is an epimorphism. Degree-0 chain wrappers in the singular Mayer–Vietoris toolkit cite this criterion. The proof rewrites homologyMap through lhMapData, reduces epi of the quotient map to elementwise surjectivity, then closes by composition of epis.
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 $T.g(y)=0$ there exist a cycle $x\in S_2$ and some $w\in T_1$ such that $\psi_{\tau_2}(x)=y+T.f(w)$. Then the induced homology map $H(\psi):H(S)\to H(T)$ is an epimorphism in $\mathbf{Mod}_{\mathbb{Z}}$.
background
The ambient module builds singular Mayer–Vietoris infrastructure over chain complexes of $\mathbb{Z}$-modules in Mathlib's ModuleCat. A short complex is a three-term diagram $X_1\xrightarrow{f}X_2\xrightarrow{g}X_3$ with $g\circ f=0$; its homology is $\ker g/\operatorname{im} f$. A morphism $\psi$ of short complexes supplies degreewise maps compatible with $f$ and $g$, and induces $H(\psi)$ on homology.
The elementwise hypothesis is the concrete cycle-lifting condition: every homology class in the target is hit by a source cycle up to a boundary in $T$. Internally this is packaged through lhMapData (the homology-map data of $\psi$) and quotMap (the map of quotients $\ker g_S/\operatorname{im} f_S\to\ker g_T/\operatorname{im} f_T$).
The local section is the homology criterion toolkit; later sections wrap the same idea for honest chain complexes via shortComplexFunctor'.
proof idea
Rewrite ShortComplex.homologyMap ψ via (lhMapData ψ).homologyMap_eq, so it factors through (lhMapData ψ).φH. Show Epi φH by identifying φH with ModuleCat.ofHom (quotMap ψ) and applying ModuleCat.epi_iff_surjective together with the already-proved quotMap_surjective ψ hsurj (which consumes the elementwise lifting hypothesis). Finish with epi_comp on the rewritten factorization.
why it matters
This is the short-complex engine behind the degree-0 chain-complex epi criterion epi_homologyMap_chain_zero, which specializes the same lifting hypothesis to HomologicalComplex.homologyMap φ 0 after killing the shape differential at $(0,0)$. That wrapper is part of Stage 2 toolkit D in SingularMayerVietoris: chain-complex interfaces needed to assemble singular Mayer–Vietoris exactness from prism, pair, and subdivision data.
In the broader Recognition foundation stack, Mayer–Vietoris-type exact sequences underwrite gluing and excision arguments on the discrete recognition complex (eight-tick octave, $D=3$ spatial skeleton). The lemma itself is pure homological algebra; its place is as a reusable epi test once singular cochains are connected to short complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.