English
For any ring R and any n, ringKrullDim R ≤ n iff every prime ideal has height ≤ n.
Русский
Для кольца R и любого n размерность Крull не превышает n тогда и только тогда, когда каждая высота простого идеала ≤ n.
LaTeX
$$$\operatorname{ringKrullDim}(R) \le n \iff \forall p,\; p\text{ prime }\Rightarrow \operatorname{height}(p) \le n.$$$
Lean4
/-- `dim R ≤ n` if and only if the height of all prime ideals is less than `n`. -/
theorem ringKrullDim_le_iff_height_le {R : Type*} [CommRing R] (n : WithBot ℕ∞) :
ringKrullDim R ≤ n ↔ ∀ ⦃p : Ideal R⦄, p.IsPrime → p.height ≤ n :=
by
rw [ringKrullDim, Order.krullDim_eq_iSup_height, iSup_le_iff]
refine ⟨fun h p hp ↦ ?_, fun h p ↦ ?_⟩
· rw [Ideal.height_eq_primeHeight]
exact h ⟨p, hp⟩
· specialize h p.2
rwa [Ideal.height_eq_primeHeight] at h
