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.

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)

def IrreducibleCloseds.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf1 : Continuous f) (hf2 : IsClosedMap f) (c : TopologicalSpace.IrreducibleCloseds X) : TopologicalSpace.IrreducibleCloseds Y

Map induced on irreducible closed subsets by a closed continuous map f. This is just a wrapper around the image of f together with proofs that it preserves irreducibility (by continuity) and closedness (since f is closed).

Equations

• IrreducibleCloseds.map hf1 hf2 c = { carrier := f '' ↑c, is_irreducible' := ⋯, is_closed' := ⋯ }

theorem IrreducibleCloseds.map_strictMono {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) : StrictMono (IrreducibleCloseds.map ⋯ ⋯)

Taking images under a closed embedding is strictly monotone on the preorder of irreducible closeds.

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

If f : X → Y is a closed embedding, then the Krull dimension of X is less than or equal to the Krull dimension of Y.

@[deprecated IsClosedEmbedding.topologicalKrullDim_le]

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

Alias of IsClosedEmbedding.topologicalKrullDim_le.

---

If f : X → Y is a closed embedding, then the Krull dimension of X is less than or equal to the Krull dimension of Y.

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