Documentation

Mathlib.Topology.KrullDimension

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 #

Implementation notes #

The proofs use order-preserving maps between posets of irreducible closed sets to establish dimension inequalities.

source
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
Instances For

    Main dimension theorems #

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

    If f : Y → X is inducing, then dim(Y) ≤ dim(X).

    source
    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

    source
    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.

    source
    theorem topologicalKrullDim_zero_of_discreteTopology (X : Type u_3) [TopologicalSpace X] [DiscreteTopology X] :
    topologicalKrullDim X ≤ 0
    source
    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
    source
    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