English
If I is prime, the ring has finite Krull dimension, and primeHeight I equals ringKrullDim, then I is maximal.
Русский
Если I является простым идеалом и высота I достигает ringKrullDim, то I является максимальным.
LaTeX
$$$[I\text{ prime}][\text{FiniteRingKrullDim}(R)]\; (I.\text{primeHeight} = \operatorname{ringKrullDim} R) \Rightarrow I \text{ is maximal}.$$$
Lean4
theorem isMaximal_of_primeHeight_eq_ringKrullDim {I : Ideal R} [I.IsPrime] [FiniteRingKrullDim R]
(e : I.primeHeight = ringKrullDim R) : I.IsMaximal :=
by
have h : I ≠ ⊤ := by
intro h
simp only [h, ← Ideal.height_eq_primeHeight, Ideal.height_top, WithBot.coe_top] at e
exact ringKrullDim_ne_top e.symm
obtain ⟨M, hM, hM'⟩ := Ideal.exists_le_maximal I h
rcases lt_or_eq_of_le hM' with (hM' | hM')
· have h1 := Ideal.primeHeight_strict_mono hM'
have h2 := e ▸ M.primeHeight_le_ringKrullDim
simp [← not_lt, h1] at h2
· exact hM' ▸ hM
