Documentation

TauCeti.AlgebraicTopology.SimplicialComplex.Realization.Star.PL.Simplex

Piecewise-linear simplex models of vertex stars with spherical or ball links #

If the link of a vertex v is a combinatorial n-sphere, then the closed star of v is PL-homeomorphic to the standard (n + 1)-simplex, the realization of the full complex on Fin (n + 2), with v going to the barycentre. The identification is pseudo-radial projection from the barycentre: the link is identified with the boundary of the simplex by its standard PL model, and each segment from a link point to v goes to the segment from its image to the barycentre. In coordinates, the apex coordinate at v is n + 2 times the least barycentric coordinate of the image, so the open star of v goes onto the open simplex.

If instead the link of v is a combinatorial n-ball, then the closed star of v is PL-homeomorphic to the same simplex with v going to its last vertex: the link is identified with the opposite facet by its standard PL model, and each segment from a link point to v goes to the segment from its image to that vertex. The apex coordinate at v is the last barycentric coordinate of the image, so the open star of v goes onto the complement of the facet.

In both cases the homeomorphism and its inverse have piecewise-linear ambient coordinate formulas. These are the local models at interior and at boundary vertices for piecewise-linear charts on combinatorial manifolds.

The ambient complex and its vertex type may be infinite: the link has finitely many faces, which makes the closed star compact.

Main results #

References #

theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.exists_homeomorph_closedStarRealization_top {ι : Type u_1} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {v : ι} {n : ℕ} (h : (K.link {v}).IsCombinatorialSphere n) :
∃ (φ : ↑(K.closedStarRealization {v}) ≃ₜ ⊤.Realization), (⇑↑(φ (K.starApex v)) = fun (x : Fin (n + 2)) => (↑n + 2)⁻¹) ∧ (∀ (x : ↑(K.closedStarRealization {v})), (↑n + 2) * Finset.univ.inf' ⋯ ⇑↑(φ x) = ↑↑x v) ∧ ∃ (F : (ι → ℝ) → Fin (n + 2) → ℝ) (G : (Fin (n + 2) → ℝ) → ι → ℝ), TauCeti.IsPLOn F (Set.range fun (x : ↑(K.closedStarRealization {v})) => ⇑↑↑x) ∧ TauCeti.IsPLOn G (Set.range fun (y : ⊤.Realization) => ⇑↑y) ∧ (∀ (x : ↑(K.closedStarRealization {v})), F ⇑↑↑x = ⇑↑(φ x)) ∧ ∀ (x : ↑(K.closedStarRealization {v})), G ⇑↑(φ x) = ⇑↑↑x

Simplex model of a closed vertex star with a spherical link. If the link of v is a combinatorial n-sphere, the closed star of v is homeomorphic to the standard (n + 1)-simplex, the realization of the full complex on Fin (n + 2), with piecewise-linear ambient coordinate formulas in both directions. The vertex goes to the barycentre, and its coordinate at a point of the closed star is n + 2 times the least coordinate of the image, so the open star goes onto the open simplex.

theorem PreAbstractSimplicialComplex.IsCombinatorialBall.exists_homeomorph_closedStarRealization_top {ι : Type u_1} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {v : ι} {n : ℕ} (h : (K.link {v}).IsCombinatorialBall n) :
∃ (φ : ↑(K.closedStarRealization {v}) ≃ₜ ⊤.Realization), ⇑↑(φ (K.starApex v)) = Pi.single (Fin.last (n + 1)) 1 ∧ (∀ (x : ↑(K.closedStarRealization {v})), ↑(φ x) (Fin.last (n + 1)) = ↑↑x v) ∧ ∃ (F : (ι → ℝ) → Fin (n + 2) → ℝ) (G : (Fin (n + 2) → ℝ) → ι → ℝ), TauCeti.IsPLOn F (Set.range fun (x : ↑(K.closedStarRealization {v})) => ⇑↑↑x) ∧ TauCeti.IsPLOn G (Set.range fun (y : ⊤.Realization) => ⇑↑y) ∧ (∀ (x : ↑(K.closedStarRealization {v})), F ⇑↑↑x = ⇑↑(φ x)) ∧ ∀ (x : ↑(K.closedStarRealization {v})), G ⇑↑(φ x) = ⇑↑↑x

Simplex model of a closed vertex star with a ball link. If the link of v is a combinatorial n-ball, the closed star of v is homeomorphic to the standard (n + 1)-simplex, the realization of the full complex on Fin (n + 2), with piecewise-linear ambient coordinate formulas in both directions. The vertex goes to the last vertex of the simplex, the link onto the opposite facet, and the coordinate of a point of the closed star at v is the last coordinate of its image, so the open star goes onto the complement of that facet.