mvSum_eq
plain-language theorem explainer
The Mayer-Vietoris sum map on homology equals the composite of the inverse biproduct isomorphism with the homology maps of the chain-level β map and the small-chain inclusion. Algebraic topologists cite it when matching the abstract sum H_n(U)⊞H_n(V)→H_n(X) to its chain-level presentation. Proof is a one-line appeal to the β-compatibility lemma, taken symmetrically.
Claim. For every degree $n\in\mathbb{N}$, the Mayer-Vietoris sum map $H_n(U)\boxplus H_n(V)\to H_n(X)$ equals the composite of the inverse of the homology biproduct isomorphism $H_n(C_*(U)\boxplus C_*(V))\cong H_n(U)\boxplus H_n(V)$ with the homology maps induced by the chain-level Mayer-Vietoris $\beta$ map and the inclusion of small singular chains into $C_*(X)$.
background
This module builds the singular Mayer-Vietoris sequence for an open cover $X=U\cup V$. The sum map sends a biproduct class $([a],[b])$ to $[k_*a]+[l_*b]$, where $k:U\hookrightarrow X$ and $l:V\hookrightarrow X$ are the subspace inclusions; that is the abstract target of the present identification.
Homology is additive on biproducts of chain complexes: there is a canonical isomorphism $H_n(C_(U)\boxplus C_(V))\cong H_n(U)\boxplus H_n(V)$. The chain-level $\beta$ map and the inclusion of the small-chain subcomplex (simplices subordinate to the cover, via the subdivision apparatus imported here) induce maps on homology whose composite, after the inverse biproduct iso, is claimed to recover the sum.
The local setting is classical singular homology in an abelian category of modules, with Mathlib homology functors and biproducts; the Recognition Science layer only supplies the ambient topological pair and the small-chain filtration.
proof idea
One-line term proof: the claim is exactly the symmetric form of the already-proved compatibility lemma that relates the homology of the chain-level $\beta$ map to the sum map through the biproduct isomorphism and the small-chain inclusion. No further rewriting or case analysis is required.
why it matters
This identification is the bridge used by every exactness check that mentions the sum map. Downstream, the composition-to-zero lemma rewrites both the pair map and the sum map into chain-level form, cancels the biproduct iso, and reduces exactness at $H_n(U)\boxplus H_n(V)$ to the chain-level relation $\alpha\circ\beta=0$. The same rewrite feeds the two exactness lemmas in the long sequence, the composition of sum with the connecting map, and the degree-zero epimorphism theorem that closes the MV sequence as $\cdots\to H_0(U)\boxplus H_0(V)\to H_0(X)\to 0$.
In the Recognition foundation stack this is pure topological scaffolding: it underwrites singular-homology computations on covers that appear in later geometric and forcing arguments, without itself invoking J-cost, $\phi$, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.