The dimension of an abstract simplicial complex

The dimension of a simplicial complex is the supremum of the dimensions of its faces, where a face with k + 1 vertices has dimension k. This file defines that dimension for PreAbstractSimplicialComplex (Mathlib's downward-closed collection of nonempty finite faces, no singleton requirement) and for AbstractSimplicialComplex.

Following the convention Mathlib uses for Order.krullDim, the dimension takes values in WithBot ℕ∞: the empty complex ⊥ has dimension ⊥ (the "-1" of the void complex), a complex whose faces have unbounded cardinality has dimension ⊤, and a finite-dimensional nonempty complex has an honest natural-number dimension. This is the primitive the layer-11 combinatorial-manifold recursion is indexed against: a combinatorial n-sphere or n-ball is an n-dimensional complex, and the boundary of the standard (n + 1)-simplex — computed here to have dimension n — is the base model of that recursion.

The definitions follow Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2. This supplements the basic API (faces, the star and link of a simplex) that the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md, layer 11) asks for on top of Mathlib's AbstractSimplicialComplex.

Main definitions

• PreAbstractSimplicialComplex.dimension: the dimension of a precomplex.
• AbstractSimplicialComplex.dimension: the dimension of an abstract complex.

Main results

• PreAbstractSimplicialComplex.le_dimension: every face's dimension bounds the complex's.
• PreAbstractSimplicialComplex.dimension_le_iff: the dimension is bounded exactly when every face's dimension is.
• PreAbstractSimplicialComplex.dimension_mono: dimension is monotone in the complex.
• PreAbstractSimplicialComplex.dimension_map_of_injective: injective relabeling preserves dimension.
• PreAbstractSimplicialComplex.dimension_eq_bot_iff: only the void complex has dimension ⊥.
• PreAbstractSimplicialComplex.dimension_eq_top_iff / dimension_lt_top_iff: infinite dimension means that face cardinalities are unbounded, while finite dimension means that they have a uniform natural-number bound.
• PreAbstractSimplicialComplex.dimension_le_card_sub_one: a finite set containing every face gives an explicit dimension bound.
• PreAbstractSimplicialComplex.exists_face_card_eq_of_dimension_eq: a finite natural-number dimension is attained by a face.
• PreAbstractSimplicialComplex.dimension_top_eq_top_of_infinite: the full complex on an infinite vertex type has infinite dimension.
• PreAbstractSimplicialComplex.dimension_simplex / PreAbstractSimplicialComplex.dimension_simplexBoundary: the dimensions of the standard simplex on V (namely V.card - 1) and of its boundary (namely V.card - 2).

noncomputable def PreAbstractSimplicialComplex.dimension {ι : Type u_1} (K : PreAbstractSimplicialComplex ι) : WithBot ℕ∞

The dimension of a pre-abstract simplicial complex: the supremum, over its faces σ, of the face dimension σ.card - 1. It takes values in WithBot ℕ∞, so the void complex has dimension ⊥ and an unbounded complex has dimension ⊤.

Equations

• K.dimension = ⨆ σ ∈ K, ↑(σ.card - 1)

theorem PreAbstractSimplicialComplex.le_dimension {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} (hσ : σ ∈ K) : ↑(σ.card - 1) ≤ K.dimension

The dimension of any face bounds the dimension of the complex.

