sChainMap_inclU_smallU_eq
plain-language theorem explainer
On the singular chain complexes, the two composite maps from C_*(U ∩ V) into the small-chain complex C_*^{U,V} agree: include into U then take the U-small map, or include into V then take the V-small map. Anyone building the Mayer–Vietoris chain maps α and β cites this equality. The proof is degreewise reduction via HomologicalComplex.hom_ext to the already-proved generator identity.
Claim. For open sets $U,V \subseteq X$, the composites of singular chain maps $$C_*(U \cap V) \xrightarrow{i_*} C_*(U) \xrightarrow{\mathrm{small}_U} C_*^{U,V}$$ and $$C_*(U \cap V) \xrightarrow{j_*} C_*(V) \xrightarrow{\mathrm{small}_V} C_*^{U,V}$$ are equal as morphisms of homological complexes.
background
The module builds the singular Mayer–Vietoris short exact sequence at the chain level. Open sets $U,V \subseteq X$ give inclusions $U \cap V \hookrightarrow U$ and $U \cap V \hookrightarrow V$; their induced singular chain maps are written $i_$ and $j_$. The target $C_*^{U,V}$ is the complex of singular chains that are small relative to the cover ${U,V}$ (each simplex lands in $U$ or in $V$).
The maps $\mathrm{small}_U$ and $\mathrm{small}_V$ send ordinary chains on $U$ (resp. $V$) into that small complex by viewing each generator as already $U$-small (resp. $V$-small). The key prior fact is the degreewise identity: both routes $C_n(U \cap V) \to C_n^{U,V}$ send a simplex of the intersection to the same small generator. That is the content of the upstream lemma that both composites through $U$ and through $V$ agree on each degree.
proof idea
Apply HomologicalComplex.hom_ext to reduce equality of chain-complex morphisms to equality in each degree $n$. In degree $n$, invoke the already-proved generator-level identity inclU_uInc_eq_inclV_vInc, which states that
$$\mathrm{chainMap}(i)_n \circ u\mathrm{Inc}_n = \mathrm{chainMap}(j)_n \circ v\mathrm{Inc}_n.$$
The small maps are assembled from those inclusions of generators, so the degreewise equalities glue to the complex-level statement. No further diagram chase is needed.
why it matters
This is the chain-complex form of the commuting square that makes the left Mayer–Vietoris map well-defined. Downstream it is used by mvα_comp_mvβ, which checks that the composite of the two MV chain maps vanishes (the first exactness relation in the SES). Without agreement of the two routes from $C_(U \cap V)$ into $C_^{U,V}$, the difference map $x \mapsto (i_*x, -j_*x)$ would not land in a single coherent target.
In the Recognition foundation stack this sits in the singular-homology toolkit used to control topological invariants of recognition spaces (covers, subdivisions, prism operators). It is pure algebraic topology scaffolding: no direct appeal to J-cost, $\varphi$, or the T0–T8 forcing chain, but it underwrites later geometric arguments that need a working MV sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.