English
If I ⊆ J are prime ideals of S and r lies in J but not in I, and p is a nonzero polynomial with p.map(Quotient.mk(I.comap f)) ≠ 0 and p.eval₂ f r ∈ I, then I.comap f is strictly smaller than J.comap f.
Русский
Если I и J — простые идеалы S и r лежит в J, но не в I, и p не нулевой с p.map(Quotient.mk(I.comap f)) ≠ 0, а p.eval₂ f r ∈ I, то I.comap f строго меньше J.comap f.
LaTeX
$$$$\forall R,S\ [\mathrm{CommRing}\ R][\mathrm{CommRing}\ S] (f:R\to+* S)\ I,J:\mathrm{Ideal} S\ [I.IsPrime], (hIJ: I\le J), {r:S}(hr: r \in (J: S) \setminus I), {p:R[X]} (p\neq 0) (p.map(\mathrm{Quotient.mk}(I.comap f)) \neq 0) (hp: p.eval₂ f r \in I) : I.comap f < J.comap f. $$$$
Lean4
theorem comap_lt_comap_of_root_mem_sdiff [I.IsPrime] (hIJ : I ≤ J) {r : S} (hr : r ∈ (J : Set S) \ I) {p : R[X]}
(p_ne_zero : p.map (Quotient.mk (I.comap f)) ≠ 0) (hp : p.eval₂ f r ∈ I) : I.comap f < J.comap f :=
let ⟨i, hJ, hI⟩ := exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff hIJ hr p_ne_zero hp
SetLike.lt_iff_le_and_exists.mpr ⟨comap_mono hIJ, p.coeff i, hJ, hI⟩
