tOpIter_mem_smallSpan
plain-language theorem explainer
The k-fold telescoped prism homotopy sends any chain in the U–V small span of degree n into the small span one degree higher. Cite it when building Mayer–Vietoris exactness from subdivision and prism operators on singular chains. The argument is induction on k, closing by the already-proved facts that both the single prism map and singular subdivision preserve the small span.
Claim. Fix sets $U,V\subseteq X$ and degree $n$. For every iterate count $k\in\mathbb{N}$ and every singular $n$-chain $z$, if $z$ lies in the submodule spanned by generators supported in $U$ or in $V$, then the $k$-fold telescoped homotopy applied to $z$ lies in the corresponding small-span submodule in degree $n+1$.
background
This module builds the singular Mayer–Vietoris apparatus: the small chain groups are the spans of singular simplices whose images lie entirely in $U$ or entirely in $V$, and smallSpan U V n is that submodule of the free singular chain module Cgrp X n.
The singular subdivision operator sdOp refines chains while staying inside the same degree; the companion lemma records that it preserves the small span. The prism (telescoping) operator tOp raises degree by one and supplies the chain homotopy between identity and subdivision; tOpIter is its finite iterate, defined by the usual recurrence tOpIter 0 = 0 and tOpIter (k+1) = tOp + sdOp ≫ tOpIter k.
Locally one is proving that the whole homotopy package respects the $U$–$V$ support filtration, which is the algebraic input needed before comparing the small complex to the full singular complex on a cover.
proof idea
Proof by induction on the iterate index $k$, pattern-matching the recurrence of tOpIter.
For $k=0$, rewrite by tOpIter_zero to the zero morphism and apply Submodule.zero_mem.
For the successor, rewrite by tOpIter_succ so the image is (tOp + sdOp ≫ tOpIter k) z. Expand the sum, apply ModuleCat.comp_apply, and close with Submodule.add_mem: the first summand is in the small span by tOp_mem_smallSpan, the second by the inductive hypothesis after sdOp_mem_smallSpan puts the subdivided chain back into the small span of degree $n$.
why it matters
The sole recorded consumer is small_inj, the degree-wise injectivity input for the small complex: if a small $n$-cycle is a boundary in the ambient singular complex, it is already a boundary in the small complex. That step needs the telescoped homotopy to map small chains to small chains one degree up, exactly what this lemma supplies.
In the broader Recognition foundation stack this is pure singular-homology scaffolding (Mayer–Vietoris exactness for an open cover), not a forcing-chain identity. It sits under the topological side of the monolith that later interfaces with discrete evolution and octave structure, but the lemma itself is classical chain-level bookkeeping: support-preserving prism iterates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.