isZero_h1
plain-language theorem explainer
If a space is the union of two open sets each with vanishing first singular homology, and their intersection is path-connected, then the whole space has vanishing H₁. Algebraic topologists cite this as the low-degree Mayer–Vietoris vanishing lemma for covers. The proof forces the degree-0 connecting map to be both mono and zero, hence H₁ of the total space is the zero module.
Claim. Let $X$ be a topological space covered by open sets $U$ and $V$ with $U \cup V = X$. Suppose $U \cap V$ is path-connected, and the first singular homology groups $H_1(U;\mathbb{Z})$ and $H_1(V;\mathbb{Z})$ both vanish. Then $H_1(X;\mathbb{Z}) = 0$.
background
The ambient module develops singular homology of spaces in the Recognition foundation stack, with an eye toward spheres and prism subdivisions. The abbreviation Hgrp is the degree-$n$ singular homology of a TopCat object with integer coefficients: the homology of the singular chain complex.
Mayer–Vietoris supplies the exact sequence relating $H_(U\cap V)$, $H_(U)\oplus H_(V)$, and $H_(X)$ for an open cover $X=U\cup V$. The pair map sends a class in $H_n(U\cap V)$ to $([i_*c],-[j_c])$ via the two inclusions; the connecting homomorphism $\delta$ lands in $H_{n+1}(X)$. Exactness at the biproduct and at $H_(X)$ is packaged as mv_exact₃ and the composition identity $\delta\circ\mathrm{mvPair}=0$.
Path-connectedness of the intersection controls $H_0(U\cap V)$: it makes the degree-0 pair map mono, which is the low-degree input that turns vanishing of $H_1(U)$ and $H_1(V)$ into vanishing of $H_1(X)$.
proof idea
Work in the Mayer–Vietoris sequence at $n=0$. Exactness (mv_exact₃) plus the hypothesis that both summands $H_1(U)$ and $H_1(V)$ are zero modules makes the connecting map $\delta:H_0(U\cap V)\to H_1(X)$ a monomorphism (the outgoing arrow from a zero biproduct is mono).
Separately, path-connectedness of $U\cap V$ yields that the degree-0 pair map is mono. The standard MV identity $\delta\circ\mathrm{mvPair}=0$ then forces $\delta=0$ by the lemma that a composite zero with mono first factor implies the second factor is zero.
A monomorphism that is the zero morphism has zero codomain, so $H_1(X)=0$ via IsZero.of_mono_eq_zero.
why it matters
This is the workhorse low-degree vanishing step inside Foundation.SingularSphere. Its sole recorded consumer is isZero_h1_of_contractible, which specialises the hypotheses to contractible open pieces (hence automatically $H_1(U)=H_1(V)=0$) with path-connected intersection, concluding $H_1(X)=0$.
In the Recognition stack, singular homology of spheres and related covers underpins the topological side of the forcing chain: eight-tick octave structure (T7) and three spatial dimensions (T8) ultimately need clean control of low-degree homology of spherical and prismatic models. The lemma closes the $H_1$ case of the open-cover vanishing argument without assuming full contractibility of $X$ itself, only of the pieces (or, more weakly, vanishing of their $H_1$).
It is fully proved (no sorry), so it is available as a black-box input to any later sphere or subdivision computation that reduces to a two-set cover.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.