The barycentric identification for stellar subdivision

Place the new vertex of a stellar subdivision at the barycenter of the starred face, fixing all other vertices, and extend linearly in barycentric coordinates. This map identifies the subdivided polyhedron bijectively with the original polyhedron. The complexes may be infinite and may have unused vertices. This is the point-set identification; no topology on the precomplex polyhedra or piecewise-linear compatibility is asserted here.

The module supplies the linear map, its coordinate and vertex formulas, mass preservation, and its image, injectivity, and surjectivity properties on the corresponding polyhedra. Together these give a point-set identification for the geometric realization of a stellar move.

References

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

The coordinate construction follows the barycentric map in TauCeti.AlgebraicTopology.SimplicialComplex.Subdivision.Realization, using the same Mathlib Geometry.SimplicialComplex.onFinsupp realization.

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

Replace the coordinate vector of v by the normalized coordinate sum over σ, fixing all other vertices. This sum is the barycenter when σ is nonempty, and zero when σ is empty. On the stellar subdivision at σ with fresh vertex v, this is the barycentric realization map to the original polyhedron.

Equations

• σ.stellarSubdivisionLinearMap v = LinearMap.id + (Finsupp.lapply v).smulRight (∑ i ∈ σ, Finsupp.single i (↑σ.card)⁻¹ - Finsupp.single v 1)

@[simp]

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

The coordinate formula for the stellar realization map.

@[simp]

theorem Finset.stellarSubdivisionLinearMap_single_of_ne {ι : Type u_1} {σ : Finset ι} {v w : ι} (hw : w ≠ v) (r : ℝ) : (σ.stellarSubdivisionLinearMap v) (Finsupp.single w r) = Finsupp.single w r

Every old vertex is fixed by the realization map.

@[simp]

theorem Finset.stellarSubdivisionLinearMap_single {ι : Type u_1} {σ : Finset ι} {v : ι} : (σ.stellarSubdivisionLinearMap v) (Finsupp.single v 1) = ∑ i ∈ σ, Finsupp.single i (↑σ.card)⁻¹

The coordinate vector of v is sent to the normalized coordinate sum over σ, which is the barycenter when σ is nonempty, and zero when σ is empty.

@[simp]

theorem Finset.sum_stellarSubdivisionLinearMap {ι : Type u_1} {σ : Finset ι} {v : ι} (hσ : σ.Nonempty) (x : ι →₀ ℝ) : (((σ.stellarSubdivisionLinearMap v) x).sum fun (x : ι) (r : ℝ) => r) = x.sum fun (x : ι) (r : ℝ) => r

The stellar realization map preserves total barycentric mass when the starred face is nonempty.

theorem PreAbstractSimplicialComplex.mapsTo_stellarSubdivisionLinearMap {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hvσ : v ∉ σ) : Set.MapsTo (⇑(σ.stellarSubdivisionLinearMap v)) (Geometry.SimplicialComplex.onFinsupp (K.stellarSubdivision σ v)).space (Geometry.SimplicialComplex.onFinsupp K).space

The barycentric map sends the stellar polyhedron into the original polyhedron.

theorem PreAbstractSimplicialComplex.injOn_stellarSubdivisionLinearMap {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hvσ : v ∉ σ) : Set.InjOn (⇑(σ.stellarSubdivisionLinearMap v)) (Geometry.SimplicialComplex.onFinsupp (K.stellarSubdivision σ v)).space

The barycentric map is injective on the stellar polyhedron when the new vertex lies outside the starred face.

theorem PreAbstractSimplicialComplex.surjOn_stellarSubdivisionLinearMap {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hσ : σ ∈ K) (hv : {v} ∉ K) : Set.SurjOn (⇑(σ.stellarSubdivisionLinearMap v)) (Geometry.SimplicialComplex.onFinsupp (K.stellarSubdivision σ v)).space (Geometry.SimplicialComplex.onFinsupp K).space

Every point of the original polyhedron has a preimage in the stellar polyhedron when the starred face belongs to the original complex and the new vertex is unused.

theorem PreAbstractSimplicialComplex.bijOn_stellarSubdivisionLinearMap {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hσ : σ ∈ K) (hv : {v} ∉ K) : Set.BijOn (⇑(σ.stellarSubdivisionLinearMap v)) (Geometry.SimplicialComplex.onFinsupp (K.stellarSubdivision σ v)).space (Geometry.SimplicialComplex.onFinsupp K).space

Placing the new vertex at the barycenter identifies the polyhedron of a stellar subdivision bijectively with the original polyhedron. No finiteness assumption is needed.