small_surj_succ
plain-language theorem explainer
If y is an (n+1)-cycle on X and open sets U,V cover X, then y is homologous to the image of a small cycle supported in U∪V. Algebraic topologists building Mayer–Vietoris for singular homology cite this as the surjectivity half of the small-complex comparison. The proof subdivides y into the small span, lifts, and corrects by the prism homotopy operator.
Claim. Let $U,V\subseteq X$ be open with $U\cup V=X$. For every $n\in\mathbb{N}$ and every singular $(n+1)$-cycle $y$ on $X$ (i.e. $\partial y=0$), there exist a small $(n+1)$-cycle $x$ (supported in $U$ or $V$) and a singular $(n+2)$-chain $w$ such that the inclusion of $x$ equals $y+\partial w$.
background
This module builds the singular Mayer–Vietoris sequence by comparing the full singular chain complex $C_\bullet(X)$ with the subcomplex of small chains: those generated by simplices landing entirely in $U$ or entirely in $V$. The small complex is written $sC_\bullet(U,V)$, with inclusion $sInc$ into $C_\bullet(X)$ and induced boundary $sBnd$.
The key geometric input is uniform smallness: iterated barycentric subdivision eventually pushes every chain into the small span whenever $U$ and $V$ are open and cover $X$ (lemma exists_sdOpIter_mem_smallSpan). Subdivision is chain-homotopic to the identity via a prism operator $t$, so $sd^k(z)-z$ is always a boundary when $z$ is a cycle.
The present lemma is the surjectivity half of the comparison in positive degrees: every full cycle is homologous to a small cycle.
proof idea
Apply uniform smallness to obtain $k$ with $sd^k(y)$ in the small span, then lift to a small chain $x$ with $sInc(x)=sd^k(y)$. Set $w=-t^k(y)$, the negative prism iterate.
Cycle condition: $sInc$ is mono, and $sInc\circ sBnd=\partial\circ sInc$, so $sBnd(x)=0$ reduces to $\partial(sd^k(y))=sd^k(\partial y)=0$.
Homology equation: the subdivision homotopy identity $sd^k(y)=y-\partial(t^k(y))$ (valid because $\partial y=0$) rearranges, after the sign on $w$, to $sInc(x)=y+\partial w$. Both steps finish by abelian-group arithmetic.
why it matters
Feeds directly into smallι_isIso_homologyMap, which asserts that inclusion of the small complex induces an isomorphism on homology in every degree. That isomorphism is the standard bridge from the short exact sequence of small/full chains to the long exact Mayer–Vietoris sequence in singular homology.
In the Recognition Science foundation layer this is pure algebraic topology scaffolding: it underwrites excision and cover-based computations used later when singular data meet the eight-tick and dimensional forcing chain. It does not itself invoke J-cost, $\varphi$, or the RCL; it supplies the homological infrastructure those arguments sit on.
Status is fully proved (no sorry). The companion injectivity input in each degree is the other half of the iso.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.