English
Let P be a proper ideal of R[x] with a property that no nonzero element of R lies in P, i.e., P ∩ R = (0). Then there exists a polynomial p ∈ P such that its image in the quotient by P ∩ R is nonzero.
Русский
Пусть P — properideal R[x] и P ∩ R = (0). Тогда существует многочлен p ∈ P, чьёобразование в фактор-пространстве R[x]/(P ∩ R)[x] не равно нулю.
LaTeX
$$$\\exists p \\in P\\; (\\operatorname{Polynomial.map}(\\operatorname{Quotient.mk}(P^{\\mathrm{comap}}) )p \\neq 0).$$$
Lean4
/-- This technical lemma asserts the existence of a polynomial `p` in an ideal `P ⊂ R[x]`
that is non-zero in the quotient `R / (P ∩ R) [x]`. The assumptions are equivalent to
`P ≠ 0` and `P ∩ R = (0)`.
-/
theorem exists_nonzero_mem_of_ne_bot {P : Ideal R[X]} (Pb : P ≠ ⊥) (hP : ∀ x : R, C x ∈ P → x = 0) :
∃ p : R[X], p ∈ P ∧ Polynomial.map (Quotient.mk (P.comap (C : R →+* R[X]))) p ≠ 0 :=
by
obtain ⟨m, hm⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr Pb)
refine ⟨m, Submodule.coe_mem m, fun pp0 => hm (Submodule.coe_eq_zero.mp ?_)⟩
refine (injective_iff_map_eq_zero (Polynomial.mapRingHom (Ideal.Quotient.mk (P.comap (C : R →+* R[X]))))).mp ?_ _ pp0
refine map_injective _ ((RingHom.injective_iff_ker_eq_bot (Ideal.Quotient.mk (P.comap C))).mpr ?_)
rw [mk_ker]
exact (Submodule.eq_bot_iff _).mpr fun x hx => hP x (mem_comap.mp hx)
