ateeIter
plain-language theorem explainer
Telescoped chain homotopy packaging the partial geometric sum of barycentric subdivision: degreewise, T_0 = 0 and T_{k+1} = T + T_k ∘ S as a ℤ-linear map from affine n-chains to (n+1)-chains. Anyone proving ∂T_k + T_k∂ = id − S^k cites this recursion. The body is a one-line match on the iteration count k.
Claim. Fix a barycenter assignment on vertex tuples. For each iteration count $k$ and degree $n$, the telescoped homotopy $T_k$ is the $\mathbb{Z}$-linear map from affine $n$-chains in $\alpha$ to affine $(n+1)$-chains defined by $T_0 = 0$ and $T_{k+1} = T + T_k \circ S$, where $T$ is the subdivision chain homotopy and $S$ is barycentric subdivision.
background
Affine $n$-chains $\mathrm{AC}_\alpha(n)$ are finitely supported $\mathbb{Z}$-linear combinations of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. The module sits in the Foundation singular-subdivision layer, which builds barycentric subdivision and its chain homotopy on these affine generators before lifting to singular chains.
Barycentric subdivision $S$ is defined by the cone recursion $S(\sigma)=b_\sigma\cdot S(\partial\sigma)$ on generators ($S=\mathrm{id}$ in degree 0). The single-step chain homotopy $T$ uses the companion recursion $T(\sigma)=b_\sigma\cdot(\sigma-T(\partial\sigma))$ ($T=0$ in degree 0). Both take a barycenter map as a parameter.
Classically one wants a homotopy between $S^k$ and the identity. The geometric series $1+S+\cdots+S^{k-1}$ supplies it once $T$ is known; this definition packages that series degreewise.
proof idea
Definition by recursion on the iteration count. The zero case returns the zero map. The successor case adds the single-step homotopy $T$ (at degree $n$) to the previous iterate post-composed with subdivision $S$ (at the same degree), using linear-map composition. No lemmas are invoked; the match is the entire body.
why it matters
This is the inductive carrier for the telescoped homotopy identity. Downstream, abnd_comp_ateeIter proves $\partial\circ T_k+T_k\circ\partial=\mathrm{id}-S^k$ on positive-degree affine chains by induction on $k$, using the successor and zero unfolding lemmas that read off this definition.
In the Recognition Foundation stack the identity is the algebraic engine that shows iterated barycentric subdivision is chain-homotopic to the identity, so it induces the identity on homology. That fact underwrites comparison and invariance arguments for singular homology built from affine chains. The construction is classical (Eilenberg–Steenrod style) rather than an RS forcing-chain step; it supplies the homological scaffolding those later steps sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.