English
If J is a prime ideal and I ≤ J, then there exists p ∈ I.minimalPrimes with p ≤ J.
Русский
Пусть J — простой идеал и I ≤ J; тогда существует p ∈ I.minimalPrimes such that p ≤ J.
LaTeX
$$$\exists p \in I.minimalPrimes,\ p \le J$$$
Lean4
theorem exists_minimalPrimes_le [J.IsPrime] (e : I ≤ J) : ∃ p ∈ I.minimalPrimes, p ≤ J :=
by
set S := {p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ OrderDual.ofDual p}
suffices h : ∃ m, OrderDual.toDual J ≤ m ∧ Maximal (· ∈ S) m
by
obtain ⟨p, hJp, hp⟩ := h
exact ⟨p, ⟨hp.prop, fun q hq hle ↦ hp.le_of_ge hq hle⟩, hJp⟩
apply zorn_le_nonempty₀
swap
· refine ⟨show J.IsPrime by infer_instance, e⟩
rintro (c : Set (Ideal R)) hc hc' J' hJ'
refine ⟨OrderDual.toDual (sInf c), ⟨Ideal.sInf_isPrime_of_isChain ⟨J', hJ'⟩ hc'.symm fun x hx => (hc hx).1, ?_⟩, ?_⟩
· rw [OrderDual.ofDual_toDual, le_sInf_iff]
exact fun _ hx => (hc hx).2
· rintro z hz
rw [OrderDual.le_toDual]
exact sInf_le hz
