English
The symmetry of the polynomial quotient isomorphism preserves the expected evaluation mapping, i.e., symmetry aligns eval and map consistently.
Русский
Симметрия изоморфизма квотирования полиномов сохраняет корректность отображения на значения, т.е. соответствия eval и map согласованы.
LaTeX
$$$\\text{polynomialQuotientEquivQuotientPolynomial}_\\text{symm}$ preserves mk-maps: …$$
Lean4
/-- If `I` is an ideal of `R`, then the ring polynomials over the quotient ring `I.quotient` is
isomorphic to the quotient of `R[X]` by the ideal `map C I`,
where `map C I` contains exactly the polynomials whose coefficients all lie in `I`. -/
def polynomialQuotientEquivQuotientPolynomial (I : Ideal R) : (R ⧸ I)[X] ≃+* R[X] ⧸ (map C I : Ideal R[X])
where
toFun :=
eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I : Ideal R[X])).comp C) quotient_map_C_eq_zero)
(Quotient.mk (map C I : Ideal R[X]) X)
invFun := Quotient.lift (map C I : Ideal R[X]) (eval₂RingHom (C.comp (Quotient.mk I)) X) eval₂_C_mk_eq_zero
map_mul' f g := by simp only [coe_eval₂RingHom, eval₂_mul]
map_add' f g := by simp only [eval₂_add, coe_eval₂RingHom]
left_inv := by
intro f
refine Polynomial.induction_on' f ?_ ?_
· intro p q hp hq
simp only [coe_eval₂RingHom] at hp hq
simp only [coe_eval₂RingHom, hp, hq, RingHom.map_add]
· rintro n ⟨x⟩
simp only [← smul_X_eq_monomial, C_mul', Quotient.lift_mk, Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk,
eval₂_X_pow, eval₂_smul, coe_eval₂RingHom, RingHom.map_pow, eval₂_C, RingHom.coe_comp, RingHom.map_mul, eval₂_X,
Function.comp_apply]
right_inv := by
rintro ⟨f⟩
refine Polynomial.induction_on' f ?_ ?_
· intro p q hp hq
simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, map_add, Quotient.lift_mk,
coe_eval₂RingHom] at hp hq ⊢
rw [hp, hq]
· intro n a
simp only [← smul_X_eq_monomial, ← C_mul' a (X ^ n), Quotient.lift_mk, Submodule.Quotient.quot_mk_eq_mk,
Quotient.mk_eq_mk, coe_eval₂RingHom, RingHom.map_pow, eval₂_C, RingHom.coe_comp, RingHom.map_mul, eval₂_X,
Function.comp_apply]
