smallU
plain-language theorem explainer
Packages the degreewise inclusions of singular chains on an open set U into the small-chains subcomplex of a cover (U,V) as a single chain map C_*(U) → C^{U,V}_*(X). Algebraic topologists building Mayer–Vietoris for singular homology cite it when assembling the MV connecting homomorphism. The construction is the chain-map structure on the already-defined degree maps, with differential compatibility from the degreewise commutation lemma.
Claim. There is a chain map $\mathrm{small}_U \colon C_*(U) \to C^{U,V}_*(X)$ whose component in degree $n$ is the inclusion of $n$-chains on $U$ into the small-chains group generated by singular simplices landing in $U$ or in $V$.
background
In the singular Mayer–Vietoris setup one works with an open cover $X = U \cup V$ and the small-chains subcomplex $C^{U,V}_*(X)$: the subcomplex of singular chains generated by simplices whose image lies entirely in $U$ or entirely in $V$ (Stage 1 of the module). Ordinary singular chains on the open set $U$ (viewed as a topological space) map into that subcomplex because every simplex of $U$ is automatically small for the cover.
The degree-$n$ piece of that inclusion is already defined as $u\mathrm{Inc}n \colon C_n(U) \to C_n^{U,V}$. The differential on the small-chains complex is the restriction of the singular boundary, recorded by the lemma that $(C^{U,V}*)\cdot d_{n+1,n}$ equals the small boundary operator. Compatibility of $u\mathrm{Inc}$ with boundaries is the separate lemma $u\mathrm{Inc}_\mathrm{comm}$.
This definition simply assembles those degreewise maps into a morphism of chain complexes $C_(U) \to C^{U,V}_(X)$.
proof idea
Definitional construction of a HomologicalComplex morphism. The degree-$n$ component is set to $u\mathrm{Inc},U,V,n$. Commutation with differentials is discharged by rewriting the small-complex differential via SSC_d and applying the already-proved degreewise identity uInc_comm.
why it matters
This is one of the two structure maps (the other is the analogous map from $C_*(V)$) that feed the Mayer–Vietoris chain-level diagram. Downstream it appears in the connecting map mvβ, in the compatibility lemmas homologyMap_mvβ_compat and mvβ_f_compat, and in the identity relating inclusions of $U$ and $V$ after composing with small-chain maps (sChainMap_inclU_smallU_eq). Without packaging $u\mathrm{Inc}$ as a genuine chain map, the long exact sequence of the cover cannot be stated in the HomologicalComplex language used by the rest of the foundation stack.
In the broader Recognition Science forcing chain this sits in the singular-homology infrastructure that underwrites topological invariants of the recognition complex (eight-tick octave, $D=3$), not in the J-cost or constants layer itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.