theorem PreAbstractSimplicialComplex.dimension_le_iff {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {n : WithBot ℕ∞} : K.dimension ≤ n ↔ ∀ σ ∈ K, ↑(σ.card - 1) ≤ n

The dimension of a complex is bounded by n exactly when every face's dimension is.

theorem PreAbstractSimplicialComplex.dimension_le_zero_iff {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} : K.dimension ≤ 0 ↔ ∀ σ ∈ K, ∃ (v : ι), σ = {v}

A precomplex has dimension at most zero exactly when every face is a singleton. The void complex is allowed.

theorem PreAbstractSimplicialComplex.dimension_mono {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : K ≤ L) : K.dimension ≤ L.dimension

Dimension is monotone in the complex.

theorem PreAbstractSimplicialComplex.dimension_map_of_injective {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {κ : Type u_2} [DecidableEq κ] (f : ι → κ) (hf : Function.Injective f) : (K.map f).dimension = K.dimension

An injective relabeling preserves the dimension of a precomplex.

@[simp]

theorem PreAbstractSimplicialComplex.dimension_bot {ι : Type u_1} : ⊥.dimension = ⊥

The void complex has dimension ⊥.

@[simp]

theorem PreAbstractSimplicialComplex.dimension_eq_bot_iff {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} : K.dimension = ⊥ ↔ K = ⊥

Only the void complex has dimension ⊥: any face contributes a nonnegative dimension.

@[simp]

theorem PreAbstractSimplicialComplex.dimension_eq_top_iff {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} : K.dimension = ⊤ ↔ ∀ (n : ℕ), ∃ σ ∈ K, n ≤ σ.card

A complex has infinite dimension exactly when its face cardinalities are unbounded.

@[simp]

theorem PreAbstractSimplicialComplex.dimension_lt_top_iff {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} : K.dimension < ⊤ ↔ ∃ (n : ℕ), ∀ σ ∈ K, σ.card ≤ n

A complex has dimension below ⊤ exactly when its face cardinalities have a uniform natural number bound.

theorem PreAbstractSimplicialComplex.exists_face_card_eq_of_dimension_eq {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.dimension = ↑n) : ∃ σ ∈ K, σ.card = n + 1

If a precomplex has finite natural-number dimension n, some face has exactly n + 1 vertices.

theorem PreAbstractSimplicialComplex.dimension_le_card_sub_one {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {V : Finset ι} (hV : ∀ σ ∈ K, σ ⊆ V) : K.dimension ≤ ↑(V.card - 1)

If every face of a complex is contained in a finite set V, then its dimension is at most V.card - 1.

theorem PreAbstractSimplicialComplex.dimension_lt_top_of_finite_vertices {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {V : Finset ι} (hV : ∀ σ ∈ K, σ ⊆ V) : K.dimension < ⊤

A complex carried by a finite set of vertices has dimension below ⊤.

theorem PreAbstractSimplicialComplex.dimension_lt_top_of_finite {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} [Finite ι] : K.dimension < ⊤

A complex on a finite vertex type has dimension below ⊤.

@[simp]

theorem PreAbstractSimplicialComplex.dimension_top_eq_top_of_infinite {ι : Type u_1} [Infinite ι] : ⊤.dimension = ⊤

The full complex on an infinite vertex type has infinite dimension.

@[simp]

theorem PreAbstractSimplicialComplex.dimension_simplex {ι : Type u_1} {V : Finset ι} (hV : V.Nonempty) : (simplex V).dimension = ↑(V.card - 1)

The dimension of the standard simplex on a nonempty vertex set V is V.card - 1.

@[simp]

theorem PreAbstractSimplicialComplex.dimension_simplexBoundary {ι : Type u_1} {V : Finset ι} (hV : 1 < V.card) : (simplexBoundary V).dimension = ↑(V.card - 2)

The dimension of the boundary of the standard simplex on a vertex set V with at least two vertices is V.card - 2.

noncomputable def AbstractSimplicialComplex.dimension {ι : Type u_1} (K : AbstractSimplicialComplex ι) : WithBot ℕ∞

The dimension of an abstract simplicial complex, defined through its underlying precomplex.

Equations

• K.dimension = K.dimension

@[simp]

theorem AbstractSimplicialComplex.dimension_toPreAbstractSimplicialComplex {ι : Type u_1} (K : AbstractSimplicialComplex ι) : K.dimension = K.dimension

The dimension of an abstract complex agrees with the dimension of its underlying precomplex.

theorem AbstractSimplicialComplex.le_dimension {ι : Type u_1} {K : AbstractSimplicialComplex ι} {σ : Finset ι} (hσ : σ ∈ K) : ↑(σ.card - 1) ≤ K.dimension

The dimension of any face bounds the dimension of the complex.

theorem AbstractSimplicialComplex.dimension_le_iff {ι : Type u_1} {K : AbstractSimplicialComplex ι} {n : WithBot ℕ∞} : K.dimension ≤ n ↔ ∀ σ ∈ K, ↑(σ.card - 1) ≤ n

The dimension of an abstract complex is bounded by n exactly when every face's dimension is.

theorem AbstractSimplicialComplex.dimension_mono {ι : Type u_1} {K L : AbstractSimplicialComplex ι} (h : K ≤ L) : K.dimension ≤ L.dimension

Dimension is monotone in the abstract complex.

@[simp]

theorem AbstractSimplicialComplex.dimension_eq_top_iff {ι : Type u_1} {K : AbstractSimplicialComplex ι} : K.dimension = ⊤ ↔ ∀ (n : ℕ), ∃ σ ∈ K, n ≤ σ.card

An abstract simplicial complex has infinite dimension exactly when its face cardinalities are unbounded.

@[simp]

theorem AbstractSimplicialComplex.dimension_lt_top_iff {ι : Type u_1} {K : AbstractSimplicialComplex ι} : K.dimension < ⊤ ↔ ∃ (n : ℕ), ∀ σ ∈ K, σ.card ≤ n

An abstract simplicial complex has dimension below ⊤ exactly when its face cardinalities have a uniform natural-number bound.

theorem AbstractSimplicialComplex.dimension_le_card_sub_one {ι : Type u_1} {K : AbstractSimplicialComplex ι} {V : Finset ι} (hV : ∀ σ ∈ K, σ ⊆ V) : K.dimension ≤ ↑(V.card - 1)

If every face of an abstract simplicial complex is contained in a finite set V, then its dimension is at most V.card - 1.

theorem AbstractSimplicialComplex.dimension_lt_top_of_finite_vertices {ι : Type u_1} {K : AbstractSimplicialComplex ι} {V : Finset ι} (hV : ∀ σ ∈ K, σ ⊆ V) : K.dimension < ⊤

An abstract simplicial complex carried by a finite set of vertices has dimension below ⊤.

theorem AbstractSimplicialComplex.dimension_lt_top_of_finite {ι : Type u_1} {K : AbstractSimplicialComplex ι} [Finite ι] : K.dimension < ⊤

An abstract simplicial complex on a finite vertex type has dimension below ⊤.

@[simp]

theorem AbstractSimplicialComplex.dimension_top_eq_top_of_infinite {ι : Type u_1} [Infinite ι] : ⊤.dimension = ⊤

The full abstract simplicial complex on an infinite vertex type has infinite dimension.