The skeletal filtration of a weak realization

The realization of the n-skeleton is precisely the closed subspace of points with at most n + 1 nonzero barycentric coordinates. These subspaces exhaust the realization, and continuity out of the realization is detected on them. The skeleta carry their own weak realization topology, which agrees with the subspace topology even for infinite complexes.

Simplicial maps preserve this filtration. If a map is injective on each face, it also reflects skeletal membership: the dimension of the face carrying a point is preserved. These statements give the skeletal part of cellularity and of compatibility with simplex characteristic maps.

References

• A. Hatcher, Algebraic Topology, Chapter 0 (skeleta and cellular maps).
• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2 (the weak topology on a polyhedron).

theorem AbstractSimplicialComplex.range_realizationMap_skeleton {ι : Type u_1} (K : AbstractSimplicialComplex ι) (n : ℕ) : Set.range (realizationMap ⋯) = {x : K.Realization | (↑x).support.card ≤ n + 1}

The realized skeleton consists exactly of the points carried by a face of dimension at most n.

theorem AbstractSimplicialComplex.isClosed_setOf_card_support_le {ι : Type u_1} (K : AbstractSimplicialComplex ι) (n : ℕ) : IsClosed {x : K.Realization | (↑x).support.card ≤ n + 1}

The points with at most n + 1 nonzero coordinates form a closed subspace.

theorem AbstractSimplicialComplex.iUnion_range_realizationMap_skeleton {ι : Type u_1} (K : AbstractSimplicialComplex ι) : ⋃ (n : ℕ), Set.range (realizationMap ⋯) = Set.univ

The skeletal filtration exhausts the realization, even in unbounded dimension.

theorem AbstractSimplicialComplex.continuous_iff_realizationMap_skeleton {ι : Type u_1} (K : AbstractSimplicialComplex ι) {X : Type u_2} [TopologicalSpace X] {f : K.Realization → X} : Continuous f ↔ ∀ (n : ℕ), Continuous (f ∘ realizationMap ⋯)

Continuity out of a weak realization can be tested on all its skeleta.

theorem PreAbstractSimplicialComplex.SimplicialMap.realizationMap_skeleton {ι : Type u_1} {κ : Type u_2} [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (n : ℕ) : AbstractSimplicialComplex.realizationMap ⋯ ∘ ⇑(f.skeleton n).realizationMap = ⇑f.realizationMap ∘ AbstractSimplicialComplex.realizationMap ⋯

Realizing the restriction to a skeleton commutes with the skeletal inclusions.

theorem PreAbstractSimplicialComplex.SimplicialMap.card_support_realizationMap_le {ι : Type u_1} {κ : Type u_2} [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (x : K.Realization) : (↑(f.realizationMap x)).support.card ≤ (↑x).support.card

A simplicial realization cannot increase the number of nonzero barycentric coordinates.

theorem PreAbstractSimplicialComplex.SimplicialMap.mapsTo_realizationMap_skeleton {ι : Type u_1} {κ : Type u_2} [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (n : ℕ) : Set.MapsTo (⇑f.realizationMap) (Set.range (AbstractSimplicialComplex.realizationMap ⋯)) (Set.range (AbstractSimplicialComplex.realizationMap ⋯))

A realized simplicial map sends each skeleton into the corresponding skeleton.

theorem PreAbstractSimplicialComplex.SimplicialMap.card_support_realizationMap_of_injOn {ι : Type u_1} {κ : Type u_2} [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (x : K.Realization) (hf : Set.InjOn ⇑f ↑(↑x).support) : (↑(f.realizationMap x)).support.card = (↑x).support.card

Injectivity on the support of a point preserves its number of nonzero barycentric coordinates.

theorem PreAbstractSimplicialComplex.SimplicialMap.preimage_realizationMap_skeleton_of_injOn {ι : Type u_1} {κ : Type u_2} [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (hf : ∀ σ ∈ K, Set.InjOn ⇑f ↑σ) (n : ℕ) : ⇑f.realizationMap ⁻¹' Set.range (AbstractSimplicialComplex.realizationMap ⋯) = Set.range (AbstractSimplicialComplex.realizationMap ⋯)

A simplicial map injective on each face reflects skeletal membership as well as preserving it.