isZero_of_isZero_inter
plain-language theorem explainer
Vanishing of singular homology is transported one degree upward across the Mayer–Vietoris connecting map when both cover pieces are contractible. If an open cover X = U ∪ V has contractible U and V and H_{n+1}(U ∩ V; ℤ) = 0, then H_{n+2}(X; ℤ) = 0. Sphere and cell-homology arguments that reduce via MV covers cite this. Proof is IsZero transport along the connecting isomorphism from isIso_mvδ_of_contractible.
Claim. Let $X$ be a space and $U,V \subseteq X$ open with $U \cup V = X$. Assume $U$ and $V$ are contractible. If the singular homology $H_{n+1}(U \cap V;\mathbb{Z})$ is the zero module, then $H_{n+2}(X;\mathbb{Z})$ is the zero module.
background
This lives in the singular-sphere foundation layer, which builds integer singular homology of topological spaces from the singular chain complex and Mayer–Vietoris machinery imported from SingularMayerVietoris and related subdivision/prism modules.
Hgrp Y k is the degree-$k$ singular homology of a space $Y$ with $\mathbb{Z}$ coefficients, i.e. the homology of the singular chain complex of $Y$. The Mayer–Vietoris connecting homomorphism mvδ relates $H_{\bullet}(U \cap V)$ to $H_{\bullet+1}(X)$ for an open cover $X = U \cup V$.
When both pieces $U$ and $V$ are contractible, the long exact MV sequence collapses in a controlled way: the connecting map in the relevant degrees becomes an isomorphism (recorded by isIso_mvδ_of_contractible). Vanishing on the intersection then forces vanishing one degree higher on $X$.
proof idea
Short term-mode argument. First install the instance that the Mayer–Vietoris connecting map mvδ in degree $n+1$ is an isomorphism, via isIso_mvδ_of_contractible applied to the open cover hypotheses and the contractibility instances on $U$ and $V$. Then transport the given IsZero hypothesis on $H_{n+1}(U \cap V)$ across that isomorphism by IsZero.of_iso applied to asIso (mvδ ...), yielding IsZero on $H_{n+2}(X)$.
why it matters
In the Recognition Science foundation stack this is a local vanishing lemma for singular homology under contractible open covers. Sphere homology (and related cell or suspension computations) routinely reduces to intersection data via Mayer–Vietoris; this lemma packages the exact degree shift of vanishing once the connecting map is known to be an iso.
It sits beside the module’s homology abbreviations and the contractible-cover iso for mvδ, feeding any later argument that needs $H_{k}(X)=0$ from $H_{k-1}(U \cap V)=0$. No downstream consumers are wired yet in the graph, so it is presently a reusable MV vanishing step rather than a named link in the T0–T8 forcing chain. It does not itself force dimension, $\varphi$, or the eight-tick octave; it only supplies homological vanishing infrastructure those geometric arguments may call.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.