sbary_affineMap
plain-language theorem explainer
Affine maps of standard simplices send barycenters of point-tuples to barycenters of the image tuples. Anyone proving equivariance of barycentric subdivision (or its prism homotopy) under pushforward of singular simplices cites this intertwining identity. The argument is coordinatewise: expand both sides by the barycenter average formula and commute finite sums.
Claim. Let $v$ be an $(n+1)$-tuple of points in the standard $d$-simplex $\Delta^d$, determining the affine map $A_v:\Delta^n\to\Delta^d$. For any $(m+1)$-tuple $w$ of points in $\Delta^n$, the barycenter of the image points equals the image of the barycenter: $\overline{A_v\circ w}=A_v(\overline{w})$.
background
The module builds singular barycentric subdivision on Mathlib's singular chain complex by first working in an affine layer on standard simplices, then transporting identities along a singular simplex $\sigma:\Delta^n\to X$. Stage 5a supplies equivariance lemmas that move affine identities to singular chains; those lemmas need affine maps to preserve barycenters.
Here $\mathrm{sbary}$ is the barycenter of a finite tuple of points in a standard simplex: the coordinatewise average with weight $(m+1)^{-1}$. The map $A_v$ is the unique affine map $\Delta^n\to\Delta^d$ sending the standard vertices to the tuple $v$. Both live in the Geometry section that precedes the singular operators sdOp and tOp.
The local setting is classical convex geometry inside $\Delta^\bullet\subset\mathbb{R}^{\bullet+1}$: no Recognition-cost or forcing-chain hypotheses appear in the statement itself.
proof idea
Pointwise equality of points in a standard simplex is reduced by stdSimplex.ext and funext on the ambient coordinate index $j$. Both sides become the same weighted sum: left is the average of the $j$-th coordinates of $A_v(w_i)$; right is the $j$-th coordinate of $A_v$ applied to the barycenter of $w$.
Unfolding the coordinate formulas for the affine map and for the barycenter, then using mul_assoc, distributing the scalar through the sum, and commuting the double finite sum (Finset.sum_comm), makes the two expressions identical. No induction on dimension and no topology beyond the simplex embedding.
why it matters
This is the geometric intertwining fact named in the doc-comment as required by the stage-5a equivariance lemmas. Downstream it is consumed by gen_pushSimplex_comp_sdOp ("sdOp on a pushed generator computes the subdivision of the pushed tuple") and gen_pushSimplex_comp_tOp (the analogous identity for the prism homotopy tOp).
Those two lemmas are the heart of transporting affine subdivision and its chain homotopy onto Mathlib singular chains: once barycenters commute with affine pushforward, the subdivided identity tuple pushed along $\sigma$ matches applying the singular operators to the pushed generator. In the broader Foundation stack this closes the geometric step that lets singular subdivision act as a chain-level operator, feeding later continuum-bridge and ledger constructions that sit above the affine layer.
It does not itself invoke the forcing chain (T0–T8), RCL, or $\varphi$-ladder; it is pure simplex geometry supporting those later stages.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.