Quotients of polynomial rings #
noncomputable def
Polynomial.quotientSpanXSubCAlgEquivAux2
{R : Type u_1}
[CommRing R]
(x : R)
:
(Polynomial R ⧸ RingHom.ker ↑(Polynomial.aeval x)) ≃ₐ[R] R
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
Equations
- Polynomial.quotientSpanXSubCAlgEquivAux1 x = Ideal.quotientEquivAlgOfEq R (_ : Ideal.span {Polynomial.X - Polynomial.C x} = RingHom.ker (Polynomial.evalRingHom x))
Instances For
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
Instances For
@[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 : R)
(y : R)
:
(AlgEquiv.symm (Polynomial.quotientSpanXSubCAlgEquiv x)) y = (algebraMap R (Polynomial R ⧸ Ideal.span {Polynomial.X - Polynomial.C x})) y
noncomputable def
Polynomial.quotientSpanCXSubCAlgEquiv
{R : Type u_1}
[CommRing R]
(x : R)
(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.
Instances For
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.
Instances For
theorem
Ideal.quotient_map_C_eq_zero
{R : Type u_1}
[CommRing R]
{I : Ideal R}
(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}
[CommRing R]
{I : Ideal R}
(f : Polynomial R)
:
f ∈ Ideal.map Polynomial.C I →
(Polynomial.eval₂RingHom (RingHom.comp Polynomial.C (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.
Instances For
@[simp]
theorem
Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk
{R : Type u_1}
[CommRing R]
(I : Ideal R)
(f : Polynomial R)
:
(RingEquiv.symm (Ideal.polynomialQuotientEquivQuotientPolynomial I))
((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)
:
(Ideal.polynomialQuotientEquivQuotientPolynomial I) (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}
:
Ideal.IsPrime P → 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 : ↥(RingHom.range (RingHom.comp (Ideal.Quotient.mk I) Polynomial.C)))
(hx : Polynomial.C x ∈ Ideal.map (Polynomial.mapRingHom (RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) 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}
[CommRing R]
{I : Ideal R}
{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}
[CommRing R]
{I : Ideal R}
{a : MvPolynomial σ R}
(ha : a ∈ Ideal.map MvPolynomial.C I)
:
(MvPolynomial.eval₂Hom (RingHom.comp MvPolynomial.C (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 (RingHom.comp (Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) MvPolynomial.C)
(_ : ∀ 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)) (MvPolynomial.X i))
⇑(Ideal.Quotient.lift (Ideal.map MvPolynomial.C I)
(MvPolynomial.eval₂Hom (RingHom.comp MvPolynomial.C (Ideal.Quotient.mk I)) MvPolynomial.X)
(_ :
∀ a ∈ Ideal.map MvPolynomial.C I,
(MvPolynomial.eval₂Hom (RingHom.comp MvPolynomial.C (Ideal.Quotient.mk I)) MvPolynomial.X) a = 0))
theorem
MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse
{R : Type u_1}
{σ : Type u_2}
[CommRing R]
(I : Ideal R)
:
Function.LeftInverse
(MvPolynomial.eval₂
(Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) MvPolynomial.C)
(_ : ∀ 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)) (MvPolynomial.X i))
⇑(Ideal.Quotient.lift (Ideal.map MvPolynomial.C I)
(MvPolynomial.eval₂Hom (RingHom.comp MvPolynomial.C (Ideal.Quotient.mk I)) MvPolynomial.X)
(_ :
∀ a ∈ Ideal.map MvPolynomial.C I,
(MvPolynomial.eval₂Hom (RingHom.comp MvPolynomial.C (Ideal.Quotient.mk I)) MvPolynomial.X) a = 0))
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.