Topological Krull Dimension

API for topological Krull dimension on irreducible spaces.

Main results

• TopologicalSpace.IrreducibleCloseds.eq_univ_of_topologicalKrullDim_nonpos: on an irreducible space with dim ≤ 0, every irreducible closed set is the whole space
• opens_eq_bot_or_top_of_irreducibleSpace_dim_zero: on an irreducible dim-0 space, the only opens are ⊥ and ⊤
• topologicalKrullDim_nonneg: non-empty spaces have dim ≥ 0
• topologicalKrullDim_subspace_lt_of_lt: strict ambient upper bounds descend to subspaces
• topologicalKrullDim_lt_top_of_lt_nat: natural-number upper bounds imply finiteness
• topologicalKrullDim_lt_nat_of_lt_of_lt_nat_succ: if dim Y < dim X < n + 1, then dim Y < n
• topologicalKrullDim_lt_of_isIrreducible_of_isClosed: proper closed subsets of irreducible spaces with finite dim have strictly smaller dim
• topologicalKrullDim_pos_iff_exists_irreducibleCloseds_ne_univ: on an irreducible space, dim > 0 iff there is a proper irreducible closed subset
• exists_closed_subset_lt_topologicalKrullDim_of_irreducible_pos: on an irreducible space of positive finite Krull dimension, there exists a proper closed subset of strictly smaller dimension

Irreducible spaces of dimension 0

theorem TopologicalSpace.IrreducibleCloseds.eq_univ_of_topologicalKrullDim_nonpos {X : Type u} [TopologicalSpace X] [IrreducibleSpace X] (S : IrreducibleCloseds X) (hdim : topologicalKrullDim X ≤ 0) : ↑S = Set.univ

On an irreducible space with topologicalKrullDim ≤ 0, every irreducible closed subset equals the whole space.

theorem opens_eq_bot_or_top_of_irreducibleSpace_dim_zero {X : Type u} [TopologicalSpace X] [IrreducibleSpace X] (hdim : topologicalKrullDim X ≤ 0) (U : TopologicalSpace.Opens X) : U = ⊥ ∨ U = ⊤

On an irreducible space of dimension ≤ 0, the only opens are ⊥ and ⊤. Every point is dense, so any nonempty open contains every point.

Dimension helpers

theorem topologicalKrullDim_nonneg {X : Type u} [TopologicalSpace X] [Nonempty X] : topologicalKrullDim X ≥ 0

On a non-empty topological space, the topological Krull dimension is ≥ 0.

theorem topologicalKrullDim_subspace_lt_of_lt {X : Type u} [TopologicalSpace X] (Y : Set X) {a : WithBot ℕ∞} (ha : topologicalKrullDim X < a) : topologicalKrullDim ↑Y < a

Any strict upper bound on the topological Krull dimension of a space also bounds the dimension of each subspace.

theorem topologicalKrullDim_lt_top_of_lt_nat {X : Type u} [TopologicalSpace X] {m : ℕ} (hm : topologicalKrullDim X < ↑m) : topologicalKrullDim X < ⊤

A natural-number upper bound on the topological Krull dimension implies that the dimension is finite.

