mvSES
plain-language theorem explainer
Packages the two Mayer–Vietoris chain maps into a single short complex of singular chain complexes: intersection chains into the biproduct of the two opens, then into the relative cover complex. Algebraic topologists cite it as the Stage-3 object whose short exactness yields the MV long exact sequence. Construction is a one-line ShortComplex.mk from the two maps and their composition-zero lemma.
Claim. The Mayer–Vietoris short complex is the short complex of chain complexes of $\mathbb{Z}$-modules $$0 \to C_*(U \cap V) \xrightarrow{\alpha} C_*(U) \oplus C_*(V) \xrightarrow{\beta} C^{U,V}_*(X) \to 0,$$ assembled from the inclusion-induced map $\alpha$ into the biproduct and the difference map $\beta$ into the $(U,V)$-cover complex, with $\beta \circ \alpha = 0$.
background
Singular Mayer–Vietoris in this module is built degreewise on free $\mathbb{Z}$-modules of singular simplices, then lifted to chain complexes. The two opens $U,V \subseteq X$ determine three singular chain complexes: $C_(U \cap V)$, the biproduct $C_(U) \oplus C_(V)$, and the cover complex $C^{U,V}_(X)$ generated by simplices that land in $U$ or in $V$.
The first arrow is the pair of inclusions of the intersection into each open (with a sign on one summand). The second is the biproduct-descended pair of inclusions into the cover complex. Their composite vanishes by the usual cancellation of the two paths through $U$ and $V$.
Stage 3 of the module records this data as a Mathlib ShortComplex in the category of chain complexes of ModuleCat ℤ, so that short-exactness and the homology long exact sequence can be invoked from the homological-algebra library rather than rebuilt by hand.
proof idea
One-line definitional wrapper: ShortComplex.mk applied to the already-constructed chain maps mvα U V and mvβ U V together with the composition identity mvα_comp_mvβ U V. No further algebra is performed at this site; the zero-composite and the maps themselves are upstream.
why it matters
This is the Stage-3 carrier object for the singular Mayer–Vietoris sequence in the Foundation layer. Downstream, mvSESdegIso identifies each degree with the concrete module short complex; mvSES_degreewise_shortExact transfers degreewise exactness across that iso; and mvSES_shortExact concludes that the whole complex of chain complexes is short exact, with no openness or covering hypotheses required beyond the singular-cover construction.
That short exactness is the algebraic input to the long exact Mayer–Vietoris sequence in homology, which the monolith uses when gluing local recognition data on overlapping regions. In the broader forcing picture it sits in the homological toolkit that supports dimension and covering arguments (T7–T8 territory), rather than in the J-cost or φ-ladder core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.