# Documentation

Mathlib.RingTheory.Polynomial.Quotient

# Quotients of polynomial rings #

noncomputable def Polynomial.quotientSpanXSubCAlgEquivAux2 {R : Type u_1} [] (x : R) :
() ≃ₐ[R] R
Instances For
noncomputable def Polynomial.quotientSpanXSubCAlgEquivAux1 {R : Type u_1} [] (x : R) :
( Ideal.span {Polynomial.X - Polynomial.C x}) ≃ₐ[R]
Instances For
noncomputable def Polynomial.quotientSpanXSubCAlgEquiv {R : Type u_1} [] (x : R) :
( Ideal.span {Polynomial.X - Polynomial.C x}) ≃ₐ[R] R

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$.

Instances For
@[simp]
theorem Polynomial.quotientSpanXSubCAlgEquiv_mk {R : Type u_1} [] (x : R) (p : ) :
↑() (↑(Ideal.Quotient.mk (Ideal.span {Polynomial.X - Polynomial.C x})) p) =
@[simp]
theorem Polynomial.quotientSpanXSubCAlgEquiv_symm_apply {R : Type u_1} [] (x : R) (y : R) :
= ↑(algebraMap R ( Ideal.span {Polynomial.X - Polynomial.C x})) y
noncomputable def Polynomial.quotientSpanCXSubCAlgEquiv {R : Type u_1} [] (x : R) (y : R) :
( Ideal.span {Polynomial.C x, Polynomial.X - Polynomial.C y}) ≃ₐ[R] R Ideal.span {x}

For a commutative ring $R$, evaluating a polynomial at an element $y \in R$ induces an isomorphism of $R$-algebras $R[X] / \langle x, X - y \rangle \cong R / \langle x \rangle$.

Instances For
noncomputable def Polynomial.quotientSpanCXSubCXSubCAlgEquiv {R : Type u_1} [] {x : R} {y : } :
( Ideal.span {Polynomial.C (Polynomial.X - Polynomial.C x), Polynomial.X - Polynomial.C y}) ≃ₐ[R] R

For a commutative ring $R$, evaluating a polynomial at elements $y(X) \in R[X]$ and $x \in R$ induces an isomorphism of $R$-algebras $R[X, Y] / \langle X - x, Y - y(X) \rangle \cong R$.

Instances For
theorem Ideal.quotient_map_C_eq_zero {R : Type u_1} [] {I : } (a : R) :
a I↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map Polynomial.C I)) Polynomial.C) a = 0
theorem Ideal.eval₂_C_mk_eq_zero {R : Type u_1} [] {I : } (f : ) :
f Ideal.map Polynomial.C I↑(Polynomial.eval₂RingHom (RingHom.comp Polynomial.C ()) Polynomial.X) f = 0

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.

Instances For
@[simp]
theorem Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk {R : Type u_1} [] (I : ) (f : ) :
↑() (↑(Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f) =
@[simp]
theorem Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk {R : Type u_1} [] (I : ) (f : ) :
= ↑(Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f
theorem Ideal.isDomain_map_C_quotient {R : Type u_1} [] {P : } :
IsDomain ( Ideal.map Polynomial.C P)

If P is a prime ideal of R, then R[x]/(P) is an integral domain.

theorem Ideal.eq_zero_of_polynomial_mem_map_range {R : Type u_1} [] (I : Ideal ()) (x : { x // x RingHom.range (RingHom.comp () Polynomial.C) }) (hx : Polynomial.C x Ideal.map (Polynomial.mapRingHom (RingHom.rangeRestrict (RingHom.comp () Polynomial.C))) I) :
x = 0

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.

theorem MvPolynomial.quotient_map_C_eq_zero {R : Type u_1} {σ : Type u_2} [] {I : } {i : R} (hi : i I) :
↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) MvPolynomial.C) i = 0
theorem MvPolynomial.eval₂_C_mk_eq_zero {R : Type u_1} {σ : Type u_2} [] {I : } {a : } (ha : a Ideal.map MvPolynomial.C I) :
↑(MvPolynomial.eval₂Hom (RingHom.comp MvPolynomial.C ()) MvPolynomial.X) a = 0
theorem MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse {R : Type u_1} {σ : Type u_2} [] (I : ) :
Function.RightInverse (MvPolynomial.eval₂ (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) MvPolynomial.C) (_ : ∀ (i : R), i I↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) MvPolynomial.C) i = 0)) fun i => ↑(Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) ()) ↑(Ideal.Quotient.lift (Ideal.map MvPolynomial.C I) (MvPolynomial.eval₂Hom (RingHom.comp MvPolynomial.C ()) MvPolynomial.X) (_ : ∀ (a : ), a Ideal.map MvPolynomial.C I↑(MvPolynomial.eval₂Hom (RingHom.comp MvPolynomial.C ()) MvPolynomial.X) a = 0))
theorem MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse {R : Type u_1} {σ : Type u_2} [] (I : ) :
Function.LeftInverse (MvPolynomial.eval₂ (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) MvPolynomial.C) (_ : ∀ (i : R), i I↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) MvPolynomial.C) i = 0)) fun i => ↑(Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) ()) ↑(Ideal.Quotient.lift (Ideal.map MvPolynomial.C I) (MvPolynomial.eval₂Hom (RingHom.comp MvPolynomial.C ()) MvPolynomial.X) (_ : ∀ (a : ), a Ideal.map MvPolynomial.C I↑(MvPolynomial.eval₂Hom (RingHom.comp MvPolynomial.C ()) MvPolynomial.X) a = 0))
noncomputable def MvPolynomial.quotientEquivQuotientMvPolynomial {R : Type u_1} {σ : Type u_2} [] (I : ) :
MvPolynomial σ (R I) ≃ₐ[R] Ideal.map MvPolynomial.C I

If I is an ideal of R, then the ring MvPolynomial σ I.quotient is isomorphic as an R-algebra to the quotient of MvPolynomial σ R by the ideal generated by I.

Instances For