sInc_comp_sRet
plain-language theorem explainer
The inclusion of degree-n small singular chains into ordinary singular chains admits a left inverse (a retraction). Anyone building the Mayer–Vietoris sequence from small simplices cites this to get a split monomorphism. The proof is a coproduct-hom extension: on each generator it reduces via the generator–inclusion identity and the definition of the retraction.
Claim. For open sets $U,V\subseteq X$ and each degree $n$, the composition of the inclusion of the small chain group into the singular chain group with the canonical retraction is the identity on the small chain group: $\iota_n\circ r_n=\mathrm{id}$ on $C_n^{\mathrm{small}}(U\cup V)$.
background
In the singular Mayer–Vietoris setup one works with the free $\mathbb{Z}$-module on singular $n$-simplices whose image lies in $U$ or in $V$ (the small simplices). That module is presented as a coproduct of copies of $\mathbb{Z}$, one per small simplex index; the coproduct inclusions are the generators of the small chain group.
The degree-$n$ inclusion map sends each small generator into the ordinary singular chain group of $X$. A matching retraction is defined by sending a generator to the corresponding small generator when the simplex is small, and to zero otherwise. The local theoretical setting is the construction of a short exact sequence of chain complexes that yields the Mayer–Vietoris long exact sequence after passage to homology.
Upstream, the generator–inclusion identity records that including a small generator and then reading it back is just the generator itself; that identity is the algebraic input used here.
proof idea
Extend equality of morphisms out of a coproduct by checking on each generator (Sigma.hom_ext). On the generator attached to a small index $t$, rewrite the composite using the right-unit law and the generator–inclusion identity, so the claim becomes that the retraction applied to the ordinary coproduct inclusion at $t$ recovers the small generator. Unfold the retraction: it is a coproduct descent, and the decidable membership test fires positively on $t$, returning exactly that generator. A final congruence closes the equality.
why it matters
Split monicity of the small-chain inclusion is the first exactness ingredient in the singular Mayer–Vietoris short exact sequence of chain complexes. Downstream, the mono lemma is the one-line application of mono-of-mono-fac to this identity, and the elementwise injectivity lemma recovers injectivity by postcomposing an equality of images with the retraction and cancelling via this composite-identity. Without a left inverse one would only have a mono after more work; the split form also makes the connecting homomorphism in the long exact sequence concrete. In the Recognition foundation stack this sits inside the singular-homology toolkit used to control topological invariants of recognition spaces, not a T0–T8 forcing step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.