gen_pushSimplex_comp_tOp
plain-language theorem explainer
On a singular simplex pushed along an affine vertex map, the prism operator on the corresponding chain generator equals the chain obtained by pushing the barycentric prism of that vertex tuple. Algebraic topologists assembling the subdivision chain homotopy cite this generator-level identity. The argument rewrites through the generator–homotopy formula, the push–simplex equivalence, and naturality of the affine chain map under barycentric operators.
Claim. Let $\sigma:\Delta^n\to X$ be continuous and let $w:\mathrm{Fin}(n'+1)\to\Delta^n$ be a vertex tuple. Writing $\mathrm{push}(\sigma,w)$ for the singular $n'$-simplex $\sigma\circ\mathrm{affine}(w)$, one has $\iota(\mathrm{push}(\sigma,w))\circ T_{n'}=\mathrm{toChain}_\sigma\bigl(\mathrm{atee}(b_n,n',\mathrm{asimplex}(w))\bigr)$, where $\iota$ is the free generator of the singular chain group, $T$ is the prism/homotopy operator, and $b_n$ is the barycentric vertex map in degree $n$.
background
This module builds the barycentric subdivision operator $S$ and its prism homotopy $T$ on singular chains of a topological space $X$, in the Mathlib singular-homology setting. Singular $n$-simplices are continuous maps $\Delta^n\to X$; the free $\mathbb{Z}$-module they generate is written $C_n(X)$, with generators $\iota(\sigma)$ (here gen).
An affine map $\Delta^{n'}\to\Delta^n$ is determined by a vertex tuple $w:\mathrm{Fin}(n'+1)\to\Delta^n$ (affineMap). Pushing $\sigma$ along that map yields the singular simplex $\mathrm{pushSimplex},\sigma,w=\sigma\circ\mathrm{affine}(w)$. The operator $T$ (tOp) is the chain homotopy that will eventually satisfy $\partial T+T\partial=\mathrm{id}-S$; on a generator it is defined via a barycentric prism construction (atee of baryFn on an affine simplex).
Upstream, gen from SingularPrism is the coproduct inclusion of a basis simplex into $C_n(X)$. The identity toChain_amap records that postcomposition by $\sigma$ intertwines affine chain maps, and amap_comp_atee is the corresponding naturality for the barycentric prism.
proof idea
Term-mode rewrite proof. First apply gen_tOp, so the left-hand side becomes toChain of the barycentric prism of the identity tuple on the pushed simplex. Replace the simplex equivalence of a push by simplexEquiv_pushSimplex. Then use LinearMap.congr_fun on toChain_amap to slide $\sigma$ past the prism, and again on amap_comp_atee (with the barycentric compatibility sbary_affineMap) to move the affine map of $w$ inside atee. Finish by amap_asimplex and affineMap_comp_idTuple, which identify the resulting affine simplex with asimplex w under the degree-$n$ barycentric map.
why it matters
Parent consumer is tOp_chain_homotopy_succ, which proves the positive-degree chain-homotopy identity $\partial\circ T+T\circ\partial=\mathrm{id}-S$ on $C_{n+1}(X)$ by extending over generators. That identity is the algebraic heart of barycentric subdivision: $S$ is chain-homotopic to the identity, so it induces the identity on homology and can be used to compare singular chains with geometric subdivisions.
In the Recognition Science foundation stack this sits inside the singular-homology toolkit that underwrites continuum limits and geometric forcing arguments (spatial dimension $D=3$, eight-tick discrete structure). The lemma itself is pure algebraic topology; it closes a generator case needed before the global homotopy equation can be stated. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.