vInc_comp_sInc
plain-language theorem explainer
The composite of the V-leg map into small chains with the small-to-singular inclusion equals the ordinary singular chain map of the subspace inclusion V ↪ X, in every degree. Anyone building Mayer–Vietoris maps, injectivity of the V-inclusion, or boundary-commutation for the cover will cite it. The proof is generator-wise: Sigma.hom_ext plus the generator identities for vInc and sInc.
Claim. For every degree $n$, if $v$ is the inclusion of singular $n$-chains on $V$ into the small chain group of the open cover $(U,V)$ and $s$ is the inclusion of that small chain group into the singular $n$-chains on $X$, then $s\circ v$ equals the chain map induced by the continuous subspace inclusion $V\hookrightarrow X$.
background
In the singular Mayer–Vietoris setup one works with three chain objects in each degree: ordinary singular chains on $X$, ordinary singular chains on the open pieces $U$ and $V$, and the "small" chain group generated by simplices that land entirely in $U$ or entirely in $V$. The small generators are written sgen; the degree-$n$ inclusion of the small group into singular chains on $X$ is sInc.
The map vInc is the canonical leg that sends a singular simplex on $V$ to the corresponding small generator (via the index map vIdx). Upstream, gen_vInc records exactly that on free generators: the free generator of a simplex on $V$, postcomposed with vInc, is the small generator of its image index. Likewise sgen_sInc says that a small generator, postcomposed with sInc, is the ordinary free generator of the underlying singular simplex on $X$.
The target identity is the chain map of the continuous inclusion $V\subset X$ supplied by SingularPair.subInc.
proof idea
Both sides are morphisms out of a biproduct (coproduct) of copies of $\mathbb{Z}$ in ModuleCat, so it is enough to check agreement on each summand inclusion. Apply Sigma.hom_ext and fix a generator index $a$.
Rewrite the left composite by pulling the summand inclusion through vInc via gen_vInc, which replaces it by the small generator at vIdx a. Then apply sgen_sInc followed by gen_map (naturality of free generators under the subspace inclusion). The two sides match definitionally, and rfl closes.
why it matters
This is the basic compatibility that lets the V-leg of the Mayer–Vietoris diagram sit inside ordinary singular chains. Downstream, vInc_injective obtains injectivity of vInc by postcomposing with sInc, rewriting via this lemma, and invoking injectivity of the ordinary subspace chain map. The same identity is the cancellation step in vInc_comm, which proves that vInc intertwines boundaries (needed for it to be a chain-map leg of the MV short complex). It also feeds smallV_comp_smallθ.
In the Recognition foundation stack this sits in the singular-homology toolkit used to control topological invariants of the discrete recognition complex (eight-tick octave, cover arguments). It does not itself force $D=3$ or the J-cost; it is infrastructure for those later geometric constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.