sInc_injective
plain-language theorem explainer
The degree-n inclusion of small singular chains (simplices landing in U or V) into ordinary singular n-chains is injective. Anyone building the singular Mayer–Vietoris sequence for an open cover will cite this as the mono half of the small-complex comparison. The proof is a one-shot left-inverse argument: the retraction of the inclusion composes to the identity on the small chain group, so equal images force equal preimages.
Claim. For sets $U,V \subseteq X$ and each degree $n\in\mathbb{N}$, the degree-$n$ inclusion homomorphism from the small chain group (generated by singular $n$-simplices with image in $U$ or in $V$) into the singular chain group $C_n(X;\mathbb{Z})$ is injective as a map of abelian groups.
background
This module builds a singular Mayer–Vietoris comparison for a cover of a space $X$ by two sets $U$ and $V$. The small chain group in degree $n$ is the free $\mathbb{Z}$-module on singular $n$-simplices whose image lies entirely in $U$ or entirely in $V$; it sits inside the ordinary singular chain group $C_n(X)$.
The inclusion of that small group is the morphism written as the degree-$n$ inclusion map: on generators it is the canonical generator map of the ambient singular complex. A matching retraction is defined so that inclusion followed by retraction is the identity on the small group (recorded as the composition identity lemma for those two maps).
The local setting is the algebraic half of singular MV: one needs the small complex to inject into, and eventually to compute the homology of, the full singular complex when $U\cup V=X$ with $U,V$ open.
proof idea
Term-mode injectivity via a left inverse. Take $a,b$ in the small chain group with equal images under the inclusion. Apply the retraction to both sides (congruence of the retraction morphism). Rewrite the resulting equality using the composition identity (inclusion then retraction equals the identity on the small group) and the module-category rules for composition and identity application. The rewritten equality is exactly $a=b$.
why it matters
Elementwise injectivity is the mono input used by the two comparison lemmas that feed the singular Mayer–Vietoris exact sequence in this module. Downstream, the injectivity lemma for small cycles (every small chain that is a boundary in the ambient complex is already a small boundary) invokes this fact when it identifies preimages under the inclusion. The positive-degree surjectivity input for small chains likewise relies on existence of small preimages under the same inclusion.
In the broader Recognition foundation stack this is pure singular-homology scaffolding: it does not touch the forcing chain (T0–T8), the J-cost, or the phi ladder. It exists so that cover-based exact sequences for singular chains are available when later geometric or recognition arguments need homology of unions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.