Documentation

Mathlib.RingTheory.Polynomial.Quotient

Quotients of polynomial rings #

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

            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
              theorem Ideal.isDomain_map_C_quotient {R : Type u_1} [CommRing R] {P : Ideal R} :
              Ideal.IsPrime PIsDomain (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 : { x // 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 : 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)) (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 : MvPolynomial σ R), 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 : 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)) (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 : MvPolynomial σ R), 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.
              Instances For