quotMap_injective
plain-language theorem explainer
If a morphism of short complexes of ℤ-modules sends a cycle to a boundary only when the cycle was already a boundary, the induced map on homology quotients is injective. Homological algebraists proving Mayer–Vietoris isomorphisms from pointwise checks cite this. The proof rewrites injectivity as trivial kernel and pushes the elementwise hypothesis through the quotient presentation via kerMap.
Claim. Let $\psi:S\to T$ be a morphism of short complexes of $\mathbb{Z}$-modules. Suppose that for every $x\in S_2$ with $g_S(x)=0$, if $\psi_2(x)$ lies in the image of $f_T$, then $x$ already lies in the image of $f_S$. Then the induced map on the homology quotients $\mathrm{quotMap}(\psi)$ is injective.
background
The ambient module builds singular Mayer–Vietoris data for short complexes of abelian groups (ℤ-modules). A short complex is a three-term diagram $X_1\xrightarrow{f}X_2\xrightarrow{g}X_3$ with $g\circ f=0$. Homology at the middle term is the quotient of cycles $\ker g$ by boundaries $\mathrm{im},f$.
A morphism $\psi:S\to T$ of short complexes supplies degreewise maps commuting with the differentials. It induces a map on homology by sending the class of a cycle to the class of its image. In this file that induced map is packaged as quotMap, built from the restricted map on kernels (kerMap) descended along the range inclusions via Submodule.mapQ.
The hypothesis is the standard elementwise injectivity criterion for homology: cycles mapped into boundaries must themselves be boundaries. The companion range lemma kerMap_range_le guarantees that kerMap respects the boundary submodules so the quotient map is well-defined.
proof idea
Rewrite injectivity as “maps to zero implies zero” via injective_iff_map_eq_zero. Lift an arbitrary quotient class $q$ to a representative cycle $\langle x,hx\rangle$ using surjectivity of Submodule.mkQ on the cycle submodule.
The assumption that quotMap ψ q = 0 rewrites, by Submodule.mapQ_apply and kerMap_range_le, as the statement that kerMap ψ ⟨x,hx⟩ is a boundary in $T$. Unpacking the subtype equality yields $\psi_2(x)=T.f,w$ for some $w$.
Feed $x$, the cycle condition, and this witness into the elementwise hypothesis hinj to obtain $v$ with $x=S.f,v$. Conclude that the original class is zero in the source quotient by exhibiting $v$ as a boundary witness.
why it matters
This lemma is one half of the concrete homology-isomorphism criterion isIso_homologyMap_of_elementwise in the same module. That parent result states that a short-complex morphism of ℤ-modules induces an isomorphism on homology as soon as two elementwise conditions hold: a surjectivity lifting condition and the injectivity condition proved here.
In the Recognition foundation stack, singular Mayer–Vietoris supplies the gluing exact sequence for chain-level recognition data on covers. Establishing homology isomorphisms from pointwise cycle/boundary checks is the algebraic engine behind comparing global and local singular complexes (prism operators, subdivision, pair sequences imported upstream). Without injectivity of the induced quotient map, the long exact Mayer–Vietoris sequence cannot be assembled from the short-complex morphism.
No forcing-chain landmark (T5–T8) is touched directly; the lemma is pure homological scaffolding inside Foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.