Compact subsets of weak polyhedra

A compact subset of a weak simplicial realization meets only finitely many open simplices, and consequently uses only finitely many vertices. This permits maps from compact spaces, including spheres and cubes, to be studied inside finite polyhedra even when the ambient complex is neither finite nor locally finite.

The compact-support finiteness results provide a finite vertex set containing the support of every point in a compact subset. They apply to arbitrary vertex types and require no local finiteness assumption on the complex. In particular, the whole realization is compact exactly when its vertex type is finite (compactSpace_realization_iff_finite): abstract simplicial complexes contain every singleton face, so no unused vertices are counted.

References

• A. Hatcher, Algebraic Topology, Appendix A, Proposition A.1 (compact subsets of weak complexes are contained in finite subcomplexes).

theorem AbstractSimplicialComplex.isClosed_of_injOn_support {ι : Type u_1} {K : AbstractSimplicialComplex ι} {s : Set K.Realization} (hs : Set.InjOn (fun (x : K.Realization) => (↑x).support) s) : IsClosed s

A set with at most one point in each open simplex is closed in the weak realization.

theorem AbstractSimplicialComplex.finite_image_support_of_isCompact {ι : Type u_1} {K : AbstractSimplicialComplex ι} {s : Set K.Realization} (hs : IsCompact s) : ((fun (x : K.Realization) => (↑x).support) '' s).Finite

Only finitely many barycentric supports occur in a compact subset of a weak realization. Equivalently, it meets only finitely many open simplices.

theorem AbstractSimplicialComplex.exists_finset_support_subset_of_isCompact {ι : Type u_1} {K : AbstractSimplicialComplex ι} {s : Set K.Realization} (hs : IsCompact s) : ∃ (V : Finset ι), ∀ x ∈ s, (↑x).support ⊆ V

Every compact subset of a weak realization uses only finitely many vertices.

theorem AbstractSimplicialComplex.compactSpace_realization_iff_finite {ι : Type u_1} (K : AbstractSimplicialComplex ι) : CompactSpace K.Realization ↔ Finite ι

A weak simplicial realization is compact exactly when its vertex type is finite. No local finiteness or dimension bound is required.