smallU_comp_small

The module builds a singular Mayer–Vietoris package: chain complexes of singular simplices that are small relative to a cover ${U,V}$, together with the usual inclusions, retractions, and boundary maps. Sibling structure includes the small subcomplex, its generators and inclusion into ordinary singular chains, a retraction, and the induced boundary.

Here $\mathrm{smallU}$ and the small inclusion are the two legs that relate the small complex on the cover to the complex generated by chains supported in $U$. The right-hand side is the chain map of the pair-level sub-inclusion of $U$ into $X$, so the lemma is a compatibility of the small-cover factorization with ordinary singular inclusion.

No external upstream lemmas are recorded on the depends edge; the only named ingredient is the degreewise identity that multiplies the two component maps in each homological degree.

Term-mode proof. Apply homological-complex extensionality to reduce equality of chain maps to equality in each degree $n$. In degree $n$, invoke the component identity that the $U$-inclusion composed with the small inclusion recovers the degree-$n$ piece of the sub-inclusion chain map. No further rewriting or diagram chase.

Inside SingularMayerVietoris this identity is bookkeeping that lets the small-cover complex sit over the ordinary singular complex of $U$ without introducing a second, incompatible inclusion. Parent consumers are not yet wired on the used-by edge, so the lemma is presently a local coherence step rather than a cited input to a named global theorem.

In the broader Recognition foundation stack, singular Mayer–Vietoris supplies the homological language later used for cover-based gluing and dimension-forcing arguments (the T8 $D=3$ step sits downstream of cover and nerve constructions). The lemma itself does not touch J-cost, the Recognition Composition Law, or the phi ladder; it only keeps the chain-level diagrams commutative so those later steps can quote a single, unambiguous inclusion of $U$.