affineMap_idTuple
plain-language theorem explainer
The affine map induced by the identity vertex tuple on the standard n-simplex is the identity continuous map. Singular-homology and subdivision arguments cite this to cancel identity pushes. The proof is coordinatewise: the barycentric sum collapses to a single term via Finset.sum_eq_single, then mul_one and mul_zero.
Claim. For every $n \in \mathbb{N}$, the affine map associated to the identity $(n+1)$-tuple of vertices of the standard simplex equals the identity continuous map $\mathrm{id}\colon \Delta^n \to \Delta^n$, where $\Delta^n = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}(n+1))$.
background
The module develops singular subdivision infrastructure: affine maps of tuples of points in a convex set, pushforwards of singular simplices, and cone/prism constructions used to compare chains. The standard $n$-simplex $\Delta^n \subset \mathbb{R}^{n+1}$ consists of nonnegative coordinates summing to one. An $(n+1)$-tuple of points determines an affine map $\Delta^n \to X$ by barycentric combination; the identity tuple is the ordered list of standard basis vertices of $\Delta^n$ itself.
Locally one needs that this identity tuple induces the identity continuous map on $\Delta^n$, so that composing a singular simplex with that affine map does nothing. Upstream arithmetic facts used in the coordinate calculation are the ordinary identities $x\cdot 1 = x$ and $x\cdot 0 = 0$ (here via Mathlib mul_one / mul_zero on $\mathbb{R}$).
proof idea
Apply continuous-map extensionality, then simplex extensionality, reducing to equality of real coordinates at each $j$. Unfold the affine-map evaluation to a finite sum over barycentric weights times vertex coordinates. Invoke Finset.sum_eq_single j: the matching term is $x_j \cdot (\mathrm{Pi.single}, j, 1)_j = x_j \cdot 1 = x_j$; every off-diagonal term is $x_b \cdot 0 = 0$ by Pi.single_eq_of_ne; the missing-index case is absurd because $j$ lies in the universe. No external RS lemmas beyond these arithmetic identities are required.
why it matters
Feeds directly into pushSimplex_idTuple, whose doc-comment states that the pushed simplex of the identity tuple is the simplex itself: after unfolding pushSimplex, one rewrites by this lemma and cancels with ContinuousMap.comp_id. That identity is the base case for subdivision and prism operators in the singular-chain complex, which the Foundation layer uses when comparing geometric realizations and when transporting recognition data along simplicial maps. It is pure algebraic-topology scaffolding rather than a T0–T8 forcing step, but it keeps the singular-homology side of the monolith free of ad-hoc identity rewrites.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.