Geometric simplices of a stellar subdivision

Placing a new vertex at the barycenter of the starred face gives nondegenerate geometric simplices, meeting along their common faces. On each subdivided simplex the barycentric identification has a linear inverse: choose a vertex of the starred face omitted by that simplex, and recover the transferred mass from its coordinate.

These simplex inverse formulas and affine independence checks allow the barycentric identification to be treated as a simplicial PL map, rather than merely a bijection of polyhedra. The complexes and ambient vertex types need not be finite.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2 (geometric starrings).

noncomputable def Finset.stellarSubdivisionInverseLinearMap {ι : Type u_1} (σ : Finset ι) (v a : ι) : (ι →₀ ℝ) →ₗ[ℝ] ι →₀ ℝ

The linear inverse formula for a stellar simplex omitting the vertex a of the starred face: transfer the a-coordinate back from that face to the new vertex v.

@[simp]

theorem Finset.stellarSubdivisionInverseLinearMap_apply {ι : Type u_1} [DecidableEq ι] (σ : Finset ι) (v a : ι) (x : ι →₀ ℝ) (i : ι) : ((σ.stellarSubdivisionInverseLinearMap v a) x) i = x i + x a * ((if i = v then ↑σ.card else 0) - if i ∈ σ then 1 else 0)

The inverse on a stellar simplex subtracts equal mass on the starred face and adds its sum at the new vertex.

@[simp]

theorem Finset.stellarSubdivisionInverseLinearMap_left_inv {ι : Type u_1} {σ : Finset ι} {v a : ι} (ha : a ∈ σ) {x : ι →₀ ℝ} (hxa : x a = 0) : (σ.stellarSubdivisionInverseLinearMap v a) ((σ.stellarSubdivisionLinearMap v) x) = x

If the coordinate at a vertex of the starred face vanishes, its linear inverse formula recovers the original vector after the stellar barycentric map.

theorem Finset.stellarSubdivisionInverseLinearMap_left_inv_on_simplex {ι : Type u_1} {σ τ : Finset ι} {v a : ι} (ha : a ∈ σ) (haτ : a ∉ τ) : Set.EqOn (⇑(σ.stellarSubdivisionInverseLinearMap v a) ∘ ⇑(σ.stellarSubdivisionLinearMap v)) id ((convexHull ℝ) ((fun (i : ι) => Finsupp.single i 1) '' ↑τ))

The inverse formula works on the entire simplex whenever the simplex omits the chosen vertex of the starred face.

theorem Finset.affineIndependent_stellarSubdivisionLinearMap {ι : Type u_1} {σ τ : Finset ι} {v a : ι} (ha : a ∈ σ) (haτ : a ∉ τ) : AffineIndependent ℝ fun (i : ↥τ) => (σ.stellarSubdivisionLinearMap v) (Finsupp.single (↑i) 1)

The barycentric images of the vertices of a simplex omitting a vertex of the starred face are affinely independent.

theorem PreAbstractSimplicialComplex.exists_linearMap_leftInverse_stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ τ : Finset ι} {v : ι} (hvσ : v ∉ σ) (hτ : τ ∈ K.stellarSubdivision σ v) : ∃ (L : (ι →₀ ℝ) →ₗ[ℝ] ι →₀ ℝ), Set.EqOn (⇑L ∘ ⇑(σ.stellarSubdivisionLinearMap v)) id ((convexHull ℝ) ((fun (i : ι) => Finsupp.single i 1) '' ↑τ))

Every simplex of the stellar subdivision admits a linear inverse to its barycentric identification on the whole simplex.

theorem PreAbstractSimplicialComplex.affineIndependent_stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ τ : Finset ι} {v : ι} (hvσ : v ∉ σ) (hτ : τ ∈ K.stellarSubdivision σ v) : AffineIndependent ℝ fun (i : ↥τ) => (σ.stellarSubdivisionLinearMap v) (Finsupp.single (↑i) 1)

Placing the fresh vertex at the barycenter gives affinely independent vertices on every face of the stellar subdivision.

theorem PreAbstractSimplicialComplex.convexHull_stellarSubdivision_inter {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ τ ρ : Finset ι} {v : ι} (hvσ : v ∉ σ) (hτ : τ ∈ K.stellarSubdivision σ v) (hρ : ρ ∈ K.stellarSubdivision σ v) : (convexHull ℝ) ((fun (i : ι) => (σ.stellarSubdivisionLinearMap v) (Finsupp.single i 1)) '' ↑τ) ∩ (convexHull ℝ) ((fun (i : ι) => (σ.stellarSubdivisionLinearMap v) (Finsupp.single i 1)) '' ↑ρ) = (convexHull ℝ) ((fun (i : ι) => (σ.stellarSubdivisionLinearMap v) (Finsupp.single i 1)) '' (↑τ ∩ ↑ρ))

Two geometric stellar simplices meet exactly in the simplex spanned by their common vertices. Thus the barycentric placement is a geometric triangulation, not merely a collection of nondegenerate simplices with the correct union.

noncomputable def PreAbstractSimplicialComplex.geometricStellarSubdivision {ι : Type u_1} [DecidableEq ι] (K : PreAbstractSimplicialComplex ι) (σ : Finset ι) (v : ι) (hvσ : v ∉ σ) : Geometry.SimplicialComplex ℝ (ι →₀ ℝ)

The geometric stellar subdivision, placing v at the barycenter of σ and retaining the standard positions of the other vertices. Its face collection is the image of the abstract stellar subdivision under that placement.

@[simp]

theorem PreAbstractSimplicialComplex.mem_geometricStellarSubdivision_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hvσ : v ∉ σ) {s : Finset (ι →₀ ℝ)} : s ∈ (K.geometricStellarSubdivision σ v hvσ).faces ↔ ∃ τ ∈ K.stellarSubdivision σ v, Finset.image (fun (i : ι) => (σ.stellarSubdivisionLinearMap v) (Finsupp.single i 1)) τ = s

The geometric stellar faces are exactly the barycentric images of the abstract stellar faces.

@[simp]

theorem PreAbstractSimplicialComplex.space_geometricStellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hσ : σ ∈ K) (hv : {v} ∉ K) : (K.geometricStellarSubdivision σ v ⋯).space = (Geometry.SimplicialComplex.onFinsupp K).space

A genuine geometric starring leaves the underlying polyhedron unchanged.