tOpIter_succ
plain-language theorem explainer
The telescoped subdivision homotopy at step k+1 equals the base homotopy plus subdivision composed with the k-step homotopy. Algebraic topologists cite it when inducting on the chain-homotopy identity id − S^k = ∂T_k + T_k∂. The proof is definitional (rfl).
Claim. For any space $X$ and degrees $n,k\in\mathbb{N}$, the telescoped singular subdivision homotopy satisfies $T_{k+1}=T+S\circ T_k$ as morphisms $C_n(X)\to C_{n+1}(X)$, where $T$ is the base subdivision homotopy and $S$ is the barycentric subdivision operator.
background
In the singular-subdivision module one works with the free abelian chain groups $C_n(X)$ of continuous singular simplices on a topological space $X$. The barycentric subdivision operator $S=\mathrm{sdOp}$ is an endomorphism of $C_n(X)$; the companion prism operator $T=\mathrm{tOp}$ raises degree by one and supplies a chain homotopy between $\mathrm{id}$ and $S$.
The iterate $T_k=\mathrm{tOpIter}$ is defined by $T_0=0$ and the recurrence $T_{k+1}=T+S\circ T_k$. This is the standard telescoping construction that realises a homotopy from $\mathrm{id}$ to $S^k$. The present lemma simply exposes that recursive clause as an equality of morphisms.
Upstream, $\mathrm{tOp}$ and $\mathrm{sdOp}$ are assembled by descending generators (barycentric cones and faces) via $\Sigma$-descents; the iterate itself is the Nat-recursion already recorded in the definition of $\mathrm{tOpIter}$.
proof idea
One-line term proof by rfl. The right-hand side is exactly the successor clause in the recursive definition of tOpIter, so the equality is definitional.
why it matters
Induction on the telescoped chain-homotopy identities needs the successor step written as an equality of morphisms. Downstream, tOpIter_chain_homotopy_succ and tOpIter_chain_homotopy_zero rewrite with this lemma to obtain $\partial T_k+T_k\partial=\mathrm{id}-S^k$ (and the degree-zero truncation $\partial T_k=\mathrm{id}-S^k$). The same unfolding feeds tOpIter_mem_smallSpan, which keeps the homotopy inside the small-span subcomplex used for Mayer–Vietoris.
In the Recognition foundation this is pure scaffolding for singular homology: once the iterated homotopy is available, barycentric subdivision becomes homotopic to the identity, so homology is invariant under refinement and the Mayer–Vietoris sequence can be assembled. No forcing-chain landmark (T5–T8) is touched directly; the lemma is infrastructure for the topological side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.