Finite stellar subdivisions preserve the weak polyhedron

Placing a new vertex at the barycenter of the starred face gives a homeomorphism from the polyhedron of a finite stellar subdivision to the original polyhedron. Consequently a finite sequence of stellar moves and inverse moves preserves the homeomorphism type of a finite polyhedron. These identifications provide the topological part of the local sphere and ball models used in triangulated manifolds; piecewise-linear regularity is a separate assertion.

A precomplex can omit vertices, so its polyhedron is the subset of an ambient weak realization whose supports are its faces. The single-move theorem allows any ambient complex containing both precomplexes. The sequence theorem uses the full complex as a common ambient space. Finiteness means finitely many faces, with no restriction on the ambient vertex type.

The construction uses the bijective barycentric map of Stellar.Realization and the compact subpolyhedron and coordinate-embedding theorems of Realization.Finite.

References

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

theorem PreAbstractSimplicialComplex.exists_homeomorph_stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {A : AbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hσ : σ ∈ K) (hv : {v} ∉ K) (hfin : K.faces.Finite) (hK : K ≤ A.toPreAbstractSimplicialComplex) (hS : K.stellarSubdivision σ v ≤ A.toPreAbstractSimplicialComplex) : ∃ (e : { x : A.Realization // (↑x).support ∈ K.stellarSubdivision σ v } ≃ₜ { x : A.Realization // (↑x).support ∈ K }), ∀ (x : { x : A.Realization // (↑x).support ∈ K.stellarSubdivision σ v }), ↑↑(e x) = (σ.stellarSubdivisionLinearMap v) ↑↑x

The barycentric identification of a finite stellar subdivision is a homeomorphism for the weak subpolyhedron topologies. The new vertex goes to the barycenter of σ and the old vertices are fixed, as specified by the underlying linear map.

theorem PreAbstractSimplicialComplex.StellarEquivalent.nonempty_homeomorph {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalent L) (hfin : K.faces.Finite) : Nonempty ({ x : ⊤.Realization // (↑x).support ∈ K } ≃ₜ { x : ⊤.Realization // (↑x).support ∈ L })

Stellar equivalent finite precomplexes have homeomorphic weak polyhedra. The subtypes exclude every unused vertex, even though their common ambient complex contains all vertices.