Subcomplexes in the weak realization topology

An inclusion of abstract simplicial complexes realizes to a closed embedding, without a finiteness or local-finiteness hypothesis. Thus a subcomplex has exactly the subspace topology inside the larger polyhedron. This permits closed subcomplexes to be used as local models and as the fixed parts of geometric deformations.

Closedness in the weak topology is tested on each closed simplex. On any one simplex, a subcomplex meets it in finitely many faces. This finite-face argument proves that inclusion sends every closed subset to a closed subset, even when the whole complex is infinite.

For a precomplex, its polyhedron is the subset of ambient realization points whose supports are its faces. The closed-set and continuity criteria apply to this actual subset, so links and deletions introduce no extra vertices. Continuity into an arbitrary topological space is determined by restriction to the subcomplex's closed simplices.

References

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

@[simp]

theorem AbstractSimplicialComplex.mem_range_realizationMap {ι : Type u_1} {K L : AbstractSimplicialComplex ι} (h : K ≤ L) (x : L.Realization) : x ∈ Set.range (realizationMap h) ↔ (↑x).support ∈ K

A point of the larger realization lies in the subcomplex precisely when its carrier is a face of that subcomplex.

theorem AbstractSimplicialComplex.isClosed_of_faceInclusion {ι : Type u_1} {L : AbstractSimplicialComplex ι} {P : PreAbstractSimplicialComplex ι} (hP : P ≤ L.toPreAbstractSimplicialComplex) {s : Set L.Realization} (hsupp : ∀ x ∈ s, (↑x).support ∈ P) (hs : ∀ (σ : Finset ι) (hσ : σ ∈ P), IsClosed (L.faceInclusion ⟨σ, ⋯⟩ ⁻¹' s)) : IsClosed s

If every point of s is carried by a precomplex P, closedness of s can be tested only on the faces of P. Unlike an abstract complex, P need not contain every ambient vertex; in particular, this applies to links, closed stars, and deletions.

theorem AbstractSimplicialComplex.support_faceInclusion_mem {ι : Type u_1} {L : AbstractSimplicialComplex ι} {P : PreAbstractSimplicialComplex ι} (hP : P ≤ L.toPreAbstractSimplicialComplex) {σ : Finset ι} (hσ : σ ∈ P) (x : StandardSimplex σ) : (↑(L.faceInclusion ⟨σ, ⋯⟩ x)).support ∈ P

The support of every point of a face of a precomplex is itself a face of that precomplex, even when the precomplex omits ambient vertices.

theorem AbstractSimplicialComplex.isClosed_setOf_support_mem {ι : Type u_1} {L : AbstractSimplicialComplex ι} {P : PreAbstractSimplicialComplex ι} (hP : P ≤ L.toPreAbstractSimplicialComplex) : IsClosed {x : L.Realization | (↑x).support ∈ P}

The polyhedron of any precomplex inside a weak realization is closed, including when the precomplex omits ambient vertices or has no faces.

theorem AbstractSimplicialComplex.continuous_subtype_iff_faceInclusion {ι : Type u_1} {L : AbstractSimplicialComplex ι} {X : Type u_2} [TopologicalSpace X] {P : PreAbstractSimplicialComplex ι} (hP : P ≤ L.toPreAbstractSimplicialComplex) {g : { x : L.Realization // (↑x).support ∈ P } → X} : Continuous g ↔ ∀ (σ : Finset ι) (hσ : σ ∈ P), Continuous (g ∘ fun (x : StandardSimplex σ) => ⟨L.faceInclusion ⟨σ, ⋯⟩ x, ⋯⟩)

A map defined on a precomplex polyhedron is continuous exactly when its composition with each canonical face map into that polyhedron is continuous. The domain carries the subspace topology of the ambient weak realization, without any finiteness assumption.

theorem AbstractSimplicialComplex.continuousOn_iff_faceInclusion {ι : Type u_1} {L : AbstractSimplicialComplex ι} {X : Type u_2} [TopologicalSpace X] {P : PreAbstractSimplicialComplex ι} (hP : P ≤ L.toPreAbstractSimplicialComplex) {f : L.Realization → X} : ContinuousOn f {x : L.Realization | (↑x).support ∈ P} ↔ ∀ (σ : Finset ι) (hσ : σ ∈ P), Continuous (f ∘ L.faceInclusion ⟨σ, ⋯⟩)

Continuity on a subcomplex can be checked on its closed simplices, with the subspace topology inherited from the ambient weak realization. The subcomplex may omit vertices.

theorem AbstractSimplicialComplex.isClosedEmbedding_realizationMap {ι : Type u_1} {K L : AbstractSimplicialComplex ι} (h : K ≤ L) : Topology.IsClosedEmbedding (realizationMap h)

Realizing a subcomplex inclusion gives a closed embedding for the weak topologies. No finiteness assumption on the complexes or their ambient vertex type is needed.