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.

TODO: The Krull dimension of Spec(R) equals the Krull dimension of R, for R a commutative ring.

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

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

Equations

• topologicalKrullDim T = krullDim (TopologicalSpace.IrreducibleCloseds T)