English
The Krull dimension is the supremum of the heights of all maximal ideals.
Русский
Размерность Крull равна супремуму высот всех максимальных идеалов.
LaTeX
$$$\operatorname{ringKrullDim}(R) = \sup\{\operatorname{height}(\mathfrak m) : \mathfrak m \text{ maximal in } R\}.$$$
Lean4
/-- In a nontrivial commutative ring `R`, the supremum of heights of all ideals is equal to the
Krull dimension of `R`. -/
theorem sup_height_eq_ringKrullDim [Nontrivial R] : ↑(⨆ (I : Ideal R) (_ : I ≠ ⊤), I.height) = ringKrullDim R :=
by
apply le_antisymm
· rw [WithBot.coe_iSup ⟨⊤, fun _ _ => le_top⟩]
refine iSup_le fun I => ?_
by_cases h : I = ⊤
· simp [h, ringKrullDim_nonneg_of_nontrivial]
· simp [h, height_le_ringKrullDim_of_ne_top]
· refine iSup_le fun p => WithBot.coe_le_coe.mpr (le_trans (b := p.last.asIdeal.height) ?_ ?_)
· rw [height_eq_primeHeight]
apply le_trans (b := ⨆ (_ : p.last ≤ p.last), ↑p.length)
· exact le_iSup (fun _ => (↑p.length : ℕ∞)) le_rfl
· exact le_iSup (fun p' => (⨆ _, p'.length : ℕ∞)) p
· apply le_trans (b := ⨆ (_ : (p.last).asIdeal ≠ ⊤), p.last.asIdeal.height)
· exact le_iSup_of_le p.last.isPrime.ne_top' le_rfl
· exact le_iSup (fun I => ⨆ _, I.height) p.last.asIdeal
