English
In a PID that is not a field, every maximal ideal has height one: height(m) = 1 for every maximal ideal m.
Русский
В ПИД, не являющемся полем, каждый максимальный идеал имеет высоту 1: высота(m) = 1 для каждого максимального идеала m.
LaTeX
$$$\\operatorname{height}(\\mathfrak{m}) = 1$ для каждого максимального идеала \\mathfrak{m} в PID, не являющемся полем$$
Lean4
/-- In a PID that is not a field, every maximal ideal has height one. -/
theorem height_eq_one_of_isMaximal {R : Type*} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (m : Ideal R)
[m.IsMaximal] (h : ¬IsField R) : m.height = 1 :=
by
refine le_antisymm ?_ ?_
· suffices h : (m.height : WithBot ℕ∞) ≤ 1 by norm_cast at h
rw [← IsPrincipalIdealRing.ringKrullDim_eq_one _ h]
exact Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'
· rw [Order.one_le_iff_pos, Ideal.height_eq_primeHeight, Ideal.primeHeight, Order.height_pos]
exact not_isMin_of_lt (b := ⊥) (Ideal.bot_lt_of_maximal m h)
