sdOpIter_mem_smallSpan
plain-language theorem explainer
Any singular n-chain already in the (U,V)-small span stays there under every iterate of the subdivision operator. Workers assembling singular Mayer–Vietoris cite this to keep cover-supported chains inside the small subcomplex while refining mesh. The argument is induction on the iterate count, feeding the single-step preservation lemma at each successor.
Claim. Let $U,V\subseteq X$ and $n,k\in\mathbb{N}$. If a singular $n$-chain $z$ lies in the small span of the cover $(U,V)$, then the $k$-fold iterate of the subdivision operator on $z$ again lies in that same small span.
background
The ambient setting is the singular chain complex of a space $X$, with $C_n(X)$ the free module on continuous maps $\Delta^n\to X$. Relative to a two-set cover $(U,V)$, the small span is the submodule generated by those singular simplices whose image lands entirely in $U$ or entirely in $V$. It is the algebraic home of the small chain complex used for Mayer–Vietoris.
Subdivision (the operator underlying barycentric or prism refinement) acts degreewise on chains. A prior one-step lemma already records that a single application of subdivision sends the small span into itself. The present statement lifts that fact from one step to an arbitrary finite iterate, so mesh refinement never ejects a chain that started cover-supported.
Module context is the singular Mayer–Vietoris development: inclusions and retractions between the small complex and the full singular complex, together with the subdivision package imported from SingularSubdivision.
proof idea
Term-mode induction on the iterate count $k$.
Base case $k=0$: the zero-iterate is the identity endomorphism of the chain group, so membership is unchanged and the hypothesis applies directly.
Successor step: rewrite the $(k+1)$-st iterate as subdivision composed with the $k$-th iterate, then apply the single-step lemma sdOp_mem_smallSpan to the inductive hypothesis. No extra hypotheses on $U$ or $V$ are needed; pure submodule closure under the operator suffices.
why it matters
This is the inductive engine behind uniform smallness: the downstream lemma exists_sdOpIter_mem_smallSpan asserts that, when $U$ and $V$ are open and cover $X$, every singular chain admits some iterate landing in the small span. That existence proof reduces generators to a finite-support case and then invokes the present closure fact to keep the refined chain inside the small span once it arrives.
In the Recognition foundation stack, singular Mayer–Vietoris supplies the homological glue for cover-based arguments (local-to-global passage on chain complexes). Keeping subdivision inside the small span is the algebraic counterpart of mesh refinement that respects the cover, which is required before connecting sequences and long exact sequences can be written on the small complex. The lemma itself is pure chain-level bookkeeping; its value is that the uniform-smallness parent can quote it without re-proving operator invariance at each inductive step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.