toChain_comp_sdOp
plain-language theorem explainer
The chain map induced by a continuous simplex intertwines singular subdivision on the target with affine barycentric subdivision on the standard simplex. Homology and subdivision arguments in the Recognition foundation cite this commutation. The proof is a short generator-wise reduction: affine-chain extensionality plus a push-simplex lemma.
Claim. Let $\sigma:\Delta^n\to X$ be continuous. Then post-composition of the induced chain map $\mathrm{toChain}(\sigma)$ with the singular subdivision operator equals composition of that same chain map with the affine barycentric subdivision of the identity $n$-simplex: $\mathrm{sd}_*\circ\mathrm{toChain}(\sigma)=\mathrm{toChain}(\sigma)\circ\mathrm{asub}(\mathrm{bary}_n)$.
background
This module builds singular subdivision for continuous simplices into a space $X$, linking it to affine geometry on vertex tuples. Affine $n$-chains $\mathrm{AC}(\alpha,n)$ are finitely supported $\mathbb{Z}$-linear combinations of maps $\mathrm{Fin}(n+1)\to\alpha$ (vertex tuples). The affine simplex generator attaches such a tuple; barycentric subdivision $\mathrm{asub}(\mathrm{bary}_n)$ acts on those tuples by the standard barycentric map.
Singular subdivision $\mathrm{sdOp}$ acts on singular chains of $X$. The map $\mathrm{toChain}(\sigma)$ sends an affine chain on the standard simplex to the singular chain obtained by pushing the continuous simplex $\sigma$ along that affine data. The lemma asserts these two subdivision operators commute through $\mathrm{toChain}$.
Upstream, the proof uses affine-chain hom-extensionality and the generator identity that pushing a simplex after singular subdivision equals affine subdivision then push (the push-simplex commutation).
proof idea
Term-mode proof by affine-chain extensionality: it suffices to check equality on a generator $w$. Unfold both linear-map compositions, rewrite the left-hand side via the definition of $\mathrm{toChain}$ on an affine simplex, and finish by the generator lemma that push-simplex after singular subdivision equals affine barycentric subdivision then push. No induction; pure pointwise reduction on $\mathrm{AC}$.
why it matters
This is the one-step commutation that lets singular subdivision be read off affine support geometry. Downstream, $\mathrm{gen_comp_sdOpIter}$ iterates it: the $k$-fold singular subdivision of a generator equals evaluating the $k$-fold affine barycentric subdivision of the identity tuple under $\mathrm{toChain}$. That parent doc states it "ties the singular operator to the affine support geometry of stage 6."
In the Recognition foundation stack, stage-6 support control feeds the forcing chain's geometric constraints (eight-tick octave, $D=3$) by ensuring subdivision does not invent new combinatorial support beyond barycentric refinement. Without this intertwining, the singular and affine sides of the subdivision argument would drift apart.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.