Vertex restrictions and compact factorization

The realization of a vertex restriction is the closed subspace of points supported on those vertices. Every continuous map with compact image factors continuously through a restriction to finitely many vertices. In particular, this applies to maps from compact spaces, reducing nullhomotopy constructions for spheres and cubes in infinite weak polyhedra to finite vertex sets.

All topologies are weak realization topologies; neither the complex nor the ambient vertex type needs to be locally finite or countable.

References

• A. Hatcher, Algebraic Topology, Appendix A, Proposition A.1.
• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2.

noncomputable def AbstractSimplicialComplex.restrictRealizationHomeomorph {ι : Type u_1} (K : AbstractSimplicialComplex ι) (s : Set ι) : (K.restrict s).Realization ≃ₜ { x : K.Realization // ↑(↑x).support ⊆ s }

Realizing a vertex restriction identifies it with the subspace of points supported on the chosen vertices.

@[simp]

theorem AbstractSimplicialComplex.restrictRealizationHomeomorph_apply {ι : Type u_1} (K : AbstractSimplicialComplex ι) (s : Set ι) (x : (K.restrict s).Realization) : ↑((K.restrictRealizationHomeomorph s) x) = (K.restrictInclusion s).realizationMap x

The restriction homeomorphism followed by the subtype inclusion is the simplicial realization of the vertex inclusion.

@[simp]

theorem AbstractSimplicialComplex.restrictRealizationHomeomorph_symm_val {ι : Type u_1} (K : AbstractSimplicialComplex ι) (s : Set ι) (x : { x : K.Realization // ↑(↑x).support ⊆ s }) : ↑((K.restrictRealizationHomeomorph s).symm x) = Finsupp.comapDomain Subtype.val ↑↑x ⋯

The inverse restriction homeomorphism pulls barycentric coordinates back along the vertex inclusion.

theorem AbstractSimplicialComplex.isClosedEmbedding_restrictInclusion_realizationMap {ι : Type u_1} (K : AbstractSimplicialComplex ι) (s : Set ι) : Topology.IsClosedEmbedding ⇑(K.restrictInclusion s).realizationMap

The realized vertex inclusion is a closed embedding, for arbitrary vertex subsets.

@[simp]

theorem AbstractSimplicialComplex.mem_range_restrictInclusion_realizationMap {ι : Type u_1} (K : AbstractSimplicialComplex ι) (s : Set ι) (x : K.Realization) : x ∈ Set.range ⇑(K.restrictInclusion s).realizationMap ↔ ↑(↑x).support ⊆ s

A point lies in the realized restriction exactly when its support uses only the chosen vertices.

theorem AbstractSimplicialComplex.isCompact_setOf_support_subset {ι : Type u_1} (K : AbstractSimplicialComplex ι) (s : Set ι) (hs : s.Finite) : IsCompact {x : K.Realization | ↑(↑x).support ⊆ s}

Points supported on a finite set of vertices form a compact subpolyhedron, even when the ambient complex has infinitely many faces.

theorem AbstractSimplicialComplex.exists_finite_restrict_factorization {ι : Type u_1} (K : AbstractSimplicialComplex ι) {X : Type u_2} [TopologicalSpace X] (f : C(X, K.Realization)) (hf : IsCompact (Set.range ⇑f)) : ∃ (V : Finset ι) (g : C(X, (K.restrict ↑V).Realization)), (K.restrictInclusion ↑V).realizationMap.comp g = f

Every continuous map with compact image factors continuously through a finite vertex restriction. The statement includes empty domains and imposes no hypothesis on the vertices.