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) [Field K] [Field L] [Algebra K L] (f : Polynomial K) : Prop

Typeclass characterising splitting fields.

• splits' : Polynomial.Splits (algebraMap K L) f
• adjoin_rootSet' : Algebra.adjoin K (f.rootSet L) = ⊤

theorem Polynomial.IsSplittingField.splits' {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {f : Polynomial K} [self : Polynomial.IsSplittingField K L f] : Polynomial.Splits (algebraMap K L) f

theorem Polynomial.IsSplittingField.adjoin_rootSet' {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {f : Polynomial K} [self : Polynomial.IsSplittingField K L f] : Algebra.adjoin K (f.rootSet L) = ⊤

theorem Polynomial.IsSplittingField.splits {K : Type v} (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) [Polynomial.IsSplittingField K L f] : Polynomial.Splits (algebraMap K L) f

theorem Polynomial.IsSplittingField.adjoin_rootSet {K : Type v} (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) [Polynomial.IsSplittingField K L f] : Algebra.adjoin K (f.rootSet L) = ⊤

instance Polynomial.IsSplittingField.map {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) [Polynomial.IsSplittingField F L f] : Polynomial.IsSplittingField K L (Polynomial.map (algebraMap F K) f)

Equations

• ⋯ = ⋯

theorem Polynomial.IsSplittingField.splits_iff {K : Type v} (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) [Polynomial.IsSplittingField K L f] : Polynomial.Splits (RingHom.id K) f ↔ ⊤ = ⊥

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 (Polynomial.map (algebraMap F K) g)] : Polynomial.IsSplittingField F L (f * 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) : L →ₐ[K] F

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

Equations

• Polynomial.IsSplittingField.lift L f hf = if hf0 : f = 0 then (Algebra.ofId K F).comp ((↑(Algebra.botEquiv K L)).comp (⋯.mpr Algebra.toTop)) else (⋯.mpr (Classical.choice ⋯)).comp Algebra.toTop

theorem Polynomial.IsSplittingField.finiteDimensional {K : Type v} (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) [Polynomial.IsSplittingField K L f] : FiniteDimensional K L

theorem Polynomial.IsSplittingField.of_algEquiv {F : Type u} {K : Type v} (L : Type w) [Field K] [Field L] [Field F] [Algebra K L] [Algebra K F] (p : Polynomial K) (f : F ≃ₐ[K] L) [Polynomial.IsSplittingField K F p] : Polynomial.IsSplittingField K L p

theorem Polynomial.IsSplittingField.adjoin_rootSet_eq_range {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] (i : L →ₐ[K] F) : Algebra.adjoin K (f.rootSet F) = i.range

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 ∈ p.rootSet L, x ∈ F) : Polynomial.Splits (algebraMap K ↥F) p

theorem IsIntegral.mem_intermediateField_of_minpoly_splits {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {x : L} (int : IsIntegral K x) {F : IntermediateField K L} (h : Polynomial.Splits (algebraMap K ↥F) (minpoly K x)) : x ∈ F