PL charts on open vertex stars with spherical links

A vertex with a combinatorial sphere as link has a Euclidean PL chart on its entire open star. Its target is the interior of the coordinate simplex. Both the chart and its inverse admit ambient PL formulas, suitable for checking transitions between vertex-star charts. Neither the complex nor its vertex type needs to be finite.

The closed-star simplex model sends the apex coordinate to a positive multiple of the minimum barycentric coordinate. Thus the open star corresponds exactly to the interior of the simplex. Dropping the last barycentric coordinate gives Euclidean coordinates; the inverse restores it as one minus the sum of the retained coordinates.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapters 2–3 (pseudo-radial projection and vertex-star charts).

The construction uses IsCombinatorialSphere.exists_homeomorph_closedStarRealization_top and AbstractSimplicialComplex.realizationTopHomeomorphCoordinateSimplex.

theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.exists_openPartialHomeomorph_openStar_isPL {ι : Type u_1} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {v : ι} {n : ℕ} (h : (K.link {v}).IsCombinatorialSphere n) : ∃ (c : OpenPartialHomeomorph K.Realization (Fin (n + 1) → ℝ)), c.source = K.openStarRealization v ∧ c.target = interior (TauCeti.coordinateSimplex (Fin (n + 1))) ∧ (↑c (K.vertex v) = fun (x : Fin (n + 1)) => (↑n + 2)⁻¹) ∧ ∃ (F : (ι → ℝ) → Fin (n + 1) → ℝ) (G : (Fin (n + 1) → ℝ) → ι → ℝ), TauCeti.IsPLOn F (Set.range fun (x : ↑(K.closedStarRealization {v})) => ⇑↑↑x) ∧ TauCeti.IsPLOn G c.target ∧ (∀ x ∈ c.source, F ⇑↑x = ↑c x) ∧ ∀ y ∈ c.target, G y = ⇑↑(↑c.symm y)

A spherical vertex link gives a PL chart on the entire open star, with target the interior of a full-dimensional simplex. The vertex maps to the barycentre. The ambient formulas agree with the chart on its source and with its inverse on its target, so callers can prove PL compatibility without unfolding the chart construction.