simplexEquiv_pushSimplex
plain-language theorem explainer
Applying the singular-simplex equivalence to a pushed simplex recovers precomposition of σ with the affine map of the vertex tuple w. Anyone transporting subdivision or prism operators through generators cites this identity. The proof is a one-line application of Equiv.apply_symm_apply, undoing the definition of pushSimplex.
Claim. Let $\sigma:\Delta^n\to X$ be a continuous singular $n$-simplex and let $w:\mathrm{Fin}(m+1)\to\Delta^n$ be a vertex tuple. If $\mathrm{push}(\sigma,w)$ denotes the singular $m$-simplex obtained by precomposing $\sigma$ with the affine map $A_w:\Delta^m\to\Delta^n$ determined by $w$, then under the canonical equivalence between indexed singular $m$-simplices and continuous maps $\Delta^m\to X$ one has $\mathrm{push}(\sigma,w)\simeq\sigma\circ A_w$.
background
The module builds barycentric subdivision and prism operators on singular chains of a topological space $X$, in the Mathlib singular-homology setting. A singular $n$-simplex is a continuous map $\sigma:\Delta^n\to X$ from the standard geometric simplex. Indexed simplices Idx X m are identified with such maps by an equivalence simplexEquiv.
Given a vertex tuple $w:\mathrm{Fin}(m+1)\to\Delta^n$, affineMap w is the unique affine continuous map $A_w:\Delta^m\to\Delta^n$ sending the $i$-th vertex of $\Delta^m$ to $w(i)$. The operation pushSimplex σ w is defined by transporting $\sigma\circ A_w$ back along simplexEquiv: it is the singular $m$-simplex obtained by precomposing $\sigma$ with that affine piece.
This lemma is the immediate inverse identity: evaluating the equivalence on a pushed simplex recovers the continuous composition used in the definition.
proof idea
By definition, pushSimplex σ w is (simplexEquiv X m).symm (σ.comp (affineMap w)). The claim is exactly Equiv.apply_symm_apply for that equivalence applied to σ.comp (affineMap w). Term-mode one-liner; no further lemmas.
why it matters
This is the bookkeeping identity that lets every later transport of subdivision and prism operators through generators rewrite in terms of ordinary continuous precomposition. Downstream, gen_pushSimplex_comp_sdOp and gen_pushSimplex_comp_tOp use it so that sdOp and tOp on a pushed generator equal the affine subdivision (resp. prism) of the pushed vertex tuple, evaluated via toChain. The same rewrite appears in toChain_amap and toChain_asimplex.
On the geometric side, small_pushSimplex invokes it to prove that smallness (range inside an open of a cover) is inherited under affine push, which is the local step in the Stage-7 small-simplices theorem exists_sdOpIter_small: after enough barycentric iterates, every piece of a subdivided singular simplex lies in one set of an open cover. That theorem is the singular-homology input to Mayer–Vietoris arguments in SingularMayerVietoris. In the Recognition foundation stack this is pure continuum scaffolding for the simplicial ledger bridge, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.