Barycenters of faces under maps of vertices

Mathlib's Convexity.StdSimplex.subBarycenter S hS is the barycenter of the face of a standard simplex spanned by a nonempty finite set S of vertices. This file records that an injective map of vertices, acting on the standard simplex by Convexity.StdSimplex.map, sends the barycenter of the face spanned by S to the barycenter of the face spanned by the image of S. For instance, the inclusion of a facet of the standard simplex sends barycenters of faces of the facet to barycenters of the corresponding faces of the simplex, which is how barycentric subdivision restricts to faces.

theorem Convexity.StdSimplex.subBarycenter_congr {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {S T : Finset M} (h : S = T) (hS : S.Nonempty) : subBarycenter S hS = subBarycenter T ⋯

Replacing the finite set in a face barycenter by an equal set does not change the barycenter.

@[simp]

theorem Convexity.StdSimplex.map_subBarycenter {K : Type u_1} {M : Type u_2} {N : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (f : M ↪ N) (S : Finset M) (hS : S.Nonempty) : map (⇑f) (subBarycenter S hS) = subBarycenter (Finset.map f S) ⋯

An injective map of vertices sends the barycenter of the face spanned by S to the barycenter of the face spanned by the image of S.