Documentation

Mathlib.RingTheory.AdjoinRoot

Adjoining roots of polynomials #

This file defines the commutative ring AdjoinRoot f, the ring R[X]/(f) obtained from a commutative ring R and a polynomial f : R[X]. If furthermore R is a field and f is irreducible, the field structure on AdjoinRoot f is constructed.

We suggest stating results on IsAdjoinRoot instead of AdjoinRoot to achieve higher generality, since IsAdjoinRoot works for all different constructions of R[α] including AdjoinRoot f = R[X]/(f) itself.

Main definitions and results #

The main definitions are in the AdjoinRoot namespace.

def AdjoinRoot {R : Type u} [CommRing R] (f : Polynomial R) :

Adjoin a root of a polynomial f to a commutative ring R. We define the new ring as the quotient of R[X] by the principal ideal generated by f.

Equations
Instances For
    Equations
    theorem AdjoinRoot.nontrivial {R : Type u} [CommRing R] (f : Polynomial R) [IsDomain R] (h : f.degree 0) :

    Ring homomorphism from R[x] to AdjoinRoot f sending X to the root.

    Equations
    Instances For
      theorem AdjoinRoot.induction_on {R : Type u} [CommRing R] (f : Polynomial R) {C : AdjoinRoot fProp} (x : AdjoinRoot f) (ih : ∀ (p : Polynomial R), C ((AdjoinRoot.mk f) p)) :
      C x
      def AdjoinRoot.of {R : Type u} [CommRing R] (f : Polynomial R) :

      Embedding of the original ring R into AdjoinRoot f.

      Equations
      Instances For
        @[simp]
        theorem AdjoinRoot.smul_mk {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [DistribSMul S R] [IsScalarTower S R R] (a : S) (x : Polynomial R) :
        a (AdjoinRoot.mk f) x = (AdjoinRoot.mk f) (a x)
        theorem AdjoinRoot.smul_of {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [DistribSMul S R] [IsScalarTower S R R] (a : S) (x : R) :
        a (AdjoinRoot.of f) x = (AdjoinRoot.of f) (a x)
        instance AdjoinRoot.instIsScalarTower {R : Type u} [CommRing R] (R₁ : Type u_1) (R₂ : Type u_2) [SMul R₁ R₂] [DistribSMul R₁ R] [DistribSMul R₂ R] [IsScalarTower R₁ R R] [IsScalarTower R₂ R R] [IsScalarTower R₁ R₂ R] (f : Polynomial R) :
        Equations
        • =
        instance AdjoinRoot.instSMulCommClass {R : Type u} [CommRing R] (R₁ : Type u_1) (R₂ : Type u_2) [DistribSMul R₁ R] [DistribSMul R₂ R] [IsScalarTower R₁ R R] [IsScalarTower R₂ R R] [SMulCommClass R₁ R₂ R] (f : Polynomial R) :
        Equations
        • =
        Equations
        • =
        instance AdjoinRoot.instAlgebra {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [CommSemiring S] [Algebra S R] :

        R[x]/(f) is R-algebra

        Equations

        The adjoined root.

        Equations
        Instances For
          instance AdjoinRoot.hasCoeT {R : Type u} [CommRing R] {f : Polynomial R} :
          Equations
          theorem AdjoinRoot.algHom_ext {R : Type u} {S : Type v} [CommRing R] {f : Polynomial R} [Semiring S] [Algebra R S] {g₁ : AdjoinRoot f →ₐ[R] S} {g₂ : AdjoinRoot f →ₐ[R] S} (h : g₁ (AdjoinRoot.root f) = g₂ (AdjoinRoot.root f)) :
          g₁ = g₂

          Two R-AlgHom from AdjoinRoot f to the same R-algebra are the same iff they agree on root f.

          @[simp]
          theorem AdjoinRoot.mk_eq_mk {R : Type u} [CommRing R] {f : Polynomial R} {g : Polynomial R} {h : Polynomial R} :
          (AdjoinRoot.mk f) g = (AdjoinRoot.mk f) h f g - h
          @[simp]
          theorem AdjoinRoot.mk_eq_zero {R : Type u} [CommRing R] {f : Polynomial R} {g : Polynomial R} :
          (AdjoinRoot.mk f) g = 0 f g
          @[simp]
          theorem AdjoinRoot.mk_self {R : Type u} [CommRing R] {f : Polynomial R} :
          @[simp]
          theorem AdjoinRoot.mk_C {R : Type u} [CommRing R] {f : Polynomial R} (x : R) :
          (AdjoinRoot.mk f) (Polynomial.C x) = (AdjoinRoot.of f) x
          @[simp]
          theorem AdjoinRoot.mk_X {R : Type u} [CommRing R] {f : Polynomial R} :
          (AdjoinRoot.mk f) Polynomial.X = AdjoinRoot.root f
          theorem AdjoinRoot.mk_ne_zero_of_degree_lt {R : Type u} [CommRing R] {f : Polynomial R} (hf : f.Monic) {g : Polynomial R} (h0 : g 0) (hd : g.degree < f.degree) :
          theorem AdjoinRoot.mk_ne_zero_of_natDegree_lt {R : Type u} [CommRing R] {f : Polynomial R} (hf : f.Monic) {g : Polynomial R} (h0 : g 0) (hd : g.natDegree < f.natDegree) :
          def AdjoinRoot.lift {R : Type u} {S : Type v} [CommRing R] {f : Polynomial R} [CommRing S] (i : R →+* S) (x : S) (h : Polynomial.eval₂ i x f = 0) :

          Lift a ring homomorphism i : R →+* S to AdjoinRoot f →+* S.

          Equations
          Instances For
            @[simp]
            theorem AdjoinRoot.lift_mk {R : Type u} {S : Type v} [CommRing R] {f : Polynomial R} [CommRing S] {i : R →+* S} {a : S} (h : Polynomial.eval₂ i a f = 0) (g : Polynomial R) :
            @[simp]
            theorem AdjoinRoot.lift_root {R : Type u} {S : Type v} [CommRing R] {f : Polynomial R} [CommRing S] {i : R →+* S} {a : S} (h : Polynomial.eval₂ i a f = 0) :
            @[simp]
            theorem AdjoinRoot.lift_of {R : Type u} {S : Type v} [CommRing R] {f : Polynomial R} [CommRing S] {i : R →+* S} {a : S} (h : Polynomial.eval₂ i a f = 0) {x : R} :
            (AdjoinRoot.lift i a h) ((AdjoinRoot.of f) x) = i x
            @[simp]
            theorem AdjoinRoot.lift_comp_of {R : Type u} {S : Type v} [CommRing R] {f : Polynomial R} [CommRing S] {i : R →+* S} {a : S} (h : Polynomial.eval₂ i a f = 0) :
            (AdjoinRoot.lift i a h).comp (AdjoinRoot.of f) = i
            def AdjoinRoot.liftHom {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [CommRing S] [Algebra R S] (x : S) (hfx : (Polynomial.aeval x) f = 0) :

            Produce an algebra homomorphism AdjoinRoot f →ₐ[R] S sending root f to a root of f in S.

            Equations
            Instances For
              @[simp]
              theorem AdjoinRoot.coe_liftHom {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [CommRing S] [Algebra R S] (x : S) (hfx : (Polynomial.aeval x) f = 0) :
              @[simp]
              theorem AdjoinRoot.aeval_algHom_eq_zero {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [CommRing S] [Algebra R S] (ϕ : AdjoinRoot f →ₐ[R] S) :
              @[simp]
              theorem AdjoinRoot.liftHom_eq_algHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (f : Polynomial R) (ϕ : AdjoinRoot f →ₐ[R] S) :
              @[simp]
              theorem AdjoinRoot.liftHom_mk {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [CommRing S] {a : S} [Algebra R S] (hfx : (Polynomial.aeval a) f = 0) {g : Polynomial R} :
              @[simp]
              theorem AdjoinRoot.liftHom_root {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [CommRing S] {a : S} [Algebra R S] (hfx : (Polynomial.aeval a) f = 0) :
              @[simp]
              theorem AdjoinRoot.liftHom_of {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [CommRing S] {a : S} [Algebra R S] (hfx : (Polynomial.aeval a) f = 0) {x : R} :
              (AdjoinRoot.liftHom f a hfx) ((AdjoinRoot.of f) x) = (algebraMap R S) x
              @[simp]
              theorem AdjoinRoot.root_isInv {R : Type u} [CommRing R] (r : R) :
              (AdjoinRoot.of (Polynomial.C r * Polynomial.X - 1)) r * AdjoinRoot.root (Polynomial.C r * Polynomial.X - 1) = 1
              theorem AdjoinRoot.algHom_subsingleton {R : Type u} [CommRing R] {S : Type u_1} [CommRing S] [Algebra R S] {r : R} :
              Subsingleton (AdjoinRoot (Polynomial.C r * Polynomial.X - 1) →ₐ[R] S)
              instance AdjoinRoot.span_maximal_of_irreducible {K : Type w} [Field K] {f : Polynomial K} [Fact (Irreducible f)] :
              (Ideal.span {f}).IsMaximal
              Equations
              • =
              noncomputable instance AdjoinRoot.instGroupWithZero {K : Type w} [Field K] {f : Polynomial K} [Fact (Irreducible f)] :
              Equations
              noncomputable instance AdjoinRoot.instField {K : Type w} [Field K] {f : Polynomial K} [Fact (Irreducible f)] :

              If R is a field and f is irreducible, then AdjoinRoot f is a field

              Equations
              theorem AdjoinRoot.coe_injective {K : Type w} [Field K] {f : Polynomial K} (h : f.degree 0) :
              theorem AdjoinRoot.mul_div_root_cancel {K : Type w} [Field K] (f : Polynomial K) [Fact (Irreducible f)] :
              (Polynomial.X - Polynomial.C (AdjoinRoot.root f)) * (Polynomial.map (AdjoinRoot.of f) f / (Polynomial.X - Polynomial.C (AdjoinRoot.root f))) = Polynomial.map (AdjoinRoot.of f) f
              theorem AdjoinRoot.isIntegral_root' {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
              def AdjoinRoot.modByMonicHom {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) :

              AdjoinRoot.modByMonicHom sends the equivalence class of f mod g to f %ₘ g.

              This is a well-defined right inverse to AdjoinRoot.mk, see AdjoinRoot.mk_leftInverse.

              Equations
              Instances For
                @[simp]
                theorem AdjoinRoot.modByMonicHom_mk {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) (f : Polynomial R) :
                def AdjoinRoot.powerBasisAux' {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
                Basis (Fin g.natDegree) R (AdjoinRoot g)

                The elements 1, root g, ..., root g ^ (d - 1) form a basis for AdjoinRoot g, where g is a monic polynomial of degree d.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem AdjoinRoot.powerBasisAux'_repr_symm_apply {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) (c : Fin g.natDegree →₀ R) :
                  (AdjoinRoot.powerBasisAux' hg).repr.symm c = (AdjoinRoot.mk g) (∑ i : Fin g.natDegree, (Polynomial.monomial i) (c i))
                  @[simp]
                  theorem AdjoinRoot.powerBasisAux'_repr_apply_to_fun {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) (f : AdjoinRoot g) (i : Fin g.natDegree) :
                  ((AdjoinRoot.powerBasisAux' hg).repr f) i = ((AdjoinRoot.modByMonicHom hg) f).coeff i
                  def AdjoinRoot.powerBasis' {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) :

                  The power basis 1, root g, ..., root g ^ (d - 1) for AdjoinRoot g, where g is a monic polynomial of degree d.

                  Equations
                  Instances For
                    @[simp]
                    theorem AdjoinRoot.powerBasis'_gen {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
                    @[simp]
                    theorem AdjoinRoot.powerBasis'_dim {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
                    (AdjoinRoot.powerBasis' hg).dim = g.natDegree
                    theorem AdjoinRoot.minpoly_root {K : Type w} [Field K] {f : Polynomial K} (hf : f 0) :
                    minpoly K (AdjoinRoot.root f) = f * Polynomial.C f.leadingCoeff⁻¹
                    def AdjoinRoot.powerBasisAux {K : Type w} [Field K] {f : Polynomial K} (hf : f 0) :
                    Basis (Fin f.natDegree) K (AdjoinRoot f)

                    The elements 1, root f, ..., root f ^ (d - 1) form a basis for AdjoinRoot f, where f is an irreducible polynomial over a field of degree d.

                    Equations
                    Instances For
                      def AdjoinRoot.powerBasis {K : Type w} [Field K] {f : Polynomial K} (hf : f 0) :

                      The power basis 1, root f, ..., root f ^ (d - 1) for AdjoinRoot f, where f is an irreducible polynomial over a field of degree d.

                      Equations
                      Instances For
                        @[simp]
                        theorem AdjoinRoot.powerBasis_gen {K : Type w} [Field K] {f : Polynomial K} (hf : f 0) :
                        @[simp]
                        theorem AdjoinRoot.powerBasis_dim {K : Type w} [Field K] {f : Polynomial K} (hf : f 0) :
                        (AdjoinRoot.powerBasis hf).dim = f.natDegree
                        theorem AdjoinRoot.minpoly_powerBasis_gen {K : Type w} [Field K] {f : Polynomial K} (hf : f 0) :
                        minpoly K (AdjoinRoot.powerBasis hf).gen = f * Polynomial.C f.leadingCoeff⁻¹
                        theorem AdjoinRoot.minpoly_powerBasis_gen_of_monic {K : Type w} [Field K] {f : Polynomial K} (hf : f.Monic) (hf' : optParam (f 0) ) :
                        def AdjoinRoot.Minpoly.toAdjoin (R : Type u) {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (x : S) :

                        The surjective algebra morphism R[X]/(minpoly R x) → R[x]. If R is a integrally closed domain and x is integral, this is an isomorphism, see minpoly.equivAdjoin.

                        Equations
                        Instances For
                          theorem AdjoinRoot.Minpoly.toAdjoin_apply' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {x : S} (a : AdjoinRoot (minpoly R x)) :
                          (AdjoinRoot.Minpoly.toAdjoin R x) a = (AdjoinRoot.liftHom (minpoly R x) x, ) a
                          theorem AdjoinRoot.Minpoly.toAdjoin.apply_X {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {x : S} :
                          (AdjoinRoot.Minpoly.toAdjoin R x) ((AdjoinRoot.mk (minpoly R x)) Polynomial.X) = x,
                          def AdjoinRoot.equiv' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) :

                          If S is an extension of R with power basis pb and g is a monic polynomial over R such that pb.gen has a minimal polynomial g, then S is isomorphic to AdjoinRoot g.

                          Compare PowerBasis.equivOfRoot, which would require h₂ : aeval pb.gen (minpoly R (root g)) = 0; that minimal polynomial is not guaranteed to be identical to g.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem AdjoinRoot.equiv'_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) :
                            (AdjoinRoot.equiv' g pb h₁ h₂) = (AdjoinRoot.liftHom g pb.gen h₂)
                            @[simp]
                            theorem AdjoinRoot.equiv'_symm_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) :
                            (AdjoinRoot.equiv' g pb h₁ h₂).symm = (pb.lift (AdjoinRoot.root g) h₁)
                            theorem AdjoinRoot.equiv'_toAlgHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) :
                            (AdjoinRoot.equiv' g pb h₁ h₂) = AdjoinRoot.liftHom g pb.gen h₂
                            theorem AdjoinRoot.equiv'_symm_toAlgHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) :
                            (AdjoinRoot.equiv' g pb h₁ h₂).symm = pb.lift (AdjoinRoot.root g) h₁
                            def AdjoinRoot.equiv (L : Type u_1) (F : Type u_2) [Field F] [CommRing L] [IsDomain L] [Algebra F L] (f : Polynomial F) (hf : f 0) :
                            (AdjoinRoot f →ₐ[F] L) { x : L // x f.aroots L }

                            If L is a field extension of F and f is a polynomial over F then the set of maps from F[x]/(f) into L is in bijection with the set of roots of f in L.

                            Equations
                            Instances For

                              The natural isomorphism R[α]/(I[α]) ≅ R[α]/((I[x] ⊔ (f)) / (f)) for α a root of f : R[X] and I : Ideal R.

                              See adjoin_root.quot_map_of_equiv for the isomorphism with (R/I)[X] / (f mod I).

                              Equations
                              Instances For

                                The natural isomorphism R[α]/((I[x] ⊔ (f)) / (f)) ≅ (R[x]/I[x])/((f) ⊔ I[x] / I[x]) for α a root of f : R[X] and I : Ideal R

                                Equations
                                Instances For

                                  The natural isomorphism (R/I)[x]/(f mod I) ≅ (R[x]/I*R[x])/(f mod I[x]) where f : R[X] and I : Ideal R

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

                                    The natural isomorphism R[α]/I[α] ≅ (R/I)[X]/(f mod I) for α a root of f : R[X] and I : Ideal R.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      noncomputable def PowerBasis.quotientEquivQuotientMinpolyMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pb : PowerBasis R S) (I : Ideal R) :

                                      Let α have minimal polynomial f over R and I be an ideal of R, then R[α] / (I) = (R[x] / (f)) / pS = (R/p)[x] / (f mod p).

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pb : PowerBasis R S) (I : Ideal R) :
                                        ∀ (a : Polynomial (R I) Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}), (pb.quotientEquivQuotientMinpolyMap I).symm a = (↑(AlgEquiv.ofRingEquiv )).symm ((↑(AdjoinRoot.quotEquivQuotMap (minpoly R pb.gen) I)).symm a)
                                        @[simp]
                                        theorem PowerBasis.quotientEquivQuotientMinpolyMap_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pb : PowerBasis R S) (I : Ideal R) :
                                        ∀ (a : S Ideal.map (algebraMap R S) I), (pb.quotientEquivQuotientMinpolyMap I) a = (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I (minpoly R pb.gen)) ((Ideal.quotientMap (Ideal.map (AdjoinRoot.of (minpoly R pb.gen)) I) (↑(AdjoinRoot.equiv' (minpoly R pb.gen) pb )).symm ) a)
                                        theorem PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pb : PowerBasis R S) (I : Ideal R) (g : Polynomial R) :
                                        (pb.quotientEquivQuotientMinpolyMap I) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((Polynomial.aeval pb.gen) g)) = (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})) (Polynomial.map (Ideal.Quotient.mk I) g)
                                        theorem PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pb : PowerBasis R S) (I : Ideal R) (g : Polynomial R) :
                                        (pb.quotientEquivQuotientMinpolyMap I).symm ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})) (Polynomial.map (Ideal.Quotient.mk I) g)) = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((Polynomial.aeval pb.gen) g)

                                        If L / K is an integral extension, K is a domain, L is a field, then any irreducible polynomial over L divides some monic irreducible polynomial over K.