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 Topology.IsInducing.topologicalKrullDim_le {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → X} (hf : IsInducing f) : topologicalKrullDim Y ≤ topologicalKrullDim X

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.

theorem topologicalKrullDim_zero_of_discreteTopology (X : Type u_3) [TopologicalSpace X] [DiscreteTopology X] : topologicalKrullDim X ≤ 0

theorem Topology.IsOpenEmbedding.coheight_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsOpenEmbedding f) (Z : TopologicalSpace.IrreducibleCloseds X) : Order.coheight (TopologicalSpace.IrreducibleCloseds.map f ⋯ Z) = Order.coheight Z

theorem Topology.IsOpenEmbedding.coheight_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [QuasiSober Y] [T0Space Y] [QuasiSober X] [T0Space X] {x : X} (f : X → Y) (hf : IsOpenEmbedding f) : Order.coheight (f x) = Order.coheight x

noncomputable def coheightZeroSetOrderIsoIrreducibleComponents {X : Type u_1} [TopologicalSpace X] [QuasiSober X] [T0Space X] : ↑{x : X | Order.coheight x = 0} ≃o ↑(irreducibleComponents X)

In a sober space X, the set of points of coheight 0 in the specialization order is order isomorphic to the set of irreducible components of X.

Equations

• One or more equations did not get rendered due to their size.

theorem QuasiSober.coheight_eq_zero_subset_of_coheight_eq_one {X : Type u_1} [TopologicalSpace X] [QuasiSober X] [IrreducibleSpace X] {p : Set X} (hp : closure p ≠ Set.univ) : {x : X | x ∈ p ∧ Order.coheight x = 1} ⊆ Subtype.val '' {x : ↑p | Order.coheight x = 0}

In a quasi-sober irreducible space X, a point of a non-dense subset p which has coheight 1 in X has coheight 0 in p.

theorem TopologicalSpace.NoetherianSpace.finite_coheight_one_of_closure_ne_univ {X : Type u_1} [TopologicalSpace X] [QuasiSober X] [IrreducibleSpace X] {p : Set X} [T0Space ↑p] [NoetherianSpace ↑p] [QuasiSober ↑p] (hp : closure p ≠ Set.univ) : {x : X | x ∈ p ∧ Order.coheight x = 1}.Finite

In a quasi-sober, irreducible, T0 space X, a Noetherian quasi-sober subspace p whose closure is not all of X contains only finitely many points of coheight 1 (in the specialization order of X).