Locally finite polyhedra

When every vertex has finite closed star, a weak geometric realization is locally compact and its topology agrees with the topology of its barycentric coordinates. The open stars are the coordinate-positive neighbourhoods; each lies in a compact closed star. This permits local models of combinatorial manifolds to be treated as coordinate subspaces without a global finiteness assumption on the triangulation.

The sphere-or-ball link condition implies finiteness of every vertex star. Consequently realizations of combinatorial manifolds satisfy both conclusions.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapters 2--3 (locally finite polyhedra and vertex stars).

theorem AbstractSimplicialComplex.locallyCompactSpace_realization_of_finite_vertex_stars {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) (hfin : ∀ (v : ι), (K.closedStar {v}).faces.Finite) : LocallyCompactSpace K.Realization

Finite vertex stars provide a compact neighbourhood around every realization point.

theorem AbstractSimplicialComplex.isEmbedding_realization_coe_of_finite_vertex_stars {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) (hfin : ∀ (v : ι), (K.closedStar {v}).faces.Finite) : Topology.IsEmbedding fun (x : K.Realization) => ⇑↑x

With finite vertex stars, the weak topology is exactly the topology induced by barycentric coordinates. No global finiteness assumption is needed.

theorem AbstractSimplicialComplex.locallyCompactSpace_realization_of_isCombinatorialManifold {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (hK : K.IsCombinatorialManifold n) : LocallyCompactSpace K.Realization

The realization of a combinatorial manifold is locally compact.

theorem AbstractSimplicialComplex.isEmbedding_realization_coe_of_isCombinatorialManifold {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (hK : K.IsCombinatorialManifold n) : Topology.IsEmbedding fun (x : K.Realization) => ⇑↑x

The weak realization of a combinatorial manifold embeds in its barycentric-coordinate space.