Skeleta of abstract simplicial complexes

The n-skeleton retains the faces with at most n + 1 vertices. Skeleta form an increasing, exhaustive filtration, and a simplicial map restricts to a map between corresponding skeleta, even when it identifies vertices. This is the combinatorial filtration underlying the cellular structure of a geometric realization.

The construction is first given for precomplexes, so it also applies to subcomplexes with unused vertices and to the void complex. An abstract complex retains all its vertices in every skeleton.

References

• A. Hatcher, Algebraic Topology, Chapter 0 (simplicial complexes and their skeleta).

def PreAbstractSimplicialComplex.skeleton {ι : Type u_1} (K : PreAbstractSimplicialComplex ι) (n : ℕ) : PreAbstractSimplicialComplex ι

The n-skeleton consists of the faces with at most n + 1 vertices.

@[simp]

theorem PreAbstractSimplicialComplex.mem_skeleton {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {n : ℕ} : σ ∈ K.skeleton n ↔ σ ∈ K ∧ σ.card ≤ n + 1

theorem PreAbstractSimplicialComplex.skeleton_le {ι : Type u_1} (K : PreAbstractSimplicialComplex ι) (n : ℕ) : K.skeleton n ≤ K

Every skeleton is a subcomplex of the original complex.

theorem PreAbstractSimplicialComplex.skeleton_mono {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} {m n : ℕ} (hKL : K ≤ L) (hmn : m ≤ n) : K.skeleton m ≤ L.skeleton n

Skeleta are monotone in the complex and the dimension bound.

@[simp]

theorem PreAbstractSimplicialComplex.skeleton_skeleton {ι : Type u_1} (K : PreAbstractSimplicialComplex ι) (m n : ℕ) : (K.skeleton m).skeleton n = K.skeleton (min m n)

Taking successive skeleta keeps the smaller dimension bound.

theorem PreAbstractSimplicialComplex.skeleton_eq_self_iff {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {n : ℕ} : K.skeleton n = K ↔ ∀ σ ∈ K, σ.card ≤ n + 1

A complex equals its n-skeleton exactly when every face has at most n + 1 vertices.

theorem PreAbstractSimplicialComplex.iSup_skeleton {ι : Type u_1} (K : PreAbstractSimplicialComplex ι) : ⨆ (n : ℕ), K.skeleton n = K

Every face occurs in some skeleton, without a finite-dimensionality assumption.

def PreAbstractSimplicialComplex.SimplicialMap.skeleton {ι : Type u_1} {κ : Type u_2} {K : PreAbstractSimplicialComplex ι} [DecidableEq κ] {L : PreAbstractSimplicialComplex κ} (f : K.SimplicialMap L) (n : ℕ) : (K.skeleton n).SimplicialMap (L.skeleton n)

A simplicial map restricts to corresponding skeleta; vertex identifications may lower the dimension of a face.

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.skeleton_apply {ι : Type u_1} {κ : Type u_2} {K : PreAbstractSimplicialComplex ι} [DecidableEq κ] {L : PreAbstractSimplicialComplex κ} (f : K.SimplicialMap L) (n : ℕ) (v : ι) : (f.skeleton n) v = f v

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.skeleton_comp {ι : Type u_1} {κ : Type u_2} {K : PreAbstractSimplicialComplex ι} [DecidableEq κ] {L : PreAbstractSimplicialComplex κ} {μ : Type u_3} [DecidableEq μ] {P : PreAbstractSimplicialComplex μ} (g : L.SimplicialMap P) (f : K.SimplicialMap L) (n : ℕ) : (g.comp f).skeleton n = (g.skeleton n).comp (f.skeleton n)

Restriction to skeleta preserves composition.

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.skeleton_id {ι : Type u_1} [DecidableEq ι] (K : PreAbstractSimplicialComplex ι) (n : ℕ) : (id K).skeleton n = id (K.skeleton n)

Restriction of an identity map is the identity on the skeleton.

@[reducible, inline]

abbrev AbstractSimplicialComplex.skeleton {ι : Type u_1} (K : AbstractSimplicialComplex ι) (n : ℕ) : AbstractSimplicialComplex ι

The n-skeleton of an abstract complex, retaining all its vertices. This reducible lift allows simplicial maps between precomplex skeleta to be used on abstract skeleta as well.

@[simp]

theorem AbstractSimplicialComplex.skeleton_toPreAbstractSimplicialComplex {ι : Type u_1} (K : AbstractSimplicialComplex ι) (n : ℕ) : (K.skeleton n).toPreAbstractSimplicialComplex = K.skeleton n

@[simp]

theorem AbstractSimplicialComplex.mem_skeleton {ι : Type u_1} {K : AbstractSimplicialComplex ι} {σ : Finset ι} {n : ℕ} : σ ∈ K.skeleton n ↔ σ ∈ K ∧ σ.card ≤ n + 1

theorem AbstractSimplicialComplex.skeleton_le {ι : Type u_1} (K : AbstractSimplicialComplex ι) (n : ℕ) : K.skeleton n ≤ K

The inclusion used to realize a skeleton as a subspace of the original polyhedron.

theorem AbstractSimplicialComplex.skeleton_mono {ι : Type u_1} {K L : AbstractSimplicialComplex ι} {m n : ℕ} (hKL : K ≤ L) (hmn : m ≤ n) : K.skeleton m ≤ L.skeleton n

Skeleta are monotone in the complex and the dimension bound.

@[simp]

theorem AbstractSimplicialComplex.skeleton_skeleton {ι : Type u_1} (K : AbstractSimplicialComplex ι) (m n : ℕ) : (K.skeleton m).skeleton n = K.skeleton (min m n)

Taking successive skeleta keeps the smaller dimension bound.

theorem AbstractSimplicialComplex.skeleton_eq_self_iff {ι : Type u_1} {K : AbstractSimplicialComplex ι} {n : ℕ} : K.skeleton n = K ↔ ∀ σ ∈ K, σ.card ≤ n + 1

A complex equals its n-skeleton exactly when all face dimensions are at most n.

theorem AbstractSimplicialComplex.iSup_skeleton {ι : Type u_1} (K : AbstractSimplicialComplex ι) : ⨆ (n : ℕ), K.skeleton n = K

The increasing family of skeleta exhausts the complex.