English
Let I ⊆ J be ideals of S with I prime, and r ∈ J\\I. For any nonzero p ∈ R[X] with p.map(Quotient.mk(I.comap f)) ≠ 0 and p.eval₂ f r ∈ I, there exists i with p.coeff i ∈ J.comap f \\ I.comap f.
Русский
Пусть I ⊆ J — идеалы кольца S, I прост и r ∈ J \ I. Для любого p ∈ R[X], такого что p не тождественно нулевой в соответствующем фактор-пространстве, и p.eval₂ f r ∈ 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),\\ r:\\, S\\ (hr: r \\in (J:\\mathrm{Set}\\, S) \\setminus I),\\ p:\\, R[X],\\ p\\text{ nonzero},\\ p.map(\\mathrm{Quotient.mk}(I.comap f)) \\neq 0,\\ (hpI: p.eval₂ f r \\in I) :\\\\exists i,\\ p.coeff i \\in (J.comap f : \\mathrm{Set} R) \\setminus (I.comap f) . $$$$
Lean4
theorem exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff [IsPrime I] (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) (hpI : p.eval₂ f r ∈ I) :
∃ i, p.coeff i ∈ (J.comap f : Set R) \ I.comap f :=
by
obtain ⟨hrJ, hrI⟩ := hr
have rbar_ne_zero : Ideal.Quotient.mk I r ≠ 0 := mt (Quotient.mk_eq_zero I).mp hrI
have rbar_mem_J : Ideal.Quotient.mk I r ∈ J.map (Ideal.Quotient.mk I) := mem_map_of_mem _ hrJ
have quotient_f : ∀ x ∈ I.comap f, (Ideal.Quotient.mk I).comp f x = 0 := by simp [Quotient.eq_zero_iff_mem]
have rbar_root :
(p.map (Ideal.Quotient.mk (I.comap f))).eval₂ (Quotient.lift (I.comap f) _ quotient_f) (Ideal.Quotient.mk I r) =
0 :=
by
convert Quotient.eq_zero_iff_mem.mpr hpI
exact _root_.trans (eval₂_map _ _ _) (hom_eval₂ p f (Ideal.Quotient.mk I) r).symm
obtain ⟨i, ne_zero, mem⟩ := exists_coeff_ne_zero_mem_comap_of_root_mem rbar_ne_zero rbar_mem_J p_ne_zero rbar_root
rw [coeff_map] at ne_zero mem
refine ⟨i, (mem_quotient_iff_mem hIJ).mp ?_, mt ?_ ne_zero⟩
· simpa using mem
simp [Quotient.eq_zero_iff_mem]
