asubIter_succ
plain-language theorem explainer
The (k+1)-fold barycentric subdivision of affine chains equals one subdivision composed with the k-fold iterate. Inductive arguments about iterated subdivision (chain-map identities, prism homotopies, diameter contraction) cite this unfolding at the successor step. The equality is definitional: it is reflexivity from the recursive construction of the iterate.
Claim. Fix a barycenter assignment $b$ and degrees $k,n\in\mathbb{N}$. Writing $S$ for the barycentric subdivision operator on affine $n$-chains and $S^{k}$ for its $k$-fold iterate, one has $S^{k+1}=S\circ S^{k}$ as $\mathbb{Z}$-linear endomorphisms of the affine chain module in degree $n$.
background
The module develops barycentric subdivision on affine chains as the geometric engine behind singular subdivision. Affine $n$-chains are finitely supported $\mathbb{Z}$-linear combinations of ordered $(n+1)$-tuples in an ambient affine space $\alpha$. The single-step operator $S$ is defined by cone recursion on generators: in degree $0$ it is the identity, and in degree $n+1$ one cones the already-subdivided boundary from the barycenter of the simplex.
Iterates $S^{k}$ are the natural tool for diameter estimates and for building the chain homotopy that shows $S$ is homotopic to the identity. The barycenter parameter is an arbitrary assignment of a point to each finite tuple, so the same algebra covers both abstract affine subdivision and the standard geometric barycenter on the standard simplex.
Upstream, the single-step map is the linear combination of cones of subdivided boundaries; composition of chain maps is ordinary linear-map composition. The iterate itself is the usual function iteration of that endomorphism.
proof idea
Purely definitional. The iterate is constructed so that the successor clause is composition of one subdivision with the previous iterate; the stated equality is therefore rfl. No lemmas are applied.
why it matters
This is the successor step used throughout the subdivision calculus. The chain-map theorem for iterates (boundary commutes with $S^{k}$) inducts by rewriting the successor via this identity and applying the single-step chain-map law. The same rewrite drives the induction for the telescoped prism homotopy $\partial T_{k}+T_{k}\partial=\mathrm{id}-S^{k}$, for commutation of $S$ with its own iterates, and for the $k$-fold support/diameter bound (pairwise distances contract by $(n/(n+1))^{k}$).
Downstream it also links singular and affine pictures: the iterated singular subdivision of a generator equals evaluation of the iterated affine subdivision of the identity tuple. In the Recognition foundation stack this is scaffolding for geometric control of singular chains, not a forcing-chain landmark (T5–T8), but it is load-bearing for any argument that needs subdivision to be a chain map or a contraction on supports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.