PL half-space charts on open vertex stars

A vertex whose link is a combinatorial n-ball or n-sphere has a chart on its entire open star, modelled on the half-space in (Fin n → ℝ) × ℝ. Both directions have ambient PL coordinate formulas, so charts of either kind can be checked for PL compatibility against each other.

For a ball link, the closed-star simplex identification carries the vertex to the last simplex vertex. Restricting the standard simplex chart at that vertex therefore gives a chart on the open star, including all its boundary points; the vertex maps to zero on the boundary of the half-space.

For a sphere link, the Euclidean chart onto the interior of the coordinate simplex is read in the half-space by taking the last simplex coordinate as the height. Its target lies in the open half-space, so these are interior charts.

Together these are the vertex charts needed to pass from combinatorial manifolds to chart-based PL manifolds with boundary.

References

• C. P. Rourke and B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapters 2–3 (polyhedral charts and combinatorial manifolds).

theorem PreAbstractSimplicialComplex.IsCombinatorialBall.exists_openPartialHomeomorph_openStar_isPL {ι : Type u_1} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {v : ι} {n : ℕ} (h : (K.link {v}).IsCombinatorialBall n) : ∃ (c : OpenPartialHomeomorph K.Realization ↑{q : (Fin n → ℝ) × ℝ | 0 ≤ q.2}), c.source = K.openStarRealization v ∧ c.target = (AbstractSimplicialComplex.simplexHalfSpacePLChart n none).target ∧ ↑(↑c (K.vertex v)) = 0 ∧ ∃ (f : (ι → ℝ) → (Fin n → ℝ) × ℝ) (g : (Fin n → ℝ) × ℝ → ι → ℝ), TauCeti.IsPLOn f (Set.range fun (x : ↑(K.closedStarRealization {v})) => ⇑↑↑x) ∧ TauCeti.IsPLOn g (↑(TauCeti.modelWithCornersHalfSpace (Fin n → ℝ)).symm ⁻¹' c.target ∩ Set.range ↑(TauCeti.modelWithCornersHalfSpace (Fin n → ℝ))) ∧ (∀ x ∈ c.source, f ⇑↑x = ↑(↑c x)) ∧ ∀ y ∈ c.target, g ↑y = ⇑↑(↑c.symm y)

A combinatorial-ball vertex link supplies a PL half-space chart on the entire open vertex star. Its forward formula is PL on the closed star, and its inverse formula is PL on the model coordinates of the chart target. The vertex lies at zero in the half-space.

theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.exists_openPartialHomeomorph_openStar_halfSpace_isPL {ι : Type u_1} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {v : ι} {n : ℕ} (h : (K.link {v}).IsCombinatorialSphere n) : ∃ (c : OpenPartialHomeomorph K.Realization ↑{q : (Fin n → ℝ) × ℝ | 0 ≤ q.2}), c.source = K.openStarRealization v ∧ (∀ y ∈ c.target, 0 < (↑y).2) ∧ ∃ (f : (ι → ℝ) → (Fin n → ℝ) × ℝ) (g : (Fin n → ℝ) × ℝ → ι → ℝ), TauCeti.IsPLOn f (Set.range fun (x : ↑(K.closedStarRealization {v})) => ⇑↑↑x) ∧ TauCeti.IsPLOn g (↑(TauCeti.modelWithCornersHalfSpace (Fin n → ℝ)).symm ⁻¹' c.target ∩ Set.range ↑(TauCeti.modelWithCornersHalfSpace (Fin n → ℝ))) ∧ (∀ x ∈ c.source, f ⇑↑x = ↑(↑c x)) ∧ ∀ y ∈ c.target, g ↑y = ⇑↑(↑c.symm y)

A combinatorial-sphere vertex link supplies a PL half-space chart on the entire open vertex star whose target lies in the open half-space. The last coordinate of the Euclidean sphere-link chart becomes the height. The forward formula is PL on the closed star, and the inverse formula is PL on the model coordinates of the chart target, in the same form as IsCombinatorialBall.exists_openPartialHomeomorph_openStar_isPL.