sdOpIter_zero
plain-language theorem explainer
The zero-fold iterate of the singular subdivision operator is the identity endomorphism of the degree-n singular chain group. Algebraic topologists and anyone inducting on subdivision depth cite it as the base case. The proof is definitional: it unfolds the recursive clause for iterate zero.
Claim. For any topological space $X$ and degree $n\in\mathbb{N}$, the $0$-th iterate of the singular subdivision operator on the degree-$n$ singular chain group $C_n(X;\mathbb{Z})$ equals the identity morphism $\mathrm{id}_{C_n(X;\mathbb{Z})}$.
background
In this module the singular chain group $C_n(X;\mathbb{Z})$ is realized as the coproduct $\coprod_{\sigma} \mathbb{Z}$ indexed by singular $n$-simplices of $X$ (the abbreviation Cgrp). The singular subdivision operator is an endomorphism of that group that barycentrically subdivides each generator; its iterates are defined by recursion on the iteration count.
The recursive definition sets the zero iterate to the identity arrow and the successor to post-composition with one more subdivision step. That base clause is exactly what this lemma records, so every induction on iteration depth can discharge the $k=0$ case by simplification.
The surrounding development builds chain homotopies between the identity and high iterates of subdivision, the classical tool that proves singular homology is a homotopy invariant and feeds Mayer–Vietoris arguments later in the foundation layer.
proof idea
One-line definitional proof: the recursive definition of the iterate already has the clause 0 ↦ 𝟙, so rfl closes the equality. No lemmas are applied beyond unfolding that definition.
why it matters
Every induction on subdivision depth bottoms out here. Downstream, additivity of iterates (sdOpIter_add), preservation of the small-span submodule (sdOpIter_mem_smallSpan), the chain-map property of iterates (sdOpIter_comp_bnd), commutation with a single subdivision step, the generator–affine-support comparison (gen_comp_sdOpIter), and both the zero and successor cases of the telescoped chain homotopy ∂T_k + T_k∂ = id − S^k all rewrite the zero iterate via this simp lemma.
In the Recognition Science foundation stack this is pure scaffolding for singular homology: it does not touch the forcing chain T0–T8, the J-cost, or φ, but it is required before Mayer–Vietoris and excision can be stated in Lean, which in turn underwrite continuum and covering arguments used higher in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.