Coordinates of polyhedra with unused vertices

The standard polyhedron of a precomplex consists of nonnegative barycentric coordinates summing to one whose support is a face. Unlike an abstract complex on a fixed vertex type, a precomplex can leave vertices unused. This characterization therefore applies to geometric moves which add or remove vertices, including stellar subdivision and elementary collapse.

The construction reuses Mathlib's Geometry.SimplicialComplex.onFinsupp and the standard simplex coordinate API in Realization.Basic.

@[simp]

theorem Geometry.SimplicialComplex.mem_space_onFinsupp_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {x : ι →₀ ℝ} : x ∈ (onFinsupp K).space ↔ (∀ (i : ι), 0 ≤ x i) ∧ (x.sum fun (x : ι) (r : ℝ) => r) = 1 ∧ x.support ∈ K

A point of the standard polyhedron has nonnegative coordinates summing to one and support a face, including for precomplexes with unused vertices.