affineMapFun
plain-language theorem explainer
Defines the barycentric combination map sending a point x in the standard n-simplex to the weighted sum of a prescribed vertex tuple in the m-simplex. Anyone building continuous affine maps Δⁿ → Δᵐ, or proving those maps land in the simplex, cites this raw coordinate formula. The body is the explicit sum ∑ᵢ xᵢ · vᵢ in barycentric coordinates.
Claim. Given vertices $v_0,\ldots,v_n$ in the standard $m$-simplex $\Delta^m$ and a point $x\in\Delta^n$, define the map $x\mapsto \sum_{i=0}^{n} x_i\, v_i$ as an $\mathbb{R}^{m+1}$-valued function (barycentric combination of the $v_i$).
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 ordered $(n+1)$-tuple of points in $\Delta^m$ determines a unique affine map $\Delta^n\to\Delta^m$ by sending the $i$-th vertex of $\Delta^n$ to the $i$-th prescribed point and extending by barycentric weights.
This definition isolates the underlying set-theoretic formula before packaging it as a continuous map of subtypes. Downstream lemmas then check that the image stays inside $\Delta^m$ and that the map is continuous in the subspace topology. The module sits under Foundation and imports Mathlib singular homology and convex-analysis primitives, so the construction is classical AT infrastructure rather than an RS-specific forcing step.
proof idea
Pure definition: the body is the coordinatewise sum fun j => ∑ i, x i * v i j. No lemmas are applied; the formula is the content. Continuity and simplex-membership are proved separately for this function.
why it matters
This is the raw kernel of the packaged continuous affine map affineMap, which builds C(Δⁿ, Δᵐ) from a vertex tuple. The membership lemma affineMapFun_mem and the continuity lemma continuous_affineMapFun both quote this function directly, then affineMap assembles them into a ContinuousMap via subtype packaging.
In the Recognition Foundation stack, singular subdivision supplies the simplicial machinery used when comparing chains, cones, and prism operators (siblings such as acone, abnd, eps). The declaration itself is classical barycentric geometry; its place in the monorepo is to keep the affine-extension step explicit and reusable before higher singular-homology constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.