affineMap_apply_coe
plain-language theorem explainer
Coordinate formula for the affine map Δⁿ→Δᵐ determined by a vertex tuple v: the j-th barycentric coordinate of the image of x is the convex combination ∑ᵢ xᵢ·(vᵢ)ⱼ. Anyone proving identities about singular subdivision, barycenters, or hull membership cites this simp lemma. The proof is pure definitional equality (rfl).
Claim. Let $v$ assign to each vertex of the standard $n$-simplex a point of the standard $m$-simplex, and let $x\in\Delta^n$. Then the $j$-th barycentric coordinate of the affine image of $x$ equals $\sum_i x_i\, v_i(j)$.
background
The ambient setting is singular subdivision of standard simplices over $\mathbb{R}$. The standard simplex $\Delta^k\subset\mathbb{R}^{k+1}$ consists of nonnegative barycentric coordinates summing to 1. An affine map $\Delta^n\to\Delta^m$ is completely determined by where it sends the $n+1$ vertices.
Upstream, affineMap packages that data: given a tuple $v:\mathrm{Fin}(n+1)\to\Delta^m$, it builds the continuous map whose underlying function is the barycentric combination $x\mapsto\sum_i x_i\cdot v_i$, already proved to land back in $\Delta^m$. This lemma simply exposes the $j$-th coordinate of that combination as a bare real sum, which is the form needed by later algebraic identities.
proof idea
Term-mode proof by rfl. The continuous-map value affineMap v x is definitionally the subtype package of affineMapFun v x, whose $j$-th coordinate is already $\sum_i x_i\cdot v_i j$. Unfolding the coercion therefore yields the stated sum with no further rewriting.
why it matters
This is the workhorse simp rule for every subsequent identity about affine maps in SingularSubdivision. Downstream it discharges the coordinate steps in: functoriality of composition (affineMap_comp), the identity-tuple case (affineMap_idTuple), vertex evaluation (affineMap_vertex), hull membership (affineMap_mem_hullOf), and barycenter intertwining (sbary_affineMap). Those lemmas underwrite the equivariance and subdivision machinery used later in the foundation layer. The declaration itself is pure linear algebra on simplices; it does not invoke the forcing chain (T0–T8) or the Recognition Composition Law, but it is infrastructure those geometric constructions rely on once singular chains enter the picture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.