English
Let P be a prime ideal of R, I an ideal of S, and le: I.comap f ≤ P. Then there exists a prime ideal Q with I ≤ Q and Q.comap f ≤ P.
Русский
Пусть P — простый идеал R, I — идеал S, и le: I.comap f ≤ P. Тогда существуетPrime-идеал Q такой, что I ≤ Q и Q.comap f ≤ P.
LaTeX
$$$\exists Q \ge I,\ Q \text{ IsPrime} \wedge Q.{\comap f} \le P$$$
Lean4
theorem exists_ideal_comap_le_prime {S} [CommSemiring S] [FunLike F R S] [RingHomClass F R S] {f : F} (P : Ideal R)
[P.IsPrime] (I : Ideal S) (le : I.comap f ≤ P) : ∃ Q ≥ I, Q.IsPrime ∧ Q.comap f ≤ P :=
have ⟨Q, hQ, hIQ, disj⟩ :=
I.exists_le_prime_disjoint (P.primeCompl.map f) <|
Set.disjoint_left.mpr fun _ ↦ by rintro hI ⟨r, hp, rfl⟩; exact hp (le hI)
⟨Q, hIQ, hQ, fun r hp' ↦ of_not_not fun hp ↦ Set.disjoint_left.mp disj hp' ⟨_, hp, rfl⟩⟩
