gen_comp_sdOpIter
plain-language theorem explainer
The k-fold singular subdivision of a generator simplex equals the singular chain obtained by transporting the k-fold affine barycentric subdivision of the standard identity simplex along that generator. Anyone reducing singular subdivision to affine diameter estimates cites this. The proof is induction on k, using the single-step intertwining of the chain transport with one subdivision step.
Claim. Let $s$ be a singular $n$-simplex on $X$ and $k\in\mathbb{N}$. Writing $G_s$ for the free-chain generator of $s$ and $\mathrm{Sd}^k$ for the $k$-fold singular subdivision operator, one has $G_s\circ\mathrm{Sd}^k$ equal to the image, under the chain map induced by $s$, of the $k$-fold affine barycentric subdivision of the standard identity $n$-simplex.
background
This module builds barycentric subdivision for singular chains on a topological space $X$, in the style of algebraic topology (Mathlib singular homology). Generators of the free chain group $C_n(X)$ are singular $n$-simplices. The singular subdivision operator $\mathrm{Sd}$ is defined so that it intertwines with affine barycentric subdivision on the standard simplex via the chain transport toChain along a simplex map.
Affine side: asimplex turns a vertex tuple in the standard simplex into an affine chain; asubIter iterates the barycentric subdivision operator built from the barycenter map baryFn. The identity tuple is the standard ordered vertex set of $\Delta^n$. Stage 6 of the module tracks Finsupp support of these affine pieces and proves geometric diameter decay under iteration (factor $n/(n+1)$ in the sup metric).
The present identity is the bridge: singular subdivision of a generator is exactly affine subdivision of the model simplex, pushed forward by that generator. Downstream smallness and Mayer–Vietoris arguments reduce to the affine geometry of stage 6.
proof idea
Induction on the iteration count $k$.
Base $k=0$: both sides are the identity. Rewrite with the zero-iterate clauses for singular and affine subdivision, cancel the categorical identity composite, and apply the fact that transporting the affine identity simplex along $s$ recovers the generator of $s$.
Successor: unfold one singular iterate and one affine iterate, reassociate, and insert the inductive hypothesis. The remaining equality is the single-step intertwining lemma: chain transport along $s$ commutes with one application of the singular subdivision operator. Evaluate that linear-map identity on the already-subdivided affine identity simplex to finish.
why it matters
Stage 6 payoff and the small-simplices route to Mayer–Vietoris both need singular subdivision of generators reduced to affine support geometry. Downstream, exists_asubIter_small states that iterated affine barycentric pieces of any affine simplex become uniformly small; this lemma is the singular-to-affine dictionary that lets those diameter bounds speak about singular chains. exists_sdOpIter_mem_smallSpan (SingularMayerVietoris) uses the dictionary for uniform smallness: every singular chain has some iterate landing in the small span of an open cover, the key input to a singular Mayer–Vietoris sequence.
In the Recognition foundation stack this is scaffolding for homology-level arguments (covers, excision-type splittings) rather than a direct T0–T8 forcing step. It does not itself force $\varphi$, eight-tick structure, or $D=3$; it equips the singular complex so later geometric comparison can run on controlled supports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.