The Krull dimension of a topological space

The Krull dimension of a topological space is the order-theoretic Krull dimension applied to the collection of all its subsets that are closed and irreducible. Unfolding this definition, it is the length of longest series of closed irreducible subsets ordered by inclusion.

Main results

• topologicalKrullDim_subspace_le: For any subspace Y ⊆ X, we have dim(Y) ≤ dim(X)

Implementation notes

The proofs use order-preserving maps between posets of irreducible closed sets to establish dimension inequalities.

noncomputable def topologicalKrullDim (T : Type u_1) [TopologicalSpace T] : WithBot ℕ∞

The Krull dimension of a topological space is the supremum of lengths of chains of closed irreducible sets.

Equations

• topologicalKrullDim T = Order.krullDim (TopologicalSpace.IrreducibleCloseds T)

Main dimension theorems

theorem IsInducing.topologicalKrullDim_le {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → X} (hf : Topology.IsInducing f) : topologicalKrullDim Y ≤ topologicalKrullDim X

If f : Y → X is inducing, then dim(Y) ≤ dim(X).

@[deprecated IsInducing.topologicalKrullDim_le (since := "2025-10-19")]

theorem IsClosedEmbedding.topologicalKrullDim_le {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → X} (hf : Topology.IsInducing f) : topologicalKrullDim Y ≤ topologicalKrullDim X

Alias of IsInducing.topologicalKrullDim_le.

---

If f : Y → X is inducing, then dim(Y) ≤ dim(X).

theorem IsHomeomorph.topologicalKrullDim_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsHomeomorph f) : topologicalKrullDim X = topologicalKrullDim Y

The topological Krull dimension is invariant under homeomorphisms

theorem topologicalKrullDim_subspace_le (X : Type u_3) [TopologicalSpace X] (Y : Set X) : topologicalKrullDim ↑Y ≤ topologicalKrullDim X

The topological Krull dimension of any subspace is at most the dimension of the ambient space.