Documentation

Mathlib.FieldTheory.SplittingField.Construction

Splitting fields #

In this file we prove the existence and uniqueness of splitting fields.

Main definitions #

Main statements #

Implementation details #

We construct a SplittingFieldAux without worrying about whether the instances satisfy nice definitional equalities. Then the actual SplittingField is defined to be a quotient of a MvPolynomial ring by the kernel of the obvious map into SplittingFieldAux. Because the actual SplittingField will be a quotient of a MvPolynomial, it has nice instances on it.

def Polynomial.factor {K : Type v} [Field K] (f : Polynomial K) :

Non-computably choose an irreducible factor from a polynomial.

Equations
Instances For

    See note [fact non-instances].

    theorem Polynomial.factor_dvd_of_not_isUnit {K : Type v} [Field K] {f : Polynomial K} (hf1 : ¬IsUnit f) :
    f.factor f
    theorem Polynomial.factor_dvd_of_degree_ne_zero {K : Type v} [Field K] {f : Polynomial K} (hf : f.degree 0) :
    f.factor f
    theorem Polynomial.factor_dvd_of_natDegree_ne_zero {K : Type v} [Field K] {f : Polynomial K} (hf : f.natDegree 0) :
    f.factor f
    theorem Polynomial.isCoprime_iff_aeval_ne_zero {K : Type v} [Field K] (f : Polynomial K) (g : Polynomial K) :
    IsCoprime f g ∀ {A : Type v} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Algebra K A] (a : A), (Polynomial.aeval a) f 0 (Polynomial.aeval a) g 0

    Divide a polynomial f by X - C r where r is a root of f in a bigger field extension.

    Equations
    Instances For
      theorem Polynomial.X_sub_C_mul_removeFactor {K : Type v} [Field K] (f : Polynomial K) (hf : f.natDegree 0) :
      (Polynomial.X - Polynomial.C (AdjoinRoot.root f.factor)) * f.removeFactor = Polynomial.map (AdjoinRoot.of f.factor) f
      theorem Polynomial.natDegree_removeFactor {K : Type v} [Field K] (f : Polynomial K) :
      f.removeFactor.natDegree = f.natDegree - 1
      theorem Polynomial.natDegree_removeFactor' {K : Type v} [Field K] {f : Polynomial K} {n : } (hfn : f.natDegree = n + 1) :
      f.removeFactor.natDegree = n
      def Polynomial.SplittingFieldAuxAux (n : ) {K : Type u} [Field K] :
      Polynomial K(L : Type u) × (x : Field L) × Algebra K L

      Auxiliary construction to a splitting field of a polynomial, which removes n (arbitrarily-chosen) factors.

      It constructs the type, proves that is a field and algebra over the base field.

      Uses recursion on the degree.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def Polynomial.SplittingFieldAux (n : ) {K : Type u} [Field K] (f : Polynomial K) :

        Auxiliary construction to a splitting field of a polynomial, which removes n (arbitrarily-chosen) factors. It is the type constructed in SplittingFieldAuxAux.

        Equations
        Instances For
          instance Polynomial.SplittingFieldAux.algebra''' {K : Type v} [Field K] {n : } {f : Polynomial K} :
          Algebra (AdjoinRoot f.factor) (Polynomial.SplittingFieldAux n f.removeFactor)
          Equations
          Equations
          • Polynomial.SplittingFieldAux.algebra' = Polynomial.SplittingFieldAux.algebra'''
          Equations
          Equations
          • =
          theorem Polynomial.SplittingFieldAux.adjoin_rootSet (n : ) {K : Type u} [Field K] (f : Polynomial K) (_hfn : f.natDegree = n) :

          A splitting field of a polynomial.

          Equations
          Instances For
            instance Polynomial.SplittingField.inhabited {K : Type v} [Field K] (f : Polynomial K) :
            Inhabited f.SplittingField
            Equations
            instance Polynomial.SplittingField.isScalarTower {K : Type v} [Field K] (f : Polynomial K) {R : Type u_1} [CommSemiring R] [Algebra R K] :
            IsScalarTower R K f.SplittingField
            Equations
            • =

            The algebra equivalence with SplittingFieldAux, which we will use to construct the field structure.

            Equations
            Instances For
              instance Polynomial.SplittingField.instGroupWithZero {K : Type v} [Field K] (f : Polynomial K) :
              GroupWithZero f.SplittingField
              Equations
              instance Polynomial.SplittingField.instField {K : Type v} [Field K] (f : Polynomial K) :
              Field f.SplittingField
              Equations
              instance Polynomial.SplittingField.instCharZero {K : Type v} [Field K] (f : Polynomial K) [CharZero K] :
              CharZero f.SplittingField
              Equations
              • =
              instance Polynomial.SplittingField.instCharP {K : Type v} [Field K] (f : Polynomial K) (p : ) [CharP K p] :
              CharP f.SplittingField p
              Equations
              • =
              instance Polynomial.SplittingField.instExpChar {K : Type v} [Field K] (f : Polynomial K) (p : ) [ExpChar K p] :
              ExpChar f.SplittingField p
              Equations
              • =
              Equations
              • =
              theorem Polynomial.SplittingField.splits {K : Type v} [Field K] (f : Polynomial K) :
              Polynomial.Splits (algebraMap K f.SplittingField) f
              def Polynomial.SplittingField.lift {K : Type v} {L : Type w} [Field K] [Field L] (f : Polynomial K) [Algebra K L] (hb : Polynomial.Splits (algebraMap K L) f) :
              f.SplittingField →ₐ[K] L

              Embeds the splitting field into any other field that splits the polynomial.

              Equations
              Instances For
                theorem Polynomial.SplittingField.adjoin_rootSet {K : Type v} [Field K] (f : Polynomial K) :
                Algebra.adjoin K (f.rootSet f.SplittingField) =
                def Polynomial.IsSplittingField.algEquiv {K : Type v} (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) [h : Polynomial.IsSplittingField K L f] :
                L ≃ₐ[K] f.SplittingField

                Any splitting field is isomorphic to SplittingFieldAux f.

                Equations
                Instances For