mvSum
plain-language theorem explainer
The Mayer-Vietoris sum sends a pair of classes in H_n(U) and H_n(V) to the sum of their images in H_n(X) under the two subspace inclusions. Anyone assembling the MV long exact sequence cites it as the middle homology arrow after the short exact sequence of chain complexes. The body is the biproduct desc of the two induced homology maps of the inclusions.
Claim. For subspaces $U,V \subseteq X$ and each degree $n$, the Mayer-Vietoris sum is the morphism $H_n(U)\oplus H_n(V)\to H_n(X)$ of singular homology (of the small chain complexes) given on classes by $([a],[b])\mapsto [k_*a]+[l_*b]$, where $k:U\hookrightarrow X$ and $l:V\hookrightarrow X$ are the subspace inclusions.
background
This module builds the Mayer-Vietoris sequence in singular homology for a cover $X=U\cup V$, working throughout with the small singular chain complex SC (from SingularPrism) rather than the unrestricted singular complex. Homology is the usual homology of that chain complex in ModuleCat.
The subspace inclusion of a set $S\subseteq X$ is the continuous map subInc (SingularPair): the subtype projection $S\to X$ as a morphism of TopCat. A continuous map of spaces induces a chain map of small complexes via sChainMap, and then a map on homology via homologyMap.
The biproduct $A\oplus B$ in an additive category comes with the universal map-out biprod.desc f g : A\oplus B\to C determined by a pair of arrows $f:A\to C$ and $g:B\to C$. That is exactly the algebraic shape of the classical MV sum $([a],[b])\mapsto k_[a]+l_[b]$.
proof idea
Pure definition, not a proof. Apply biprod.desc to the pair of homology maps
homologyMap (sChainMap (subInc X U)) n and
homologyMap (sChainMap (subInc X V)) n.
Each leg is the map on $H_n$ induced by the corresponding subspace inclusion; the biproduct desc is the unique arrow out of $H_n(U)\oplus H_n(V)$ with those two components. No lemmas are invoked beyond the constructors of biproducts and homology maps.
why it matters
This is the middle arrow of the Mayer-Vietoris triangle at the homology level. Downstream it is the right factor in mvPair_comp_mvSum (the composition $H_n(U\cap V)\to H_n(U)\oplus H_n(V)\to H_n(X)$ is zero), and it appears in the exactness lemmas mv_exact₂ and mv_exact₃. The degree-zero tail theorem mvSum_epi_zero proves it is an epimorphism when $U\cup V=X$ with $U,V$ open, so the MV sequence ends $\cdots\to H_0(U)\oplus H_0(V)\to H_0(X)\to 0$. The sanity lock mvSum_epi_of_left_univ records the same when $U=X$. The rewrite form mvSum_eq identifies it with the homology of the chain-level $\beta$ map after the small-chains and biproduct isomorphisms. In the RS foundation stack this is ordinary algebraic topology scaffolding: the MV LES is the computational engine for homology of glued spaces, not a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.