affineMap_comp
plain-language theorem explainer
Functoriality of affine maps on standard simplices: the composite of the maps induced by vertex tuples v and w equals the affine map of the pushed vertices i ↦ v_*(w i). Cited when building singular chains, face restrictions, or barycentric subdivision. Proof is pointwise coordinate algebra after ContinuousMap.ext: double sums rearrange by sum_comm and ring.
Claim. Let $v$ assign to each vertex of $\Delta^n$ a point of $\Delta^m$, and $w$ assign to each vertex of $\Delta^k$ a point of $\Delta^n$. Write $A_v:\Delta^n\to\Delta^m$ and $A_w:\Delta^k\to\Delta^n$ for the induced continuous affine maps. Then $A_v\circ A_w=A_{v\circ w}$, where $(v\circ w)_i:=A_v(w_i)$.
background
The module develops singular subdivision for Recognition Science foundations, importing Mathlib singular homology and the local prism toolkit. An affine map on standard simplices is the continuous map $A_v:\Delta^n\to\Delta^m$ determined by a vertex tuple $v:\mathrm{Fin}(n+1)\to\Delta^m$: it sends the $i$-th vertex of $\Delta^n$ to $v_i$ and extends by barycentric coordinates.
Coordinatewise, $(A_v x)_j=\sum_i x_i,v_i(j)$. That identity is the simp lemma used throughout the file. Composition of continuous maps is the usual $C(X,Y)$ composition; the claim is that this operation is compatible with the vertex-tuple presentation of affine maps.
Upstream, the definition of the affine map packages the barycentric formula into a ContinuousMap between standard simplices. The apply-coe lemma exposes the sum formula needed for algebraic rearrangement.
proof idea
Term-mode proof via ContinuousMap.ext, then stdSimplex.ext and funext on the target barycentric coordinate $j$. The goal becomes equality of two real sums. Unfold with affineMap_apply_coe, expand products of sums (Finset.sum_mul, Finset.mul_sum), commute the double sum (Finset.sum_comm), and finish each summand by ring. No external named lemmas beyond the local apply-coe identity.
why it matters
This is the associativity/functoriality step for affine maps on simplices inside the singular-subdivision stack. Downstream, affineMap_comp_face specializes it to topological face inclusions: composing $A_v$ with a face map restricts the vertex tuple along Fin.succAbove. The chain-level lemma toChain_amap uses the same compatibility so that toChain turns affine pushforward into precomposition of singular simplices.
In the broader Recognition foundation, singular chains and prism operators support discrete geometric constructions (octave/tick structure, interface geometry) that sit under the forcing chain. The result itself is pure convex-geometry algebra; it does not invoke J-cost, $\phi$, or T5–T8, but it is infrastructure those geometric layers rely on when they talk in singular homology language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.