English
For any I ideal and a in the image map(I), the evaluation of a under eval₂ with C and quotient equals zero.
Русский
Для любого идеала I и элемента a в образе, вычисление eval₂ с C и квотой даёт нулевой результат.
LaTeX
$$$\\forall I\\, a:\\, a \\in (I.map C) \\Rightarrow eval₂( C, X)\\, a = 0$$$
Lean4
theorem eval₂_C_mk_eq_zero {I : Ideal R} {a : MvPolynomial σ R}
(ha : a ∈ (Ideal.map (C : R →+* MvPolynomial σ R) I : Ideal (MvPolynomial σ R))) :
eval₂Hom (C.comp (Ideal.Quotient.mk I)) X a = 0 :=
by
rw [as_sum a]
rw [coe_eval₂Hom, eval₂_sum]
refine Finset.sum_eq_zero fun n _ => ?_
simp only [eval₂_monomial, Function.comp_apply, RingHom.coe_comp]
refine mul_eq_zero_of_left ?_ _
suffices coeff n a ∈ I by
rw [← @Ideal.mk_ker R _ I, RingHom.mem_ker] at this
simp only [this, C_0]
exact mem_map_C_iff.1 ha n
