English
In a Noetherian ring, height ≤ n is equivalent to a covBy-type condition: if q < p and every q' with q < q' avoids p, then q.height < n.
Русский
В кольце Нотереан висота ≤ n эквивалентна условию covBy: если q < p и каждый q' с q < q' не удовлетворяет q' < p, то height(q) < n.
LaTeX
$$$p.height \le n \iff \forall q,\; q.IsPrime \to q < p \to (\forall q',\; q'.IsPrime \to q < q' \to \lnot q' < p) \to q.height < n.$$$
Lean4
theorem height_le_iff_covBy {p : Ideal R} {n : ℕ} [p.IsPrime] [IsNoetherianRing R] :
p.height ≤ n ↔ ∀ q : Ideal R, q.IsPrime → q < p → (∀ q' : Ideal R, q'.IsPrime → q < q' → ¬q' < p) → q.height < n :=
by
rw [Ideal.height_le_iff]
constructor
· intro H q hq e _
exact H q hq e
· intro H q hq e
obtain ⟨⟨x, hx⟩, hqx, hxp⟩ := @exists_le_covBy_of_lt { I : Ideal R // I.IsPrime } ⟨q, hq⟩ ⟨p, ‹_›⟩ _ _ e
exact (Ideal.height_mono hqx).trans_lt (H _ hx hxp.1 (fun I hI e ↦ hxp.2 (show Subtype.mk x hx < ⟨I, hI⟩ from e)))
