Geometric balls and spheres from combinatorial complexes

The weak polyhedron of a combinatorial n-ball or n-sphere is PL-homeomorphic to its standard simplicial model and homeomorphic to the Euclidean closed ball or unit sphere. The ball result identifies the closed vertex stars used to construct manifold charts, while the sphere result identifies the spherical links at interior vertices. The topological results concern the actual subpolyhedron of an arbitrary ambient realization, so unused ambient vertices contribute no extra points.

Intrinsic stellar equivalence supplies the PL homeomorphism to a simplex or simplex boundary, and injective relabeling replaces its arbitrary finite vertex labels by canonical Fin labels while preserving ambient PL coordinate formulas. The standard models then supply the Euclidean closed ball or sphere. No finiteness assumption on the ambient complex or its vertex type is required; finiteness follows from the combinatorial ball or sphere hypothesis.

References

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

PL standard models

theorem PreAbstractSimplicialComplex.IsCombinatorialBall.exists_plHomeomorphic_simplex {ι : Type u_1} {P : PreAbstractSimplicialComplex ι} {n : ℕ} [DecidableEq ι] (h : P.IsCombinatorialBall n) : ∃ (V : Finset ι), V.card = n + 1 ∧ P.PLHomeomorphic (simplex V)

A combinatorial ball is PL-homeomorphic to a simplex of the prescribed dimension.

theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.exists_plHomeomorphic_simplexBoundary {ι : Type u_1} {P : PreAbstractSimplicialComplex ι} {n : ℕ} [DecidableEq ι] (h : P.IsCombinatorialSphere n) : ∃ (V : Finset ι), V.card = n + 2 ∧ P.PLHomeomorphic (simplexBoundary V)

A combinatorial sphere is PL-homeomorphic to the boundary of a simplex of the prescribed dimension.

theorem PreAbstractSimplicialComplex.IsCombinatorialBall.plHomeomorphic_standardSimplex {ι : Type u_1} {P : PreAbstractSimplicialComplex ι} {n : ℕ} [DecidableEq ι] (h : P.IsCombinatorialBall n) : P.PLHomeomorphic (simplex Finset.univ)

A combinatorial ball has the PL homeomorphism type of the simplex on a canonical finite vertex type. This removes the arbitrary labels from exists_plHomeomorphic_simplex, which is useful when transporting the standard simplex charts.

theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.plHomeomorphic_standardSimplexBoundary {ι : Type u_1} {P : PreAbstractSimplicialComplex ι} {n : ℕ} [DecidableEq ι] (h : P.IsCombinatorialSphere n) : P.PLHomeomorphic (simplexBoundary Finset.univ)

A combinatorial sphere has the PL homeomorphism type of the boundary of the simplex on a canonical finite vertex type. This is the standard link model used by PL vertex charts.

theorem PreAbstractSimplicialComplex.IsCombinatorialBall.exists_homeomorph_standardSimplex {ι : Type u_1} {P : PreAbstractSimplicialComplex ι} {A : AbstractSimplicialComplex ι} {n : ℕ} [DecidableEq ι] (h : P.IsCombinatorialBall n) (hA : P ≤ A.toPreAbstractSimplicialComplex) : ∃ (e : { x : A.Realization // (↑x).support ∈ P } ≃ₜ ⊤.Realization) (f : (ι → ℝ) → Fin (n + 1) → ℝ) (g : (Fin (n + 1) → ℝ) → ι → ℝ), TauCeti.IsPLOn f (Set.range fun (x : { x : A.Realization // (↑x).support ∈ P }) => ⇑↑↑x) ∧ TauCeti.IsPLOn g (Set.range fun (y : ⊤.Realization) => ⇑↑y) ∧ (∀ (x : { x : A.Realization // (↑x).support ∈ P }), f ⇑↑↑x = ⇑↑(e x)) ∧ ∀ (y : ⊤.Realization), g ⇑↑y = ⇑↑↑(e.symm y)

A combinatorial ball has a PL homeomorphism to the realization of the standard simplex, with ambient PL coordinate formulas in both directions.

theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.exists_homeomorph_standardSimplexBoundary {ι : Type u_1} {P : PreAbstractSimplicialComplex ι} {A : AbstractSimplicialComplex ι} {n : ℕ} [DecidableEq ι] (h : P.IsCombinatorialSphere n) (hA : P ≤ A.toPreAbstractSimplicialComplex) : ∃ (e : { x : A.Realization // (↑x).support ∈ P } ≃ₜ (AbstractSimplicialComplex.standardSuccSimplexBoundary n).Realization) (f : (ι → ℝ) → Fin (n + 2) → ℝ) (g : (Fin (n + 2) → ℝ) → ι → ℝ), TauCeti.IsPLOn f (Set.range fun (x : { x : A.Realization // (↑x).support ∈ P }) => ⇑↑↑x) ∧ TauCeti.IsPLOn g (Set.range fun (y : (AbstractSimplicialComplex.standardSuccSimplexBoundary n).Realization) => ⇑↑y) ∧ (∀ (x : { x : A.Realization // (↑x).support ∈ P }), f ⇑↑↑x = ⇑↑(e x)) ∧ ∀ (y : (AbstractSimplicialComplex.standardSuccSimplexBoundary n).Realization), g ⇑↑y = ⇑↑↑(e.symm y)

A combinatorial sphere has a PL homeomorphism to the realization of the standard simplex boundary, with ambient PL coordinate formulas in both directions.

Topological standard models

theorem PreAbstractSimplicialComplex.IsCombinatorialBall.nonempty_homeomorph_closedBall {ι : Type u_1} {P : PreAbstractSimplicialComplex ι} {A : AbstractSimplicialComplex ι} {n : ℕ} [DecidableEq ι] (h : P.IsCombinatorialBall n) (hA : P ≤ A.toPreAbstractSimplicialComplex) : Nonempty ({ x : A.Realization // (↑x).support ∈ P } ≃ₜ ↑(Metric.closedBall 0 1))

A combinatorial n-ball has a weak polyhedron homeomorphic to the Euclidean closed n-ball.

The ambient complex may contain unused vertices. They are removed by the weak-polyhedron subtype.

theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.nonempty_homeomorph_sphere {ι : Type u_1} {P : PreAbstractSimplicialComplex ι} {A : AbstractSimplicialComplex ι} {n : ℕ} [DecidableEq ι] (h : P.IsCombinatorialSphere n) (hA : P ≤ A.toPreAbstractSimplicialComplex) : Nonempty ({ x : A.Realization // (↑x).support ∈ P } ≃ₜ ↑(Metric.sphere 0 1))

A combinatorial n-sphere has a weak polyhedron homeomorphic to the unit n-sphere, inside any ambient realization containing it. This includes the two-point zero-sphere.

Vertex-star ball models

theorem PreAbstractSimplicialComplex.IsCombinatorialManifold.nonempty_homeomorph_closedStar_closedBall {ι : Type u_1} {n : ℕ} {K : AbstractSimplicialComplex ι} [DecidableEq ι] (h : K.IsCombinatorialManifold n) {v : ι} (hv : {v} ∈ K) : Nonempty (↑(K.closedStarRealization {v}) ≃ₜ ↑(Metric.closedBall 0 1))

The weak polyhedron of a vertex's closed star in a combinatorial n-manifold is homeomorphic to the Euclidean closed n-ball, providing the local closed-ball model for its vertex charts.

The statement uses the weak realization topology and allows an arbitrary ambient vertex type; unused ambient vertices contribute no points.