mv_exact
plain-language theorem explainer
Exactness of Mayer-Vietoris at intersection homology: for open U,V covering X, the sequence H_{n+1}(X) → H_n(U∩V) → H_n(U)⊕H_n(V) is exact in every degree. Algebraic topologists building singular homology, and any RS argument that splits a space into two opens, would cite it. Proof transfers exactness from the short exact sequence of chain complexes along a short-complex isomorphism built from the small-chains and biproduct homology isos.
Claim. Let $U,V$ be open subsets of a space $X$ with $U\cup V=X$. For every $n\in\mathbb{N}$, the short complex $H_{n+1}(X)\xrightarrow{\delta} H_n(U\cap V)\xrightarrow{\alpha} H_n(U)\oplus H_n(V)$ is exact.
background
Singular Mayer-Vietoris computes the singular homology of a space from an open cover ${U,V}$ with $U\cup V=X$. The connecting map $\delta$ and the pair map into the biproduct $H_n(U)\oplus H_n(V)$ form one vertex of the long exact sequence.
The module works in the category of chain complexes of $R$-modules. A short exact sequence of complexes (the Mayer-Vietoris SES of singular chains, restricted to chains small relative to ${U,V}$) induces a long exact sequence in homology. The small-chains complex is quasi-isomorphic to ordinary singular chains once $U$ and $V$ are open and cover $X$; biproducts of complexes compute as degreewise direct sums, so homology of a biproduct is the biproduct of homologies.
Local setting: Foundation-layer singular homology infrastructure (prisms, pairs, subdivision), imported from Mathlib homology sequences and ModuleCat biproducts.
proof idea
One transfers exactness rather than chasing cycles. Apply ShortComplex.exact_of_iso to the degree-$(n+1,n)$ connecting exactness statement from the short-exact Mayer-Vietoris SES of chain complexes (homology_exact₁ on mvSES_shortExact).
The mediating short-complex isomorphism is assembled by ShortComplex.isoMk from three pieces: the small-chains homology iso in degree $n+1$, the identity on the middle term, and the biproduct homology iso in degree $n$. The two commuting squares are discharged by unfolding the definitions of the connecting map and the pair map and cancelling inverse/identity compositions (Iso.hom_inv_id_assoc, comp_id, id_comp).
why it matters
This is the first of the three exactness vertices that assemble the full Mayer-Vietoris long exact sequence in singular homology (exactness at $H_n(U\cap V)$, then at the biproduct, then at $H_{n+1}(X)$). Without it the connecting homomorphism cannot be used to relate homology of $X$ to homology of the pieces and their intersection.
In the Recognition Science Foundation layer it supplies the standard topological splitting tool: any later argument that decomposes a recognition space, a cover, or a configuration into two opens can quote this exactness rather than rebuild cycle-boundary bookkeeping. It sits downstream of the small-chains quasi-isomorphism and the SES of chain complexes, and upstream of the degree-zero surjectivity tail and any global MV package theorem. No direct link to the T0-T8 forcing chain; pure homology infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.