isZero_h1_inter
plain-language theorem explainer
Open cover U ∪ V = X with H₂(X) = 0 and H₁(U) = H₁(V) = 0 forces H₁(U ∩ V) = 0. Algebraic topologists working the high-dim linking-vanishing chain cite it as the MV middle step. The proof is a short term application of banked Mayer–Vietoris exactness at degree 1, with both flanking groups zero.
Claim. Let $X$ be a topological space and $U,V \subseteq X$ open with $U \cup V = X$. If the singular homology groups satisfy $H_2(X) = 0$, $H_1(U) = 0$, and $H_1(V) = 0$, then $H_1(U \cap V) = 0$.
background
The module develops high-dimensional linking vanishing: complements of arcs and closed sets in spaces with controlled singular homology. Singular homology $H_n$ is packaged as the abelian group Hgrp on a TopCat object; IsZero means the group is the zero object.
Mayer–Vietoris for an open cover $U \cup V = X$ yields a long exact sequence whose degree-1 segment runs (schematically) $H_2(X) \to H_1(U \cap V) \to H_1(U) \oplus H_1(V)$. The banked exactness lemma mv_exact₁ supplies that exact triangle in the category of abelian groups.
Local setting: once $H_2(X)$ and both $H_1(U)$, $H_1(V)$ vanish, exactness pins the middle term $H_1(U \cap V)$ to zero. That is the pure homological input needed before specializing to arc complements and two-arc unions.
proof idea
One short term proof. Instantiate banked Mayer–Vietoris exactness mv_exact₁ at degree 1 for the open cover $(U,V)$. The resulting exact triangle has middle object $H_1(U \cap V)$.
Apply the exact-triangle vanishing lemma isZero_X₂: the source map out of $H_2(X)$ is zero because hX2 makes that group zero (eq_of_src); the target into $H_1(U) \oplus H_1(V)$ is zero because the biproduct of two zero groups is zero (biprod_isZero_iff on hU1 and hV1, then eq_of_tgt). Exactness therefore forces the middle group to vanish.
why it matters
Direct input to isZero_h1_unionCompl, the abstract two-arc Mayer–Vietoris statement: two closed sets $K_+, K_-$ in $W$ with $H_2(W \setminus (K_+ \cap K_-)) = 0$ and $H_1$-acyclic individual complements have $H_1$-acyclic union complement. That parent theorem is the high-dim half of the linking-vanishing program (paired with the low-dim import).
In the Recognition foundation layer this is infrastructure, not a forcing-chain landmark (T5–T8). It clears the homological obstruction so that linking classes of arcs cannot survive in controlled complements, supporting later geometric rigidity arguments that feed the discrete recognition geometry. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.