Documentation

Mathlib.RingTheory.Polynomial.Quotient

Quotients of polynomial rings #

noncomputable def Polynomial.quotientSpanXSubCAlgEquiv {R : Type u_1} [CommRing R] (x : R) :

For a commutative ring R, evaluating a polynomial at an element xR induces an isomorphism of R-algebras R[X]/XxR.

Equations
noncomputable def Polynomial.quotientSpanCXSubCAlgEquiv {R : Type u_1} [CommRing R] (x y : R) :

For a commutative ring R, evaluating a polynomial at an element yR induces an isomorphism of R-algebras R[X]/x,XyR/x.

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def Polynomial.quotientSpanCXSubCXSubCAlgEquiv {R : Type u_1} [CommRing R] {x : R} {y : Polynomial R} :

For a commutative ring R, evaluating a polynomial at elements y(X)R[X] and xR induces an isomorphism of R-algebras R[X,Y]/Xx,Yy(X)R.

Equations
  • One or more equations did not get rendered due to their size.
theorem Ideal.quotient_map_C_eq_zero {R : Type u_1} [CommRing R] {I : Ideal R} (a : 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
  • One or more equations did not get rendered due to their size.

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

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} [CommRing R] {I : Ideal R} {i : R} (hi : i I) :
theorem MvPolynomial.eval₂_C_mk_eq_zero {R : Type u_1} {σ : Type u_2} [CommRing R] {I : Ideal R} {a : MvPolynomial σ R} (ha : a Ideal.map C I) :
noncomputable def MvPolynomial.quotientEquivQuotientMvPolynomial {R : Type u_1} {σ : Type u_2} [CommRing R] (I : Ideal R) :

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.

Equations
  • One or more equations did not get rendered due to their size.