bounds_of_mv
plain-language theorem explainer
With H₂(X)=0, a 1-cycle on the intersection of an open cover U∪V=X bounds on that intersection whenever its pushforwards bound separately on U and on V. Algebraic topologists running Mayer-Vietoris elementwise cite this as injectivity of the degree-1 MV map into H₁(U)⊕H₁(V). The proof kills the homology class by biproduct projections, MV exactness, and the vanishing of H₂(X).
Claim. Let $X$ be a space with open sets $U,V$ such that $U\cup V=X$, and assume $H_2(X)=0$. If $z$ is a singular $1$-cycle on $U\cap V$ whose images under the inclusions $U\cap V\hookrightarrow U$ and $U\cap V\hookrightarrow V$ are boundaries, then $z$ itself is a boundary on $U\cap V$.
background
The module builds elementwise Mayer-Vietoris calculus for singular chains on open covers, in service of acyclicity statements for arc complements. Degree-1 homology classes of 1-cycles are written via a class map: the class vanishes if and only if the cycle is a boundary. Pushforwards of cycles remain cycles, and the class map is natural under continuous maps.
The Mayer-Vietoris pairing sends a class on the intersection to the biproduct of the two pushforward classes (with a sign on the second factor). Exactness of the MV short complex at degree 1 says a class on $U\cap V$ lies in the kernel of that pairing precisely when it is the image of a class in $H_2(X)$. The ambient import is LinkingVanishingHighDim: high-dimensional linking and vanishing tools that need these elementary MV facts.
proof idea
Rewrite the goal as vanishing of the homology class of $z$ (class-equals-zero iff bounds). The two pushforward-bounds hypotheses become vanishing of the pushed classes on $U$ and on $V$.
Project the MV biproduct image of the class: the first factor equals the homology map of the $U$-inclusion (biproduct lift and naturality), hence is zero; the second equals the negative of the $V$-homology map and likewise vanishes. Biproduct extensionality gives that the paired class is zero.
Exactness of the degree-1 MV short complex then supplies a preimage in $H_2(X)$. The IsZero hypothesis on $H_2(X)$ forces that preimage to zero, so the class of $z$ is zero and $z$ bounds.
why it matters
Direct input to the bisection step: a 1-cycle of the complement of $KU=KP\cup KM$ whose pushforwards bound in both half-complements already bounds, once $H_2((KP\cap KM)^c)=0$. That bisection is the inductive engine for arc-complement acyclicity in this module.
In the Recognition foundation layer, clearing residual $H_1$ on complements underpins linking-vanishing arguments imported from LinkingVanishingHighDim. Those geometric facts support the dimensional side of the forcing chain (T8, $D=3$) and the eight-tick octave geometry, by ensuring no leftover 1-cycles survive after repeated closed-set bisection. The claim is fully proved; no scaffold remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.