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.

For the specialization preorder, defined on any topological space, the codimension Order.coheight x of a point is the supremum of the lengths of the chains of proper generalizations of x. On a T₀ space the specialization preorder is a partial order; there, 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: the codimension of a point for the specialization preorder is at most the Krull dimension of the space.
• TauCeti.topologicalKrullDim_eq_iSup_coheight: on a quasi-sober space, the Krull dimension is the supremum of the codimensions of the points for the specialization preorder.
• TauCeti.height_eq_topologicalKrullDim_closure_singleton: on a quasi-sober T₀ space, the height of a point for the specialization preorder is the Krull dimension of its closure.
• TauCeti.topologicalKrullDim_closure_singleton_le_of_not_isMax: on a quasi-sober T₀ space all of whose points have codimension at most d + 1, the closure of a point that is not the generic point of an irreducible component has dimension at most d.
• GeneralizingMap.coheight_apply_le_coheight: a continuous generalizing map cannot increase the codimension of a point.
• GeneralizingMap.topologicalKrullDim_le_of_surjective: the target of a continuous, surjective, generalizing map to a quasi-sober space has dimension at most its source.

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 α] (x : α) : ↑(Order.coheight x) ≤ topologicalKrullDim α

The codimension of a point for the specialization preorder is at most the Krull dimension of the space.

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

On a quasi-sober topological space, the Krull dimension is the supremum of the codimensions of the points for the specialization preorder: generic points of a chain of irreducible closed subsets form a chain of proper generalizations.

theorem TauCeti.height_eq_topologicalKrullDim_closure_singleton {α : Type u_1} [TopologicalSpace α] [QuasiSober α] [T0Space α] (x : α) : ↑(Order.height x) = topologicalKrullDim ↑(closure {x})

On a quasi-sober T₀ topological space, the height of a point for the specialization preorder (x ≤ y ↔ y ⤳ x) is the Krull dimension of its closure: the points below x are the points of closure {x}, and they correspond to its irreducible closed subsets.

theorem TauCeti.topologicalKrullDim_closure_singleton_le_of_not_isMax {α : Type u_1} [TopologicalSpace α] [QuasiSober α] [T0Space α] {d : ℕ} (hdim : ∀ (y : α), Order.coheight y ≤ ↑d + 1) {x : α} (hx : ¬IsMax x) : topologicalKrullDim ↑(closure {x}) ≤ ↑d

On a quasi-sober T₀ topological space all of whose points have codimension at most d + 1 for the specialization preorder, the closure of a point x which is not maximal, that is, not the generic point of an irreducible component, has Krull dimension at most d: a chain of specializations of x extends by a proper generalization of x. For instance, a prime divisor on a scheme of dimension at most two is a curve.

theorem GeneralizingMap.coheight_apply_le_coheight {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : GeneralizingMap f) (hcont : Continuous f) (x : X) : Order.coheight (f x) ≤ Order.coheight x

A continuous generalizing map cannot increase the coheight of a point for the specialization preorders: chains of proper generalizations lift along the map.

theorem GeneralizingMap.topologicalKrullDim_le_of_surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [QuasiSober Y] {f : X → Y} (hf : GeneralizingMap f) (hcont : Continuous f) (hsurj : Function.Surjective f) : topologicalKrullDim Y ≤ topologicalKrullDim X

The target of a continuous, surjective, generalizing map to a quasi-sober space has Krull dimension at most that of the source.

theorem Topology.IsOpenEmbedding.coheight_subtype_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsOpenEmbedding f) {T : Set X} {F : Set Y} (hTF : ∀ (v : X), v ∈ T ↔ f v ∈ F) {x : X} (hx : x ∈ T) : Order.coheight ⟨x, hx⟩ = Order.coheight ⟨f x, ⋯⟩

Along an open embedding f, the coheight of a point x of a subset T of the source, in the specialization order of T, is the coheight of f x in a subset F of the target with v ∈ T ↔ f v ∈ F: open sets are closed under generization, so chains of generizations in F lift to T. For T = f ⁻¹' F this is the subset version of Topology.IsOpenEmbedding.coheight_eq.

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.