gen_pushSimplex_comp_sdOp
plain-language theorem explainer
On a generator obtained by pushing a singular simplex along a vertex tuple, the singular subdivision operator equals the image under the transport map of the affine barycentric subdivision of that tuple. Algebraic topologists building the chain-map property of singular subdivision cite this transport identity. The proof rewrites via the generator formula for subdivision, then matches affine maps through composition lemmas for barycentric subdivision.
Claim. Let $\sigma:\Delta^n\to X$ be a continuous singular $n$-simplex and let $w:\mathrm{Fin}(n'+1)\to\Delta^n$ be a vertex tuple. Then the singular subdivision operator applied to the generator of the pushed simplex $\sigma\circ\mathrm{aff}(w)$ equals the singular chain obtained by transporting, via $\sigma$, the affine barycentric subdivision of the affine simplex determined by $w$.
background
This module develops singular subdivision on the singular chain complex of a topological space $X$, in the style of classical algebraic topology (barycentric subdivision of singular simplices). The generator map sends an indexed singular simplex to the corresponding basis element of the free $\mathbb{Z}$-module of $n$-chains.
Pushing a simplex along a vertex tuple $w$ composes $\sigma$ with the affine map $\Delta^{n'}\to\Delta^n$ that sends standard vertices to $w$. The affine subdivision operator acts on formal $\mathbb{Z}$-linear combinations of affine simplices by iterated barycentric coning; baryFn supplies the barycenter data. The transport toChain $\sigma$ converts an affine chain in the standard simplex into a singular chain in $X$ by post-composing with $\sigma$.
Upstream, the affine map of a vertex tuple is the continuous map $\Delta^n\to\Delta^m$ determined by sending vertices to the tuple, and composing that map with the identity tuple recovers the tuple itself. The generator of a singular simplex is the canonical inclusion of that summand into the free chain module.
proof idea
Term-mode rewrite proof. First expand subdivision on a generator via the defining identity for sdOp on generators, reducing to a toChain expression on the barycentric subdivision of the identity tuple after applying the simplex equivalence of the pushed simplex.
Rewrite the equivalence of the push by the corresponding push lemma. Apply function congruence for the linear map identity that toChain intertwines affine post-composition with push, evaluated on the subdivided identity tuple. Then apply congruence for the composition law relating affine-map post-composition to affine subdivision (using that barycenters are preserved under affine maps). Finish by simplifying the affine map on an affine simplex and recovering the original vertex tuple from composition with the identity tuple.
why it matters
This is the transport heart of singular subdivision: it moves subdivision from the singular side onto affine barycentric data where combinatorial identities are available. Downstream, toChain_comp_sdOp quotes it directly to prove that transport intertwines singular subdivision with affine subdivision on every generator, and sdOp_comp_bnd uses the generator calculus (including this style of identity) to prove that subdivision is a chain map, $\partial\circ S=S\circ\partial$.
In the Recognition Science foundation stack, singular-homology infrastructure supports continuum and topological arguments that sit beneath forcing and continuum limits; the lemma itself is pure AT bookkeeping rather than a T0–T8 forcing step. It closes a proved (no-sorry) link needed before chain-homotopy and homology-invariance statements for subdivision can be assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.