English
There is a canonical isomorphism between polynomials over R/I and the quotient of R[X] by the ideal map(C,I).
Русский
Существует канонический изоморфизм между полиномами над R/I и квотированием R[X] по идеалу map(C,I).
LaTeX
$$$\\text{polynomialQuotientEquivQuotientPolynomial} : (R[X] / (\\operatorname{map} C I)) \\cong (R / I)[X]$$$
Lean4
theorem eval₂_C_mk_eq_zero {I : Ideal R} :
∀ f ∈ (map (C : R →+* R[X]) I : Ideal R[X]), eval₂RingHom (C.comp (Quotient.mk I)) X f = 0 :=
by
intro a ha
rw [← sum_monomial_eq a]
dsimp
rw [eval₂_sum]
refine Finset.sum_eq_zero fun n _ => ?_
dsimp
rw [eval₂_monomial (C.comp (Quotient.mk I)) X]
refine mul_eq_zero_of_left (Polynomial.ext fun m => ?_) (X ^ n)
rw [RingHom.comp_apply, coeff_C]
by_cases h : m = 0
· simpa [h] using Quotient.eq_zero_iff_mem.2 ((mem_map_C_iff.1 ha) n)
· simp [h]
