Piecewise-linear joins of vertex stars with a centre

Let F be an ambient coordinate formula embedding the geometric link of a vertex v onto a set T of a coordinate space κ → ℝ, and let b be a point there. Sending each point (1 - t) • y + t • v of the closed star of v, with y in the link, to (1 - t) • F y + t • b identifies the closed star with the convex join of T and b, provided these segments do not meet away from b. That proviso is recorded by a height function h recovering the parameter t along each segment.

When F, its inverse on T, and h are piecewise linear, the resulting homeomorphism and its inverse have piecewise-linear ambient coordinate formulas. This is pseudo-radial projection: for a link identified with the boundary of a simplex and b the barycentre, it identifies the closed star of a vertex with the whole simplex, and for a link identified with a facet of a simplex and b the opposite vertex, it identifies the closed star with that simplex. Such simplex models are the local models for piecewise-linear charts on the open vertex stars of a combinatorial manifold.

Only the closed star needs to be compact; the ambient complex and both vertex types may be infinite.

Main results

• AbstractSimplicialComplex.exists_homeomorph_closedStarRealization_convexJoin: the identification of a closed vertex star with the convex join of a link model and a centre, with piecewise-linear coordinate formulas in both directions.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapter 1, “Joins and Cones”, and Chapter 2, “Pseudo-Radial Projection”, pp. 20–21.

theorem AbstractSimplicialComplex.exists_homeomorph_closedStarRealization_convexJoin {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {v : ι} {F : (ι → ℝ) → κ → ℝ} {G : (κ → ℝ) → ι → ℝ} {b : κ → ℝ} {h : (κ → ℝ) → ℝ} (hK : IsCompact (K.closedStarRealization {v})) (hne : (K.geometricLink v).Nonempty) (hF : TauCeti.IsPLOn F (Set.range fun (y : ↑(K.geometricLink v)) => ⇑↑↑y)) (hG : TauCeti.IsPLOn G (Set.range fun (y : ↑(K.geometricLink v)) => F ⇑↑↑y)) (hGF : ∀ (y : ↑(K.geometricLink v)), G (F ⇑↑↑y) = ⇑↑↑y) (hh : TauCeti.IsPLOn h (convexJoin ℝ (Set.range fun (y : ↑(K.geometricLink v)) => F ⇑↑↑y) {b})) (hhF : ∀ (y : ↑(K.geometricLink v)), ∀ t ∈ Set.Icc 0 1, h ((1 - t) • F ⇑↑↑y + t • b) = t) : ∃ (φ : ↑(K.closedStarRealization {v}) ≃ₜ ↑(convexJoin ℝ (Set.range fun (y : ↑(K.geometricLink v)) => F ⇑↑↑y) {b})), ↑(φ (K.starApex v)) = b ∧ (∀ (x : ↑(K.closedStarRealization {v})), h ↑(φ x) = ↑↑x v) ∧ (∀ (x : ↑(K.closedStarRealization {v})) (hx : ↑↑x v < 1), ↑(φ x) = (1 - ↑↑x v) • F ⇑↑↑(K.starLinkProjection v ⟨↑x, ⋯⟩) + ↑↑x v • b) ∧ ∃ (F' : (ι → ℝ) → κ → ℝ) (G' : (κ → ℝ) → ι → ℝ), TauCeti.IsPLOn F' (Set.range fun (x : ↑(K.closedStarRealization {v})) => ⇑↑↑x) ∧ TauCeti.IsPLOn G' (convexJoin ℝ (Set.range fun (y : ↑(K.geometricLink v)) => F ⇑↑↑y) {b}) ∧ (∀ (x : ↑(K.closedStarRealization {v})), F' ⇑↑↑x = ↑(φ x)) ∧ ∀ (x : ↑(K.closedStarRealization {v})), G' ↑(φ x) = ⇑↑↑x

Pseudo-radial projection of a closed vertex star. Let F be a piecewise-linear coordinate formula for the geometric link of v, with a piecewise-linear inverse G on its image T, and let b be a centre with a piecewise-linear height function h that reads off t along every segment from T to b. Then the closed star of v is homeomorphic to the convex join of T and b: the apex goes to b, the apex coordinate is the height, every other point x goes to (1 - t) • F y + t • b, where t is its apex coordinate and y its radial projection to the link, and the homeomorphism and its inverse have piecewise-linear ambient coordinate formulas.

The height condition says exactly that these segments meet only at b.