theorem topologicalKrullDim_lt_nat_of_lt_of_lt_nat_succ {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {n : ℕ} (hYX : topologicalKrullDim Y < topologicalKrullDim X) (hXn : topologicalKrullDim X < ↑(n + 1)) : topologicalKrullDim Y < ↑n

If Y has strictly smaller topological Krull dimension than X, then any natural-number upper bound dim X < n + 1 descends to the predecessor bound dim Y < n.

noncomputable def TopologicalSpace.IrreducibleCloseds.height {X : Type u} [TopologicalSpace X] (S : IrreducibleCloseds X) : ℕ∞

The height of an irreducible closed subset in the inclusion order.

Equations

• S.height = Order.height S

theorem TopologicalSpace.IrreducibleCloseds.height_add_one_le {X : Type u} [TopologicalSpace X] {S T : IrreducibleCloseds X} (hST : S < T) : S.height + 1 ≤ T.height

theorem TopologicalSpace.IrreducibleCloseds.height_le_topologicalKrullDim {X : Type u} [TopologicalSpace X] (S : IrreducibleCloseds X) : ↑S.height ≤ topologicalKrullDim X

theorem TopologicalSpace.IrreducibleCloseds.height_le_height_map_of_isInducing {X : Type u} [TopologicalSpace X] {Y : Type u_1} [TopologicalSpace Y] {f : Y → X} (hf : Topology.IsInducing f) (S : IrreducibleCloseds Y) : S.height ≤ (map f ⋯ S).height

theorem TopologicalSpace.IrreducibleCloseds.height_add_one_le_topologicalKrullDim_of_isClosed_of_ne_univ {X : Type u} [TopologicalSpace X] [IrreducibleSpace X] {Y : Set X} (hY : IsClosed Y) (hne : Y ≠ Set.univ) (S : IrreducibleCloseds ↑Y) : ↑S.height + 1 ≤ topologicalKrullDim X

An irreducible closed subset of a proper closed subspace of an irreducible space has height at most one less than the ambient topological Krull dimension.

theorem TopologicalSpace.topologicalKrullDim_eq_iSup_height (X : Type u) [TopologicalSpace X] : topologicalKrullDim X = ⨆ (S : IrreducibleCloseds X), ↑S.height

The topological Krull dimension is the supremum of the heights of irreducible closed sets.

theorem TopologicalSpace.topologicalKrullDim_add_one_eq_iSup_height_add_one (X : Type u) [TopologicalSpace X] : topologicalKrullDim X + 1 = ⨆ (S : IrreducibleCloseds X), ↑S.height + 1

The topological Krull dimension plus one is the supremum of the heights of irreducible closed sets, each shifted by one.

theorem topologicalKrullDim_add_one_le_of_isIrreducible_of_isClosed {X : Type u} [TopologicalSpace X] [IrreducibleSpace X] {Y : Set X} (hY : IsClosed Y) (hne : Y ≠ Set.univ) : topologicalKrullDim ↑Y + 1 ≤ topologicalKrullDim X

Unconditional: topologicalKrullDim Y + 1 ≤ topologicalKrullDim X for Y ⊊ X closed in irreducible X.

theorem topologicalKrullDim_lt_of_isIrreducible_of_isClosed {X : Type u} [TopologicalSpace X] [IrreducibleSpace X] {Y : Set X} (hY : IsClosed Y) (hne : Y ≠ Set.univ) (hfin : topologicalKrullDim ↑Y < ⊤) : topologicalKrullDim ↑Y < topologicalKrullDim X

On an irreducible space, a proper closed subset with finite Krull dimension has strictly smaller Krull dimension. The finiteness hypothesis excludes the case where both Y and X have infinite dimension.

theorem topologicalKrullDim_pos_iff_exists_irreducibleCloseds_ne_univ {X : Type u} [TopologicalSpace X] [IrreducibleSpace X] : topologicalKrullDim X > 0 ↔ ∃ (Z : TopologicalSpace.IrreducibleCloseds X), ↑Z ≠ Set.univ

On an irreducible space, positive topological Krull dimension is equivalent to the existence of a proper irreducible closed subset.

theorem exists_closed_subset_lt_topologicalKrullDim_of_irreducible_pos {X : Type u} [TopologicalSpace X] [IrreducibleSpace X] (hpos : topologicalKrullDim X > 0) (hX_lt_top : topologicalKrullDim X < ⊤) : ∃ (Z : Set X), IsClosed Z ∧ Z ≠ Set.univ ∧ topologicalKrullDim ↑(TopCat.of ↑Z) < topologicalKrullDim X

On an irreducible space of positive finite Krull dimension, one can choose a proper closed subset Z ⊊ X of strictly smaller Krull dimension. This isolates the structural closed-subset choice from the separate task of passing numerical bounds to Z.