mv
plain-language theorem explainer
Left arrow of the singular Mayer–Vietoris short complex: chains on U∩V map to the biproduct of chains on U and on V by x ↦ (i_*x, −j_*x). Anyone assembling the MV exact sequence for open covers of a space X cites this map. The body is a one-line biprod.lift of the two inclusion-induced singular chain maps, with a sign on the second leg.
Claim. For open sets $U,V \subseteq X$, the chain map $\alpha \colon C_\bullet(U \cap V) \to C_\bullet(U) \oplus C_\bullet(V)$ is defined by $x \mapsto (i_* x,\, -j_* x)$, where $i \colon U \cap V \hookrightarrow U$ and $j \colon U \cap V \hookrightarrow V$ are the inclusions and $i_*, j_*$ are the induced maps on singular chain complexes.
background
The module builds the singular Mayer–Vietoris sequence for a pair of open sets $U,V$ in a topological space $X$. Singular chain complexes $SC(Y)$ are the usual free abelian complexes on continuous simplices into $Y$, viewed in the category of chain complexes of modules so that Mathlib biproducts and homology sequences apply.
The two inclusions of the intersection $U \cap V$ into $U$ and into $V$ induce chain maps (via the sibling sChainMap construction on continuous maps). The left MV map packages those two induced maps into a single arrow out of $SC(U \cap V)$ into the biproduct $SC(U) \boxplus SC(V)$. The companion right map (mvβ) sends a pair of chains on $U$ and $V$ into the small subcomplex of chains on $X$ supported in $U \cup V$.
Together $\alpha$ and $\beta$ form the short complex whose homology is the Mayer–Vietoris long exact sequence once exactness is established.
proof idea
Pure definition, not a proved lemma. The arrow is biprod.lift applied to the pair (sChainMap (mvInclU U V), −(sChainMap (mvInclV U V))). The first component is the chain map induced by the inclusion $U \cap V \hookrightarrow U$; the second is the negative of the chain map induced by $U \cap V \hookrightarrow V$. Biproduct universal property supplies the unique map into the biproduct with those two components.
why it matters
This is the standard left leg of the singular Mayer–Vietoris short complex inside the Foundation layer. Recognition Science needs controlled singular homology on covers (eight-tick discrete structure, prism and subdivision operators live in sibling modules) so that topological invariants of the recognition complex can be computed by gluing local data on $U$ and $V$.
The definition sits between the inclusion and small-subcomplex machinery (mvInclU, mvInclV, smallU, smallV, SSC) and any later exactness or long-exact-sequence theorems that will quote $\alpha$ and $\beta$ as the short-complex differentials. No forcing-chain landmark (T5–T8) is settled here; the contribution is infrastructural homology for the geometric side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.