tOpIter_chain_homotopy_succ
plain-language theorem explainer
On singular chains of a space X in degree n+1, the iterated prism operator T_k is a chain homotopy from the identity to the k-fold barycentric subdivision S^k: ∂T_k + T_k∂ = id − S^k. Algebraic topologists cite this when reducing homology computations to small simplices. The proof is induction on k, using the single-step prism homotopy and naturality of subdivision under the boundary.
Claim. For any topological space $X$ and naturals $n,k$, writing $\partial$ for the singular boundary, $T_k$ for the $k$-fold prism operator, and $S^k$ for the $k$-fold barycentric subdivision operator on singular chains, one has $\partial\circ T_k + T_k\circ\partial = \mathrm{id} - S^k$ as endomorphisms of the degree-$(n+1)$ singular chain group of $X$.
background
This lives in the singular-subdivision foundation layer: singular chain groups $C_\bullet(X)$ of a space $X\in\mathbf{Top}$, with boundary $\partial=\mathrm{bnd}$, the barycentric subdivision operator $S=\mathrm{sdOp}$, and the prism (chain-homotopy) operator $T=\mathrm{tOp}$ that witnesses $S\simeq\mathrm{id}$. Iterates $S^k=\mathrm{sdOpIter}$ and $T_k=\mathrm{tOpIter}$ are defined by the usual recurrence $S^{k+1}=S\circ S^k$ and $T_{k+1}=T+S\circ T_k$ (with $T_0=0$, $S^0=\mathrm{id}$).
The single-step identity $\partial T+T\partial=\mathrm{id}-S$ (in positive degree) is already available as tOp_chain_homotopy_succ; naturality of subdivision under the boundary, $S\circ\partial=\partial\circ S$, is sdOp_comp_bnd. The module builds the affine-simplex calculus (cones, prisms, supports) needed to make these operators concrete on singular chains, then lifts them to the chain-complex morphisms used here.
proof idea
Induction on the iteration count $k$.
Base $k=0$: $T_0=0$ and $S^0=\mathrm{id}$, so both sides collapse to $0=\mathrm{id}-\mathrm{id}$ by the zero-comp and sub_self simplifications.
Successor step: expand $T_{k+1}$ and $S^{k+1}$ by their recursive clauses. Distribute $\partial$ and composition over the resulting sums (preadditive comp_add/add_comp and associativity). The cross term $\partial\circ S\circ T_k$ is rewritten via naturality $S\circ\partial=\partial\circ S$ so that $S$ factors out on the left. The remaining expression splits as the single-step homotopy $\partial T+T\partial$ plus $S$ applied to the inductive hypothesis block $\partial T_k+T_k\partial$. Substitute tOp_chain_homotopy_succ and the IH, use $S^{k+1}=S^k\circ S$ (sdOpIter_comp_sdOp), and finish by abelian cancellation (abel).
why it matters
This is the telescoped homotopy that turns one-step subdivision into a genuine chain-homotopy equivalence $\mathrm{id}\simeq S^k$ in every positive degree. Downstream, sub_sdOpIter_eq_bnd_succ specialises it to cycles: if $\partial z=0$ then $z-S^k z=\partial(T_k z)$, so a cycle and its subdivided image differ by a boundary. That identity is the algebraic engine behind Mayer–Vietoris arguments in SingularMayerVietoris.
It also feeds exists_asubIter_small (Stage 6 payoff): once chains may be replaced by highly subdivided ones up to homology, the geometric fact that iterated barycentric pieces of an affine simplex become uniformly small upgrades to a homology statement. In the Recognition Science foundation stack this is pure singular-homology scaffolding (not a T0–T8 forcing step), but it is required infrastructure for any later comparison of recognition complexes with classical singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.