Krull dimension of topological spaces: open covers and closed points

This file records facts about the topological Krull dimension and the codimension of points.

The Krull dimension of a space is the supremum of the Krull dimensions of the members of an open cover: an irreducible closed subset meeting an open subset U is the closure of its trace on U, so every chain of irreducible closed subsets of the whole space restricts to a chain of the same length in any open subset containing a point of its smallest member. For schemes this is what reduces dimension computations to affine opens. Similarly, the preimage of a set under an embedding has the Krull dimension of the part of the set lying in the range.

On a T₀ topological space the specialization order is a partial order, so the codimension Order.coheight x of a point is defined: it is the supremum of the lengths of the chains of proper specializations of x. On a space all of whose points have codimension at most one, a point of codimension exactly one is closed, since a proper specialization of such a point would have codimension at least two.

Main declarations

• TauCeti.topologicalKrullDim_eq_iSup_of_isOpenEmbedding: the Krull dimension of a space covered by the ranges of open embeddings is the supremum of the Krull dimensions of their domains.
• Topology.IsEmbedding.topologicalKrullDim_preimage: the preimage of a set under an embedding has the Krull dimension of the part of the set in the range.
• TauCeti.isClosed_singleton_of_forall_coheight_le_one_of_coheight_eq_one: on a T₀ space all of whose points have codimension at most one for the specialization order, a point of codimension one is closed.
• TauCeti.coheight_le_topologicalKrullDim: on a T₀ space, the codimension of a point is at most the Krull dimension of the space.
• TauCeti.topologicalKrullDim_eq_iSup_coheight: on a quasi-sober T₀ space, the Krull dimension is the supremum of the codimensions of the points.

theorem TauCeti.topologicalKrullDim_eq_iSup_of_isOpenEmbedding {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] {Y : ι → Type u_3} [(i : ι) → TopologicalSpace (Y i)] (f : (i : ι) → Y i → X) (hf : ∀ (i : ι), Topology.IsOpenEmbedding (f i)) (hcover : ∀ (x : X), ∃ (i : ι), x ∈ Set.range (f i)) : topologicalKrullDim X = ⨆ (i : ι), topologicalKrullDim (Y i)

The Krull dimension of a space covered by the ranges of a family of open embeddings is the supremum of the Krull dimensions of their domains.

theorem TauCeti.isClosed_singleton_of_forall_coheight_le_one_of_coheight_eq_one {α : Type u_1} [TopologicalSpace α] [T0Space α] (hdim : ∀ (y : α), Order.coheight y ≤ 1) {x : α} (hx : Order.coheight x = 1) : IsClosed {x}

On a T₀ topological space all of whose points have codimension at most one for the specialization order, a point of codimension one is closed.

theorem TauCeti.coheight_le_topologicalKrullDim {α : Type u_1} [TopologicalSpace α] [T0Space α] (x : α) : ↑(Order.coheight x) ≤ topologicalKrullDim α

On a T₀ topological space, the codimension of a point for the specialization order is at most the Krull dimension of the space.

theorem TauCeti.topologicalKrullDim_eq_iSup_coheight (α : Type u_1) [TopologicalSpace α] [QuasiSober α] [T0Space α] : topologicalKrullDim α = ⨆ (x : α), ↑(Order.coheight x)

On a quasi-sober T₀ topological space, the Krull dimension is the supremum of the codimensions of the points for the specialization order: every irreducible closed subset is the closure of a unique generic point.

theorem Topology.IsEmbedding.topologicalKrullDim_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : Y → X} (he : IsEmbedding e) (Z : Set X) : topologicalKrullDim ↑(e ⁻¹' Z) = topologicalKrullDim ↑(Z ∩ Set.range e)

The preimage of a set Z under an embedding e is homeomorphic to the part of Z in the range of e, so the two have the same Krull dimension.