English
For a prime ideal I, primeHeight I = 0 if and only if I is a minimal prime over R.
Русский
Для простого идеала I высота primeHeight I равна нулю тогда и только тогда, когда I является минимальным примарным над R.
LaTeX
$$$\operatorname{primeHeight}(I) = 0 \;\iff\; I \in \mathrm{minimalPrimes}(R).$$$
Lean4
/-- A prime ideal has height zero if and only if it is minimal -/
theorem primeHeight_eq_zero_iff {I : Ideal R} [I.IsPrime] : primeHeight I = 0 ↔ I ∈ minimalPrimes R :=
by
rw [Ideal.primeHeight, Order.height_eq_zero, minimalPrimes, Ideal.minimalPrimes]
simp only [bot_le, and_true, Set.mem_setOf_eq, Minimal, IsMin]
constructor
· intro h
by_contra! h'
obtain ⟨P, ⟨hP₁, ⟨hP₂, hP₃⟩⟩⟩ := h' (inferInstance)
exact hP₃ (h (b := ⟨P, hP₁⟩) hP₂)
· rintro ⟨hI, hI'⟩ b hb
exact hI' (y := b.asIdeal) b.isPrime hb
