English
If a ring R has finite Krull dimension, then there exists a maximal ideal whose height equals the Krull dimension of R.
Русский
Если кольцо R имеет конечную размерность Крull, то существует максимальная идеал с высотой, равной размерности Крull кольца R.
LaTeX
$$$\exists \mathfrak m \; (\mathfrak m \text{ maximal}) \land \operatorname{height}(\mathfrak m) = \operatorname{ringKrullDim}(R).$$$
Lean4
/-- If `R` has finite Krull dimension, there exists a maximal ideal `m` with `ht m = dim R`. -/
theorem exists_isMaximal_height [FiniteRingKrullDim R] : ∃ (p : Ideal R), p.IsMaximal ∧ p.height = ringKrullDim R :=
by
let l := LTSeries.longestOf (PrimeSpectrum R)
obtain ⟨m, hm, hle⟩ := l.last.asIdeal.exists_le_maximal IsPrime.ne_top'
refine ⟨m, hm, le_antisymm (height_le_ringKrullDim_of_ne_top IsPrime.ne_top') ?_⟩
trans (l.last.asIdeal.height : WithBot ℕ∞)
· rw [Ideal.height_eq_primeHeight]
exact LTSeries.height_last_longestOf.symm.le
· norm_cast
exact height_mono hle
