mvSum_epi_zero
plain-language theorem explainer
When open sets U and V cover X, the degree-0 Mayer–Vietoris sum H_0(U)⊕H_0(V)→H_0(X) is an epimorphism, so the MV sequence ends …→H_0(U)⊕H_0(V)→H_0(X)→0. Cite this for exactness of the singular MV tail. The proof lifts degreewise surjectivity of β through homology, then composes with the small-chain isomorphism at degree 0.
Claim. Let $U,V\subseteq X$ be open with $U\cup V=X$. Then the Mayer–Vietoris sum map $H_0(U)\oplus H_0(V)\to H_0(X)$ is an epimorphism in the category of modules (equivalently, surjective on $H_0$).
background
This lives in the singular Mayer–Vietoris development for Recognition Science foundations: singular chains on open covers, with a “small” subcomplex of chains supported in U or V, and the usual MV short exact sequence of chain complexes.
The sum map at homology is induced by the two inclusions into X. Degreewise, the β component of the MV SES is already epic (from the short-exactness package at each degree). Separately, the inclusion of small chains into ordinary singular chains induces an isomorphism on homology in every degree when U and V are open and cover X (excision/small-chain theorem).
At degree 0 the geometric content is connectivity of path-components: every 0-cycle on X is homologous to a combination of cycles supported in U and in V. The theorem isolates that H_0 tail so the long exact MV sequence can be closed with a zero on the right.
proof idea
Two instances, then rewrite.
First, homologyMap(mvβ) at degree 0 is epic: apply epi_homologyMap_chain_zero to the β chain map. The side condition is solved by degreewise exactness: (mvSES_degreewise_shortExact U V 0).epi_g gives that β at chain level 0 is epic, hence surjective in ModuleCat; pick a preimage x of y and witness the homology lift as ⟨x, 0⟩ using map_zero and add_zero.
Second, homologyMap(smallι) at 0 is an isomorphism by smallι_isIso_homologyMap under the open-cover hypotheses.
Rewrite the sum map via mvSum_eq (sum factors through small chains and β). With both factors epic (iso ⇒ epi), infer_instance closes Epi (mvSum U V 0).
why it matters
Closes the degree-0 end of the singular Mayer–Vietoris long exact sequence in this foundation module: without an epic sum map, one cannot write …→H_0(U)⊕H_0(V)→H_0(X)→0. That tail is the algebraic statement that path-components of X are generated by those of U and V under an open cover.
No downstream consumers are wired yet in the graph (used_by empty), so this is presently a leaf lemma inside SingularMayerVietoris, sitting beside the small-chain and SES scaffolding (smallι, mvβ, degreewise short exactness). In the broader RS foundation stack it is topological infrastructure rather than a forcing-chain (T0–T8) step: it supports later singular-homology arguments that may feed recognition/covering constructions, not the J-cost or φ-ladder directly.
The adjacent sanity-lock comment records the special case U=univ, where the first summand alone already gives the epi via the identity cover.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.