mono_mvPair_zero
plain-language theorem explainer
When the intersection of two open sets is path-connected, the degree-0 Mayer–Vietoris pair map into H_0(U) ⊕ H_0(V) is a monomorphism. Algebraic topologists cite this to control low-degree exactness on covers. The proof factors the pair map through the first biproduct projection, identifies that factor with the induced inclusion map on H_0, and uses path-connectedness to make the augmentation iso so mono-cancellation applies.
Claim. Let $U,V \subseteq X$. If $U \cap V$ is path-connected, then the Mayer–Vietoris pair map $H_0(U \cap V) \to H_0(U) \oplus H_0(V)$ is a monomorphism.
background
This lives in the singular-homology foundation for spheres and covers. The Mayer–Vietoris pair map in degree $n$ is the map $H_n(U \cap V) \to H_n(U) \oplus H_n(V)$ induced by the two inclusions of the intersection; it is the first nontrivial arrow of the MV long exact sequence once the cover $U \cup V = X$ is fixed.
Path-connectedness of a space forces the augmentation $H_0 \to \mathbb{Z}$ (or the corresponding group object augH on the universal open) to be an isomorphism. The space-level inclusion $U \cap V \hookrightarrow U$ induces a chain map whose homology in degree 0 is the first component of the pair map. Upstream, mvInclU is exactly that inclusion, and sChainMap turns continuous maps of spaces into singular chain maps.
Local setting: singular chains on topological spaces in TopCat, with biproducts of homology groups and mono/iso instances in the abelian category of groups.
proof idea
Path-connectedness of $U \cap V$ supplies IsIso for the augmentation on $H_0(U \cap V)$. Rewrite the composite of the induced inclusion map on $H_0$ with the augmentation on $U$ via homologyMap_augH; that composite is mono, so by mono-cancellation the inclusion map on $H_0$ itself is mono.
The pair map composed with the first biproduct projection equals that inclusion map (biprod.lift_fst). Hence the composite pair-then-fst is mono, and mono-cancellation against biprod.fst yields mono of the pair map in degree 0.
why it matters
Feeds directly into isZero_h1: if $U$ and $V$ have vanishing $H_1$ and $U \cap V$ is path-connected, then $H_1(X)=0$. That low-degree vanishing is the first step toward identifying singular homology of spheres and related covers in the Recognition foundation stack (singular prism, pair, subdivision, Mayer–Vietoris).
In the broader RS chain this is scaffolding for topological invariants that later interface with the eight-tick octave and $D=3$ forcing, not a physics claim itself. It closes the mono half of the degree-0 MV arrow so exactness arguments can kill $H_1$ on the union.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.