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

• Polynomial.IsSplittingField: A predicate on a field to be a splitting field of a polynomial f.

## Main statements #

• Polynomial.IsSplittingField.lift: An embedding of a splitting field of the polynomial f into another field such that f splits.
class Polynomial.IsSplittingField (K : Type v) (L : Type w) [] [] [Algebra K L] (f : ) :

Typeclass characterising splitting fields.

Instances
theorem Polynomial.IsSplittingField.splits' {K : Type v} {L : Type w} [] [] [Algebra K L] {f : } [self : ] :
theorem Polynomial.IsSplittingField.adjoin_rootSet' {K : Type v} {L : Type w} [] [] [Algebra K L] {f : } [self : ] :
theorem Polynomial.IsSplittingField.splits {K : Type v} (L : Type w) [] [] [Algebra K L] (f : ) [] :
theorem Polynomial.IsSplittingField.adjoin_rootSet {K : Type v} (L : Type w) [] [] [Algebra K L] (f : ) [] :
instance Polynomial.IsSplittingField.map {F : Type u} {K : Type v} (L : Type w) [] [] [] [Algebra K L] [Algebra F K] [Algebra F L] [] (f : ) [] :
Equations
• =
theorem Polynomial.IsSplittingField.splits_iff {K : Type v} (L : Type w) [] [] [Algebra K L] (f : ) [] :
theorem Polynomial.IsSplittingField.mul {F : Type u} {K : Type v} (L : Type w) [] [] [] [Algebra K L] [Algebra F K] [Algebra F L] [] (f : ) (g : ) (hf : f 0) (hg : g 0) [] [Polynomial.IsSplittingField K L (Polynomial.map () g)] :
def Polynomial.IsSplittingField.lift {F : Type u} {K : Type v} (L : Type w) [] [] [] [Algebra K L] [Algebra K F] (f : ) [] (hf : Polynomial.Splits () f) :

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

Equations
• = if hf0 : f = 0 then ().comp ((()).comp (.mpr Algebra.toTop)) else (.mpr ()).comp Algebra.toTop
Instances For
theorem Polynomial.IsSplittingField.finiteDimensional {K : Type v} (L : Type w) [] [] [Algebra K L] (f : ) [] :
theorem Polynomial.IsSplittingField.of_algEquiv {F : Type u} {K : Type v} (L : Type w) [] [] [] [Algebra K L] [Algebra K F] (p : ) (f : F ≃ₐ[K] L) [] :
theorem Polynomial.IsSplittingField.adjoin_rootSet_eq_range {F : Type u} {K : Type v} (L : Type w) [] [] [] [Algebra K L] [Algebra K F] (f : ) [] (i : L →ₐ[K] F) :
Algebra.adjoin K (f.rootSet F) = i.range
theorem IntermediateField.splits_of_splits {K : Type v} {L : Type w} [] [] [Algebra K L] {p : } {F : } (h : Polynomial.Splits () p) (hF : xp.rootSet L, x F) :
theorem IsIntegral.mem_intermediateField_of_minpoly_splits {K : Type v} {L : Type w} [] [] [Algebra K L] {x : L} (int : ) {F : } (h : Polynomial.Splits (algebraMap K F) (minpoly K x)) :
x F