tOp_chain_homotopy_succ
plain-language theorem explainer
On singular chains of a space X in degree n+1 (n ≥ 0), the prism operator T is a chain homotopy from the identity to barycentric subdivision S: ∂T + T∂ = id − S. Algebraic topologists cite this as the one-step homotopy that makes iterated subdivision homotopic to the identity. The proof reduces to generators, pushes both composite summands into the free module on abstract simplices, and invokes the algebraic prism identity there.
Claim. For every topological space $X$ and every $n \in \mathbb{N}$, writing $\partial$ for the singular boundary, $T$ for the prism (chain-homotopy) operator, and $S$ for barycentric subdivision on singular chains, $$\partial_{n}\circ T_{n} + T_{n+1}\circ \partial_{n+1} = \mathrm{id} - S_{n+1}$$ on the degree-$(n+1)$ singular chain group of $X$.
background
The module builds singular chain groups $C_\bullet(X)$ for $X:\mathrm{Top}$, together with the usual boundary $\partial$, the barycentric subdivision operator $S$, and a prism operator $T$ that fills the straight-line homotopy from a simplex to its subdivided image. Algebraic counterparts on the standard simplex (abstract chains asimplex, abstract boundary abnd, abstract prism atee against the barycentric map baryFn) live in the free $\mathbb{Z}$-module on tuples; the geometric operators are recovered by pushing those formulas forward along singular simplices via toChain and the generator maps gen.
The local claim is the classical one-step chain-homotopy identity in positive degree: $\partial T + T\partial = \mathrm{id}-S$ on $C_{n+1}(X)$. Degree 0 is handled separately (both sides vanish). Upstream infrastructure includes naturality of generators under face maps and subdivision (gen_d, gen_tOp, gen_sdOp, gen_pushSimplex_comp_tOp) and the algebraic prism identity abnd_comp_atee on abstract simplices.
proof idea
Work after Sigma.hom_ext on a single generator $s$ of $C_{n+1}(X)$. Rewrite the two composite summands separately: $s\cdot(\partial\circ T)$ becomes toChain of the abstract prism applied to the abstract boundary of the identity simplex, via gen_d, face-push naturality, and gen_pushSimplex_comp_tOp; $s\cdot(T\circ\partial)$ becomes toChain of the abstract boundary of the abstract prism, via gen_tOp and toChain_comp_abnd. Their sum is therefore the image under toChain of the algebraic combination that abnd_comp_atee identifies with $\mathrm{id}-S$ on the abstract identity simplex. Transporting that identity back with gen_sdOp and toChain_asimplex_idTuple finishes the equality.
why it matters
This is the inductive step that feeds tOpIter_chain_homotopy_succ, which telescopes to $\partial T_k + T_k\partial = \mathrm{id}-S^k$ for the $k$-fold prism and subdivision operators. That iterated homotopy is the standard bridge from geometric subdivision to chain-level homotopy equivalences in singular homology, and it sits in the Foundation layer that packages classical singular machinery for later Recognition use (comparison maps, acyclic models, and continuum limits built on eight-tick / octave structure).
Within the forcing chain the lemma is infrastructure rather than a T0–T8 step: it does not force $\varphi$, $D=3$, or the J-cost, but it supplies the chain-homotopy control needed whenever singular chains must be compared after refinement. Downstream only the iterated form is listed as a direct consumer; once that is in hand, subdivision becomes homotopic to the identity in every positive degree.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.