affineMap
plain-language theorem explainer
Continuous affine map Δⁿ → Δᵐ fixed by a vertex tuple in the target simplex, sending the i-th source vertex to the prescribed point. Singular-chain and barycentric-subdivision arguments cite it as the basic geometric morphism of simplices. The definition packages the barycentric combination into a ContinuousMap via the underlying sum, a membership proof, and a continuity lemma.
Claim. Given points $v_0,\ldots,v_n$ in the standard $m$-simplex $\Delta^m$, there is a continuous map $f_v:\Delta^n\to\Delta^m$ with $f_v(x)=\sum_i x_i\,v_i$ in barycentric coordinates, sending the $i$-th vertex of $\Delta^n$ to $v_i$.
background
The ambient objects are standard geometric simplices $\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},(k+1))$, the sets of nonnegative barycentric weight vectors summing to one. An ordered $(n+1)$-tuple of points in $\Delta^m$ determines a unique affine map $\Delta^n\to\Delta^m$ by extending the vertex assignment linearly in those coordinates.
The underlying point map is the barycentric combination $x\mapsto\sum_i x_i,v_i$ (componentwise on the ambient $\mathbb{R}^{m+1}$). Upstream lemmas show that this combination stays inside the target simplex and is continuous as a map of topological spaces. The present definition packages that data as an element of the continuous-map type $C(\Delta^n,\Delta^m)$.
The module sits in the singular-subdivision layer of the foundation: it supplies the geometric maps used to build cones, prisms, and barycentric subdivisions of singular simplices, feeding later chain-level constructions.
proof idea
Definitional packaging, not a tactic proof. The toFun field is the subtype pair of the barycentric sum affineMapFun v x with the membership lemma affineMapFun_mem. Continuity of the ContinuousMap is obtained by applying Continuous.subtype_mk to the already-proved continuity of affineMapFun. No further algebraic work occurs at this site.
why it matters
This is the basic geometric arrow for the singular-subdivision toolkit. Downstream results use it for functoriality (composite of affine maps equals the affine map of the pushed vertex tuple), identity behaviour (affine map of the identity tuple is the identity continuous map), face restriction (composition with a topological face inclusion restricts the vertex tuple along succAbove), vertex evaluation, and hull membership (the image lands in the convex hull of the vertex tuple).
Those lemmas are the geometric substrate for prism and cone operators and for controlled subdivision of singular simplices. In the Recognition Science foundation they support the chain-level constructions that eventually interface with the eight-tick octave and dimensional forcing, though this declaration itself is pure simplex geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.