The topology of finite polyhedra

For a complex with finitely many faces, the weak topology of its realization agrees with its barycentric-coordinate topology. In particular, the realization is compact and its coordinate map into ι → ℝ is a closed embedding. This permits finite polyhedra, including finite local models of triangulated manifolds, to be treated as ordinary coordinate subspaces.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapter 2 (polyhedra and their topology).

theorem AbstractSimplicialComplex.isCompact_setOf_support_mem {ι : Type u_1} (K : AbstractSimplicialComplex ι) {L : PreAbstractSimplicialComplex ι} (hL : L ≤ K.toPreAbstractSimplicialComplex) (hfin : L.faces.Finite) : IsCompact {x : K.Realization | (↑x).support ∈ L}

A finite subcomplex occupies a compact subset of the weak realization.

theorem AbstractSimplicialComplex.compactSpace_realization_of_finite_faces {ι : Type u_1} (K : AbstractSimplicialComplex ι) (hfin : K.faces.Finite) : CompactSpace K.Realization

The weak realization of a complex with finitely many faces is compact.

instance AbstractSimplicialComplex.instCompactSpaceRealization {ι : Type u_1} [Finite ι] (K : AbstractSimplicialComplex ι) : CompactSpace K.Realization

The weak realization of a complex on a finite vertex type is compact.

theorem AbstractSimplicialComplex.isClosedEmbedding_realization_coe_restrict {ι : Type u_1} (K : AbstractSimplicialComplex ι) {s : Set K.Realization} (hs : IsCompact s) : Topology.IsClosedEmbedding fun (x : ↑s) => ⇑↑↑x

Barycentric coordinates restrict to a closed embedding on every compact subset of the weak realization. This applies in particular to compact local chart domains.

theorem AbstractSimplicialComplex.isClosedEmbedding_realization_coe {ι : Type u_1} (K : AbstractSimplicialComplex ι) (hfin : K.faces.Finite) : Topology.IsClosedEmbedding fun (x : K.Realization) => ⇑↑x

For a complex with finitely many faces the barycentric-coordinate map is a closed embedding. Thus the weak topology is exactly the topology inherited from coordinate space.