# Quotients of polynomial rings #

source
noncomputable def Polynomial.quotientSpanXSubCAlgEquiv {R : Type u_1} [CommRing R] (x : R) :
(Polynomial R ⧸ Ideal.span {X - 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 = (Ideal.quotientEquivAlgOfEq R ⋯).trans { toEquiv := (RingHom.quotientKerEquivOfRightInverse ⋯).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source
@[simp]
theorem Polynomial.quotientSpanXSubCAlgEquiv_mk {R : Type u_1} [CommRing R] (x : R) (p : Polynomial R) :
(quotientSpanXSubCAlgEquiv x) ((Ideal.Quotient.mk (Ideal.span {X - C x})) p) = eval x p
source
@[simp]
theorem Polynomial.quotientSpanXSubCAlgEquiv_symm_apply {R : Type u_1} [CommRing R] (x y : R) :
(quotientSpanXSubCAlgEquiv x).symm y = (algebraMap R (Polynomial R ⧸ Ideal.span {X - C x})) y
source
noncomputable def Polynomial.quotientSpanCXSubCAlgEquiv {R : Type u_1} [CommRing R] (x y : R) :
(Polynomial R ⧸ Ideal.span {C x, X - 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.

Instances For

source
noncomputable def Polynomial.quotientSpanCXSubCXSubCAlgEquiv {R : Type u_1} [CommRing R] {x : R} {y : Polynomial R} :
(Polynomial (Polynomial R) ⧸ Ideal.span {C (X - C x), X - 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.

Instances For

source
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
source
theorem Ideal.quotient_map_C_eq_zero {R : Type u_1} [CommRing R] {I : Ideal R} (a : R) :
a ∈ I → ((Quotient.mk (map Polynomial.C I)).comp Polynomial.C) a = 0
source
theorem Ideal.eval₂_C_mk_eq_zero {R : Type u_1} [CommRing R] {I : Ideal R} (f : Polynomial R) :
f ∈ map Polynomial.C I → (Polynomial.eval₂RingHom (Polynomial.C.comp (Quotient.mk I)) Polynomial.X) f = 0
source
def Ideal.polynomialQuotientEquivQuotientPolynomial {R : Type u_1} [CommRing R] (I : Ideal R) :
Polynomial (R ⧸ I) ≃+* Polynomial R ⧸ 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.

Instances For

source
@[simp]
theorem Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk {R : Type u_1} [CommRing R] (I : Ideal R) (f : Polynomial R) :
I.polynomialQuotientEquivQuotientPolynomial.symm ((Quotient.mk (map Polynomial.C I)) f) = Polynomial.map (Quotient.mk I) f
source
@[simp]
theorem Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk {R : Type u_1} [CommRing R] (I : Ideal R) (f : Polynomial R) :
I.polynomialQuotientEquivQuotientPolynomial (Polynomial.map (Quotient.mk I) f) = (Quotient.mk (map Polynomial.C I)) f
source
theorem Ideal.isDomain_map_C_quotient {R : Type u_1} [CommRing R] {P : Ideal R} :
P.IsPrime → IsDomain (Polynomial R ⧸ map Polynomial.C P)

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

source
theorem Ideal.eq_zero_of_polynomial_mem_map_range {R : Type u_1} [CommRing R] (I : Ideal (Polynomial R)) (x : ↥((Quotient.mk I).comp Polynomial.C).range) (hx : Polynomial.C x ∈ map (Polynomial.mapRingHom ((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.

source
theorem Ideal.IsField.of_isPrincipalIdealRing_polynomial {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing (Polynomial R)] :
IsField R

Given a domain `R`, if `R[X]` is a principal ideal ring, then `R` is a field.

source
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 C I)).comp C) i = 0
source
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) :
(eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) a = 0
source
theorem MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse {R : Type u_1} {σ : Type u_2} [CommRing R] (I : Ideal R) :
Function.RightInverse (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯) fun (i : σ) => (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ⇑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)

Split off from `quotientEquivQuotientMvPolynomial` for speed.

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

Split off from `quotientEquivQuotientMvPolynomial` for speed.

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

Instances For