Quotients of polynomial rings

noncomputable def Polynomial.quotientSpanXSubCAlgEquivAux2 {R : Type u_1} [CommRing R] (x : R) : (Polynomial R ⧸ RingHom.ker (Polynomial.aeval x).toRingHom) ≃ₐ[R] R

Equations

• Polynomial.quotientSpanXSubCAlgEquivAux2 x = { toEquiv := (RingHom.quotientKerEquivOfRightInverse ⋯).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

noncomputable def Polynomial.quotientSpanXSubCAlgEquivAux1 {R : Type u_1} [CommRing R] (x : R) : (Polynomial R ⧸ Ideal.span {Polynomial.X - Polynomial.C x}) ≃ₐ[R] Polynomial R ⧸ RingHom.ker (Polynomial.aeval x).toRingHom

Equations

• Polynomial.quotientSpanXSubCAlgEquivAux1 x = Ideal.quotientEquivAlgOfEq R ⋯

noncomputable def Polynomial.quotientSpanXSubCAlgEquiv {R : Type u_1} [CommRing R] (x : R) : (Polynomial 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$.

Equations

• Polynomial.quotientSpanXSubCAlgEquiv x = (Polynomial.quotientSpanXSubCAlgEquivAux1 x).trans (Polynomial.quotientSpanXSubCAlgEquivAux2 x)

@[simp]

theorem Polynomial.quotientSpanXSubCAlgEquiv_mk {R : Type u_1} [CommRing R] (x : R) (p : Polynomial R) : (Polynomial.quotientSpanXSubCAlgEquiv x) ((Ideal.Quotient.mk (Ideal.span {Polynomial.X - Polynomial.C x})) p) = Polynomial.eval x p

@[simp]

theorem Polynomial.quotientSpanXSubCAlgEquiv_symm_apply {R : Type u_1} [CommRing R] (x y : R) : (Polynomial.quotientSpanXSubCAlgEquiv x).symm y = (algebraMap R (Polynomial R ⧸ Ideal.span {Polynomial.X - Polynomial.C x})) y

noncomputable def Polynomial.quotientSpanCXSubCAlgEquiv {R : Type u_1} [CommRing R] (x y : R) : (Polynomial 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$.

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} : (Polynomial (Polynomial R) ⧸ 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$.

Equations

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

theorem Polynomial.modByMonic_eq_zero_iff_quotient_eq_zero {R : Type u_1} [CommRing R] (p q : Polynomial R) (hq : q.Monic) : p %ₘ q = 0 ↔ (Ideal.Quotient.mk (Ideal.span {q})) p = 0

theorem Ideal.quotient_map_C_eq_zero {R : Type u_1} [CommRing R] {I : Ideal R} (a : R) : a ∈ I → ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)).comp Polynomial.C) a = 0

theorem Ideal.eval₂_C_mk_eq_zero {R : Type u_1} [CommRing R] {I : Ideal R} (f : Polynomial R) : f ∈ Ideal.map Polynomial.C I → (Polynomial.eval₂RingHom (Polynomial.C.comp (Ideal.Quotient.mk I)) Polynomial.X) f = 0

def Ideal.polynomialQuotientEquivQuotientPolynomial {R : Type u_1} [CommRing R] (I : Ideal R) : Polynomial (R ⧸ I) ≃+* Polynomial R ⧸ Ideal.map Polynomial.C I

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.

@[simp]

theorem Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk {R : Type u_1} [CommRing R] (I : Ideal R) (f : Polynomial R) : I.polynomialQuotientEquivQuotientPolynomial.symm ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f) = Polynomial.map (Ideal.Quotient.mk I) f

@[simp]

theorem Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk {R : Type u_1} [CommRing R] (I : Ideal R) (f : Polynomial R) : I.polynomialQuotientEquivQuotientPolynomial (Polynomial.map (Ideal.Quotient.mk I) f) = (Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f

theorem Ideal.isDomain_map_C_quotient {R : Type u_1} [CommRing R] {P : Ideal R} : P.IsPrime → IsDomain (Polynomial R ⧸ 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} [CommRing R] (I : Ideal (Polynomial R)) (x : ↥((Ideal.Quotient.mk I).comp Polynomial.C).range) (hx : Polynomial.C x ∈ Ideal.map (Polynomial.mapRingHom ((Ideal.Quotient.mk I).comp Polynomial.C).rangeRestrict) 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} [CommRing R] {I : Ideal R} {i : R} (hi : i ∈ I) : ((Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)).comp MvPolynomial.C) i = 0

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 MvPolynomial.C I) : (MvPolynomial.eval₂Hom (MvPolynomial.C.comp (Ideal.Quotient.mk I)) MvPolynomial.X) a = 0

theorem MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse {R : Type u_1} {σ : Type u_2} [CommRing R] (I : Ideal R) : Function.RightInverse (MvPolynomial.eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)).comp MvPolynomial.C) ⋯) fun (i : σ) => (Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) (MvPolynomial.X i)) ⇑(Ideal.Quotient.lift (Ideal.map MvPolynomial.C I) (MvPolynomial.eval₂Hom (MvPolynomial.C.comp (Ideal.Quotient.mk I)) MvPolynomial.X) ⋯)

theorem MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse {R : Type u_1} {σ : Type u_2} [CommRing R] (I : Ideal R) : Function.LeftInverse (MvPolynomial.eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)).comp MvPolynomial.C) ⋯) fun (i : σ) => (Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) (MvPolynomial.X i)) ⇑(Ideal.Quotient.lift (Ideal.map MvPolynomial.C I) (MvPolynomial.eval₂Hom (MvPolynomial.C.comp (Ideal.Quotient.mk I)) MvPolynomial.X) ⋯)

noncomputable def MvPolynomial.quotientEquivQuotientMvPolynomial {R : Type u_1} {σ : Type u_2} [CommRing R] (I : Ideal R) : MvPolynomial σ (R ⧸ I) ≃ₐ[R] MvPolynomial σ 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.

Equations

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