affineMap_comp_idTuple
plain-language theorem explainer
Composing the affine map determined by a vertex tuple v with the identity vertex tuple recovers v pointwise. Algebraic topologists working the singular subdivision operators cite this when transporting generators under pushforward. The proof is a one-line funext reduction to the vertex-evaluation lemma for affine maps.
Claim. For any vertex tuple $v : \mathrm{Fin}(n+1) \to \Delta^m$, the continuous affine map $\Delta^n \to \Delta^m$ determined by $v$, composed with the identity vertex tuple of $\Delta^n$, equals $v$ as functions on $\mathrm{Fin}(n+1)$.
background
In the singular subdivision module one works with continuous maps out of standard simplices $\Delta^k \subset \mathbb{R}^{k+1}$. An affine map $\Delta^n \to \Delta^m$ is completely determined by where it sends the $n+1$ vertices: given a tuple $v : \mathrm{Fin}(n+1) \to \Delta^m$, the construction affineMap produces the unique continuous affine map sending the $i$-th vertex of $\Delta^n$ to $v,i$.
The identity vertex tuple is the map $i \mapsto$ the $i$-th standard vertex of $\Delta^n$. The companion lemma that the affine map evaluates on vertices exactly to the prescribed points is already proved by reducing the barycentric combination to a single summand.
This sits in the foundation layer that builds barycentric subdivision and prism operators on singular chains, feeding the transport of generators under pushforward of simplices.
proof idea
Term-mode proof by function extensionality: it suffices to check equality at each index $i : \mathrm{Fin}(n+1)$. At index $i$ the left-hand side is the affine map applied to the $i$-th standard vertex, which equals $v,i$ by the vertex-evaluation lemma for affine maps. No further rewriting is required.
why it matters
This identity is the bookkeeping step that lets pushforward of a generator commute with the subdivision and prism operators. Downstream it is used in the two transport lemmas: subdivision of a pushed generator equals the chain obtained by subdividing the pushed vertex tuple, and likewise for the prism/homotopy operator. Without recovering the original tuple after composing with the identity vertices, the simplex-equivalence rewrites in those proofs would not close.
In the broader Recognition foundation this is pure singular-homology scaffolding (barycentric subdivision, chain homotopy to the identity), not a forcing-chain step. It keeps the geometric operators on generators honest so later homology arguments can treat subdivision as a chain map up to homotopy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.