lhMapData
plain-language theorem explainer
Packages a short-complex morphism of ℤ-modules into Mathlib's left-homology map data, using the induced kernel and quotient maps. Homological algebraists cite it when turning elementwise cycle/boundary conditions into statements about homology maps. The body fills the three required squares by direct diagram chase and reflexivity.
Claim. Given a morphism $\psi$ of short complexes of $\mathbb{Z}$-modules, assemble the left-homology map data relative to the standard $\mathrm{ModuleCat}$ left-homology data on domain and codomain: the kernel component is the map on kernels induced by $\psi$, and the homology component is the induced map on quotients by images, with the three naturality squares holding.
background
The ambient module builds singular Mayer–Vietoris machinery for chain complexes of abelian groups (viewed in ModuleCat ℤ). A short complex is a three-term diagram $X_1 \xrightarrow{f} X_2 \xrightarrow{g} X_3$ with $g\circ f=0$; left homology is $\ker g/\mathrm{im},f$.
Mathlib's LeftHomologyMapData is the structure that records how a short-complex morphism acts on kernels and on homology, together with the commuting triangles that make the induced homology map well-defined. Here both sides use the canonical moduleCatLeftHomologyData.
Upstream, kerMap ψ is the restriction of the middle component of ψ to kernels, and quotMap ψ is the induced map on the homology quotients. The construction sits downstream of the singular prism, pair, and subdivision infrastructure imported by the module.
proof idea
Definitional construction, not a deep argument. Set the kernel arrow to ModuleCat.ofHom (kerMap ψ) and the homology arrow to ModuleCat.ofHom (quotMap ψ). The inclusion-commuting square is reflexivity after hom_ext. The middle square reduces, after Subtype.ext, to the short-complex naturality identity $\psi_2\circ S.f = T.f\circ\psi_1$, read off ψ.comm₁₂ via comp_apply. The projection square is again definitional equality of the quotient maps.
why it matters
This is the concrete bridge from elementwise chain-level maps to Mathlib homology morphisms inside the singular Mayer–Vietoris development. Downstream, isIso_homologyMap_of_elementwise rewrites ShortComplex.homologyMap ψ via (lhMapData ψ).homologyMap_eq and obtains an isomorphism from surjectivity of the homology component plus an injectivity criterion; epi_homologyMap_of_elementwise does the same for epimorphisms. classOf_natural in ArcComplementAcyclic uses the same packaging when pushing homology classes along chain maps.
In the Recognition foundation layer this supports acyclicity and excision arguments for singular chains (arc complements, covers), which feed the topological side of the forcing chain rather than the J-cost or φ-ladder algebra directly. It is pure scaffolding for those homology isomorphisms, not a physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.