mvSESdeg
plain-language theorem explainer
Degree-n Mayer–Vietoris short complex of ℤ-modules: C_n(U∩V) → C_n(U)⊕C_n(V) → C_n^{U,V}, with the standard (i_U,−i_V) and sum-of-inclusions maps. Anyone proving degreewise exactness of singular MV cites this object. It is a pure constructor: ShortComplex.mk from the two chain maps and the already-proved composition-zero identity.
Claim. For each degree $n\in\mathbb{N}$ and a pair of subspaces $U,V\subseteq X$, form the short complex of $\mathbb{Z}$-modules $$C_n(U\cap V)\xrightarrow{(i_{U*},\,-i_{V*})} C_n(U)\oplus C_n(V)\xrightarrow{j_U+j_V} C_n^{U,V},$$ where $i_U,i_V$ are the inclusions of the intersection, $j_U,j_V$ land in the small singular chains of the cover, and the composite is the zero map.
background
Singular Mayer–Vietoris compares the singular chain complexes of two subspaces $U,V$ of a space $X$ with those of the intersection and of a “small” complex $C_\bullet^{U,V}$ generated by simplices that land entirely in $U$ or entirely in $V$. The space-level inclusions $U\cap V\hookrightarrow U$ and $U\cap V\hookrightarrow V$ induce chain maps; at degree $n$ these become the two legs of a biproduct lift.
Dually, $uInc$ and $vInc$ are the degree-$n$ maps $C_n(U)\to C_n^{U,V}$ and $C_n(V)\to C_n^{U,V}$ that send a chain to its image in the small complex (via the generating inclusions of the cover). Their biproduct descent is the second arrow of the short complex.
The local setting is the Foundation development of singular homology with subdivision and prism operators already in place, so that the small complex is available as a concrete $\mathbb{Z}$-module in each degree. The identity that the composite of the two arrows vanishes is recorded as the degreewise vanishing lemma for the $\alpha\beta$ pair.
proof idea
Pure definitional constructor, not a proof. ShortComplex.mk is applied to three data: (1) the biproduct lift of chainMap of the intersection-into-$U$ inclusion and the negative of the intersection-into-$V$ inclusion; (2) the biproduct descent of the two small-complex inclusions uInc and vInc at degree $n$; (3) the already-established fact that those two maps compose to zero degreewise. No tactics run; the short-complex axioms are discharged by that vanishing lemma.
why it matters
This is the concrete algebraic object whose mono, epi, and exactness properties assemble into the degreewise short-exact Mayer–Vietoris sequence. Downstream, mvSESdeg_mono, mvSESdeg_epi, and mvSESdeg_exact each target one arrow or the kernel–image relation, and mvSESdeg_shortExact packages all three. The isomorphism mvSESdegIso then identifies this concrete short complex with the degree-$n$ evaluation of the homological-complex-level MV short complex, so long exact sequences in homology can be read off from the homology sequence of a short exact sequence of complexes.
In the Recognition Science foundation stack this sits under the singular-homology toolkit used to control topological invariants of the recognition complex (eight-tick octave, cover arguments on the discrete carrier). It does not itself invoke T5–T8 or the RCL; it is pure algebraic topology scaffolding that those geometric arguments rely on when they pass to homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.