Splitting fields #

This file introduces the notion of a splitting field of a polynomial and provides an embedding from a splitting field to any field that splits the polynomial. A polynomial f : K[X] splits over a field extension L of K if it is zero or all of its irreducible factors over L have degree 1. A field extension of K of a polynomial f : K[X] is called a splitting field if it is the smallest field extension of K such that f splits.

Main definitions #

Main statements #

class Polynomial.IsSplittingField (K : Type v) (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) :

Typeclass characterising splitting fields.

    theorem Polynomial.IsSplittingField.mul {F : Type u} {K : Type v} (L : Type w) [Field K] [Field L] [Field F] [Algebra K L] [Algebra F K] [Algebra F L] [IsScalarTower F K L] (f : Polynomial F) (g : Polynomial F) (hf : f 0) (hg : g 0) [Polynomial.IsSplittingField F K f] [Polynomial.IsSplittingField K L ( (algebraMap F K) g)] :
    def Polynomial.IsSplittingField.lift {F : Type u} {K : Type v} (L : Type w) [Field K] [Field L] [Field F] [Algebra K L] [Algebra K F] (f : Polynomial K) [Polynomial.IsSplittingField K L f] (hf : Polynomial.Splits (algebraMap K F) f) :

    Splitting field of f embeds into any field that splits f.

    Instances For
      theorem IntermediateField.splits_of_splits {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {p : Polynomial K} {F : IntermediateField K L} (h : Polynomial.Splits (algebraMap K L) p) (hF : ∀ (x : L), x Polynomial.rootSet p Lx F) :
      Polynomial.Splits (algebraMap K { x // x F }) p