idTuple
plain-language theorem explainer
The identity vertex tuple sends each standard basis index i in Fin(n+1) to the i-th vertex of the standard n-simplex. It is the reference vertex configuration for affine subdivision and for pushing singular simplices. Anyone citing singular subdivision, the small-simplices theorem, or Mayer–Vietoris span preservation uses it as the base generator. The body is a one-line pointwise assignment to stdSimplex.vertex.
Claim. For each $n \in \mathbb{N}$, define the identity vertex tuple $\mathrm{idTuple}(n) : \mathrm{Fin}(n+1) \to \Delta^n$ by $i \mapsto e_i$, where $e_i$ is the $i$-th vertex of the standard $n$-simplex $\Delta^n = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}(n+1))$.
background
Singular subdivision in this module builds chain-level operators from affine geometry on the standard simplex. A vertex tuple is a map from $\mathrm{Fin}(n+1)$ into $\Delta^n$ (or a higher simplex); the associated affine map is the unique affine extension sending vertices to the listed points. The identity tuple is the canonical choice: each formal vertex lands on the geometric vertex of the same index.
The module sits in the Foundation layer that develops singular chains, barycentric subdivision, and support-control lemmas needed for Mayer–Vietoris arguments on covers. Downstream, iterated affine subdivision is applied to the affine simplex of this identity tuple, then pushed forward along a singular simplex to control ranges relative to open sets $U,V$.
Sibling constructions (affine maps of tuples, cone and boundary operators on affine simplices, barycentric iteration) all treat this tuple as the unit of the vertex-configuration monoid under composition with affine maps.
proof idea
Definitional one-liner: pointwise, index $i$ is sent to stdSimplex.vertex i. No lemmas are invoked; noncomputability is inherited from the ambient simplex API. Immediate consequences (proved elsewhere) are that the affine map of this tuple is the continuous identity on $\Delta^n$, and that composing any vertex tuple’s affine map with this identity tuple recovers the original tuple.
why it matters
This is the base configuration for Stage 6–7 singular subdivision. gen_comp_sdOpIter states that iterated singular subdivision of a generator equals evaluation of iterated affine subdivision of the affine simplex on the identity tuple, tying the singular operator to affine support geometry. The small-simplices theorem exists_sdOpIter_small quantifies over the support of that iterated subdivision of asimplex (idTuple n) to force every pushed piece into $U$ or $V$.
Mayer–Vietoris lemmas sdOp_mem_smallSpan and tOp_mem_smallSpan inherit that geometry when showing subdivision and the subdivision homotopy preserve the small-span submodule. Locally, affineMap_idTuple and affineMap_comp_idTuple make the identity tuple the unit for affine-map composition. In the broader RS foundation this is pure algebraic topology scaffolding for cover arguments, not a forcing-chain (T0–T8) step, but it underwrites the chain-level machinery those geometric claims rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.