English
For a prime p in a Noetherian ring, p.height ≤ n iff there exists an ideal I with p ∈ minimalPrimes(I) and spanRank(I) ≤ n (in ENat sense).
Русский
Для простого p в кольце Ноetherian высота p ≤ n тогда и только тогда, когда существует идеал I с p ∈ minimalPrimes(I) и spanRank(I) ≤ n (в смысле ENat).
LaTeX
$$$p.height \le n \iff \exists I: \mathrm{Ideal}(R), p \in I.minimalPrimes \land I.spanRank \le n$$$
Lean4
/-- In a commutative Noetherian ring `R`, a prime ideal `p` has height no greater than `n` if and
only if it is a minimal ideal over some ideal generated by no more than `n` elements. -/
theorem height_le_iff_exists_minimalPrimes (p : Ideal R) [p.IsPrime] (n : ℕ∞) :
p.height ≤ n ↔ ∃ I : Ideal R, p ∈ I.minimalPrimes ∧ I.spanRank ≤ n :=
by
constructor
· intro h
obtain ⟨I, hI, e₁, e₂⟩ := exists_spanRank_eq_and_height_eq p (IsPrime.ne_top ‹_›)
refine ⟨I, Ideal.mem_minimalPrimes_of_height_eq hI e₂.ge, e₁.symm ▸ ?_⟩
norm_cast
· rintro ⟨I, hp, hI⟩
exact
le_trans (Ideal.height_le_spanRank_toENat_of_mem_minimal_primes I p hp)
(by simpa using (Cardinal.toENat.monotone' hI))
