English
For prime I ≤ J and r ∈ (J \ I), and p ∈ R[X] with p.map(Quotient.mk(I.comap f)) ≠ 0 and p.eval₂ f r ∈ I, there exists a coefficient i with p.coeff i ∈ (J.comap f) \ (I.comap f).
Русский
При I ⊊ J простых и r ∈ (J \ I), а p ∈ R[X] с p.map(...) ≠ 0 и p.eval₂ f r ∈ I существует коэффициент i, такой что p.coeff i ∈ (J.comap f) \ (I.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), (hr: r\in (J: Set 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) : \exists i, p.coeff i \in (J.comap f : \mathrm{Set} R) \setminus I.comap f. $$$$
Lean4
theorem comap_lt_comap_of_integral_mem_sdiff [Algebra R S] [hI : I.IsPrime] (hIJ : I ≤ J) {x : S}
(mem : x ∈ (J : Set S) \ I) (integral : IsIntegral R x) : I.comap (algebraMap R S) < J.comap (algebraMap R S) :=
by
obtain ⟨p, p_monic, hpx⟩ := integral
refine comap_lt_comap_of_root_mem_sdiff hIJ mem (map_monic_ne_zero p_monic) ?_
convert I.zero_mem
