mv_middle_exact
plain-language theorem explainer
Middle exactness for the Mayer–Vietoris chain sequence: if singular n-chains a on U and b on V cancel after inclusion into the ambient small complex, they come from a single n-chain on U ∩ V. Algebraic topologists building the MV long exact sequence cite this. The proof builds the preimage by lifting supp(a) into the intersection, then recovers the V-component by injectivity of the V-inclusion.
Claim. Let $U,V \subseteq X$ be open (or admissible) sets and $n \in \mathbb{N}$. Write $C_n(-)$ for the singular chain group in degree $n$. If $a \in C_n(U)$ and $b \in C_n(V)$ satisfy $i_U(a) + i_V(b) = 0$ in the ambient small complex, then there exists $x \in C_n(U \cap V)$ with $j_U(x) = a$ and $j_V(x) = -b$, where $j_U,j_V$ are the inclusions of the intersection into $U$ and $V$.
background
This module builds a singular Mayer–Vietoris short exact sequence of chain complexes for a cover ${U,V}$ of a space $X$. Chains live in the free abelian groups $C_n(Y) = C_{\mathrm{grp}}(\mathrm{TopCat.of}, Y, n)$ generated by singular $n$-simplices; inclusions of subspaces induce chain maps by postcomposition on simplices.
The maps $uInc$ and $vInc$ push chains from $U$ and $V$ into a common “small” ambient complex; $mvInclU$ and $mvInclV$ are the inclusions of $U \cap V$ into $U$ and $V$. Exactness in the middle degree is the statement that $\ker(i_U \oplus i_V) = \mathrm{im}(j_U, -j_V)$ on chains.
Coordinate and support machinery (coordAt, suppOf, unitOf, liftIdx, pushIdx) treats chains as finite formal sums of basis simplices, so cancellation of images can be read simplex-by-simplex.
proof idea
Classical proof. First show every simplex in $\mathrm{supp}(a)$ lands in $U \cap V$: if a support index of $a$ had no matching $V$-index, then at the corresponding ambient coordinate one would have $\mathrm{coord}(i_U(a)) = \mathrm{coord}(a) \neq 0$ while $\mathrm{coord}(i_V(b)) = 0$, contradicting $i_U(a)+i_V(b)=0$.
Define $x$ as the sum over $\mathrm{supp}(a)$ of the same coefficients on the lifted intersection simplices. Termwise, $j_U$ sends each lifted generator back to the original $U$-simplex, so $j_U(x)=a$ after reassembling the support sum.
For the $V$-side, the commuting square $i_U \circ j_U = i_V \circ j_V$ gives $i_V(j_V(x)) = i_U(a)$. Injectivity of $i_V$ plus $i_U(a)+i_V(b)=0$ forces $j_V(x)=-b$.
why it matters
This is the nontrivial kernel–image step for Mayer–Vietoris exactness on singular chains. Downstream, mvSESdeg_exact packages it into exactness of the degree-$n$ short complex $(C_n(U\cap V) \to C_n(U)\oplus C_n(V) \to C_n^{\mathrm{small}})$, which is the algebraic input to the long exact MV sequence in homology.
In the Recognition foundation stack, singular MV is infrastructure for gluing local recognition data on overlapping charts (subdivision, prisms, pairs) rather than a direct T0–T8 forcing step. It sits under the same geometric layer as the eight-tick and $D=3$ arguments: once local chain-level identities glue, global topological invariants of the recognition complex become well-defined.
No scaffolding remains here; the lemma is fully proved and closes the middle exactness obligation for the SES.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.