smallU_f
plain-language theorem explainer
At each degree n, the chain map sending singular chains on the open set U into the (U,V)-small complex has component equal to the degreewise inclusion of chains. Anyone simplifying Mayer–Vietoris diagrams or naturality squares for the small-chain complex will cite this. The proof is pure definitional equality (rfl).
Claim. For every $n \in \mathbb{N}$, the degree-$n$ component of the chain map $C_*(U) \to C_*^{U,V}(X)$ (which treats every singular simplex supported in $U$ as $(U,V)$-small) equals the degreewise inclusion $C_n(U) \to C_n^{U,V}$.
background
This module builds a singular Mayer–Vietoris sequence from a cover by opens $U,V$ of a space $X$. The small-chain complex $C_*^{U,V}$ is generated by singular simplices that land entirely in $U$ or entirely in $V$; it sits between ordinary singular chains on the pieces and chains on $X$.
The degreewise inclusion $C_n(U) \to C_n^{U,V}$ is the map that sends a generator (a simplex in $U$) to the corresponding small generator. Assembling those degreewise maps with a boundary-commutation check yields a chain map $C_(U) \to C_^{U,V}$. The present lemma records that the degree-$n$ component of that assembled chain map is exactly the degreewise inclusion already defined.
Upstream, the chain map is constructed by setting its components to those inclusions and verifying they commute with the differential of the small complex; the inclusion itself is a sigma-desc over the index of opens covering $U$.
proof idea
One-line definitional wrapper. The chain map from chains on $U$ into the small complex is defined by taking its degree-$n$ component to be the degreewise inclusion, so the equality is rfl. Marked @[simp] so downstream rewrites unfold the chain-map component automatically.
why it matters
Needed to keep Mayer–Vietoris naturality and compatibility lemmas free of manual unfolding. The sole recorded consumer is the compatibility statement for the connecting map $\beta$ in the singular Mayer–Vietoris sequence (degreewise face of the MV connecting homomorphism). Without this simp fact, every diagram chase that compares the assembled chain map to the degreewise inclusion would re-expand the chain-map constructor by hand.
In the broader Recognition foundation stack this sits in the singular-homology toolkit used to control topological invariants of the discrete recognition complex (subdivision, prism operators, pair sequences). It is bookkeeping rather than a forcing-chain step (T0–T8), but it is the glue that lets those topological arguments stay diagrammatic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.