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.

Instances For

    See note [fact non-instances].

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

    Instances For
      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.

      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.

        Instances For

          A splitting field of a polynomial.

          Instances For

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

            Instances For

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

              Instances For

                Any splitting field is isomorphic to SplittingFieldAux f.

                Instances For