pushSimplex_idTuple
plain-language theorem explainer
Pushing a singular $n$-simplex $\sigma$ along the identity vertex tuple recovers $\sigma$ itself under the singular-simplex equivalence. Anyone reducing subdivision or chain identities to the unsubdivided generator cites this. The proof unfolds the push definition and rewrites by the affine-map identity lemma plus composition with the identity map.
Claim. Let $\sigma:\Delta^n\to X$ be continuous. Writing $w_{\mathrm{id}}$ for the identity vertex tuple on $\Delta^n$ (the map sending each standard basis index to the corresponding vertex), the singular simplex obtained by precomposing $\sigma$ with the affine map of $w_{\mathrm{id}}$ equals $\sigma$ itself under the inverse of the singular-simplex equivalence $\mathrm{Idx}(X,n)\simeq C(\Delta^n,X)$.
background
This module builds singular subdivision machinery over Mathlib's singular homology, with continuous maps out of the standard simplex $\Delta^n=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin}(n+1))$ as the basic singular simplices.
The identity vertex tuple $w_{\mathrm{id}}=\mathrm{idTuple},n$ sends each index $i$ to the vertex $\mathrm{stdSimplex.vertex},i$. Its affine map is the identity continuous map on $\Delta^n$ (lemma affineMap_idTuple). The push operation forms the singular $m$-simplex obtained by precomposing $\sigma$ with the affine map of a vertex tuple $w$ in $\Delta^n$, then transporting via the inverse of the retyped singular-simplex equivalence $\mathrm{simplexEquiv}$.
That equivalence is Mathlib's $\mathrm{TopCat.toSSetObjEquiv}$, retyped so the domain is literally $\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin}(m+1))$ and rewriting is unblocked.
proof idea
One-line algebraic reduction after unfolding. Unfold the definition of the push: it is $\mathrm{simplexEquiv}^{-1}(\sigma\circ\mathrm{affineMap},w)$. Specialize $w$ to the identity tuple, replace $\mathrm{affineMap},w_{\mathrm{id}}$ by $\mathrm{id}_{\Delta^n}$ via affineMap_idTuple, then cancel $\sigma\circ\mathrm{id}=\sigma$ by ContinuousMap.comp_id. The result is exactly $\mathrm{simplexEquiv}^{-1},\sigma$.
why it matters
Local bookkeeping for the identity case of singular subdivision. Downstream, toChain_asimplex_idTuple applies it to show that the chain associated to the abstract identity simplex is the free generator $\mathrm{gen},X,n,s$: after rewriting through toChain_asimplex and this lemma, Equiv.symm_apply_apply finishes. That identity is the base case against which nontrivial face and cone pushes are compared when building subdivided chains. In the Recognition foundation stack this sits under the singular-homology scaffolding that supports discrete geometric forcing (eight-tick octave, $D=3$), not a forcing-chain step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.