Quotients of polynomial rings #
For a commutative ring $R$, evaluating a polynomial at an element $x \in R$ induces an isomorphism of $R$-algebras $R[X] / \langle X - x \rangle \cong R$.
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
Equations
- I.polynomial_quotient_equiv_quotient_polynomial = {to_fun := ⇑(polynomial.eval₂_ring_hom (ideal.quotient.lift I ((ideal.quotient.mk (ideal.map polynomial.C I)).comp polynomial.C) ideal.quotient_map_C_eq_zero) (⇑(ideal.quotient.mk (ideal.map polynomial.C I)) polynomial.X)), inv_fun := ⇑(ideal.quotient.lift (ideal.map polynomial.C I) (polynomial.eval₂_ring_hom (polynomial.C.comp (ideal.quotient.mk I)) polynomial.X) ideal.eval₂_C_mk_eq_zero), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
Given any ring R
and an ideal I
of R[X]
, we get a map R → R[x] → R[x]/I
.
If we let R
be the image of R
in R[x]/I
then we also have a map R[x] → R'[x]
.
In particular we can map I
across this map, to get I'
and a new map R' → R'[x] → R'[x]/I
.
This theorem shows I'
will not contain any non-zero constant polynomials
If I
is an ideal of R
, then the ring mv_polynomial σ I.quotient
is isomorphic as an
R
-algebra to the quotient of mv_polynomial σ R
by the ideal generated by I
.
Equations
- mv_polynomial.quotient_equiv_quotient_mv_polynomial I = {to_fun := ⇑(mv_polynomial.eval₂_hom (ideal.quotient.lift I ((ideal.quotient.mk (ideal.map mv_polynomial.C I)).comp mv_polynomial.C) _) (λ (i : σ), ⇑(ideal.quotient.mk (ideal.map mv_polynomial.C I)) (mv_polynomial.X i))), inv_fun := ⇑(ideal.quotient.lift (ideal.map mv_polynomial.C I) (mv_polynomial.eval₂_hom (mv_polynomial.C.comp (ideal.quotient.mk I)) mv_polynomial.X) _), left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}