mvSum_comp_mv
plain-language theorem explainer
In the singular Mayer–Vietoris sequence for an open cover X = U ∪ V, the sum map H_{n+1}(U) ⊕ H_{n+1}(V) → H_{n+1}(X) followed by the connecting map H_{n+1}(X) → H_n(U ∩ V) is the zero morphism. Anyone assembling exactness of MV at H_{n+1}(X) cites this. The proof reduces to the general fact that homology of the middle map of a short exact sequence of complexes composes to zero with the connecting homomorphism, after transporting across the small-complex isomorphism.
Claim. Let $U,V \subseteq X$ be open with $U \cup V = X$. For every $n \in \mathbb{N}$, the composite $$H_{n+1}(U) \oplus H_{n+1}(V) \xrightarrow{\mathrm{sum}} H_{n+1}(X) \xrightarrow{\delta} H_n(U \cap V)$$ is the zero map of abelian groups (equivalently, of $R$-modules in the ambient category).
background
The module builds the singular Mayer–Vietoris long exact sequence for an open cover of a space by two opens whose union is the whole space. Singular chains on $U$, $V$, $U \cap V$, and $X$ assemble into a short exact sequence of chain complexes (the MV SES), after restricting to the subcomplex of chains that are small relative to the cover and identifying that subcomplex with the full singular complex via the usual subdivision/prism argument.
The sum map is induced on homology by the pair of inclusions $U,V \hookrightarrow X$ (biproduct of the two homology groups). The connecting homomorphism $\delta$ is the boundary map of the long exact homology sequence of that SES. Exactness of MV is the statement that consecutive maps in $$\cdots \to H_{n+1}(U)\oplus H_{n+1}(V) \to H_{n+1}(X) \xrightarrow{\delta} H_n(U\cap V) \to H_n(U)\oplus H_n(V) \to \cdots$$ compose to zero and that kernels equal images.
This lemma is the first of those composition-to-zero facts: sum then $\delta$ vanishes. Its sibling records $\delta$ then the pair map vanishes; exactness at the middle term is stated separately.
proof idea
Start from the general SES identity: for the short exact sequence of complexes underlying MV, the homology map of the middle arrow composed with the connecting homomorphism $\delta$ of the LES is zero (comp_δ on mvSES_shortExact).
Rewrite the concrete sum map and connecting map in terms of that SES data plus the isomorphism identifying small singular homology with ordinary singular homology (mvSum_eq, mvδ, and the inverse of smallIso). After reassociating, the iso cancels by Iso.hom_inv_id_assoc, the SES identity applies, and the remaining composite is zero by comp_zero.
No new chain-level computation is done here; the work is transport of the abstract SES vanishing across the small-complex identification.
why it matters
Mayer–Vietoris is the standard computational engine for singular homology of spaces glued from opens. In the Recognition Science foundation stack this module supplies that engine in Lean, so later geometric and forcing arguments can quote homology exact sequences rather than rebuild them.
The lemma is one of the two composition-to-zero legs needed before exactness at $H_{n+1}(X)$ and at $H_n(U\cap V)$ can be stated. Together with the sibling vanishing $\delta$ then pair, it feeds the exactness theorem announced immediately below in the same file.
Within the broader RS chain (T0–T8 forcing, eight-tick structure, $D=3$), this is pure topological scaffolding: it does not itself force $\varphi$, $J$, or dimension, but it is part of the homology toolkit those geometric arguments may invoke when working with covers and gluings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.