smallV_f
plain-language theorem explainer
The degree-n face of the chain map sending singular chains on V into the (U,V)-small chain complex is exactly the degree-n inclusion of V-chains. Homological algebraists building Mayer–Vietoris for singular chains cite this as the unpacking identity for that map. The proof is pure definitional equality (rfl).
Claim. For every $n \in \mathbb{N}$, the degree-$n$ component of the chain map $C_*(V) \to C_*^{U,V}(X)$ equals the degree-$n$ inclusion $C_n(V) \to C_n^{U,V}(X)$ of $V$-chains into the small-chain groups for the cover $(U,V)$.
background
In the singular Mayer–Vietoris setup, one works with the subcomplex of chains that are small relative to an open cover $(U,V)$ of a space $X$. The object $C_*^{U,V}(X)$ collects those small singular chains; ordinary singular chains on the open set $V$ land inside it because every simplex supported in $V$ is automatically small.
The chain map in question is the inclusion $C_(V) \to C_^{U,V}(X)$ whose degree-$n$ arrow is built by sending each generator simplex of $V$ along the small-chain generator map. That degree-$n$ arrow is the inclusion of $V$-chains into the small-chain group at degree $n$. The present lemma simply records that the chain-map component equals that inclusion.
proof idea
One-line definitional wrapper. The chain map is defined by setting its degree-$n$ component equal to the $V$-inclusion into small chains, so the equality is rfl. Marked @[simp] so downstream rewrites unfold the component automatically.
why it matters
Local plumbing inside the singular Mayer–Vietoris module. The sole recorded consumer is the compatibility lemma for the Mayer–Vietoris connecting map’s degree-$n$ face, which needs the chain-map component exposed as the $V$-inclusion. Without this simp fact, every later identity that compares boundaries or biproduct projections against the small-chain inclusion would have to unfold the chain-map definition by hand. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is infrastructure for the singular-homology side of the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.