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

source
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' : Splits (algebraMap K L) f
- adjoin_rootSet' : Algebra.adjoin K (f.rootSet L) = ⊤

Instances

source
theorem Polynomial.IsSplittingField.splits {K : Type v} (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) [IsSplittingField K L f] :
Splits (algebraMap K L) f
source
theorem Polynomial.IsSplittingField.adjoin_rootSet {K : Type v} (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) [IsSplittingField K L f] :
Algebra.adjoin K (f.rootSet L) = ⊤
source
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) [IsSplittingField F L f] :
IsSplittingField K L (Polynomial.map (algebraMap F K) f)
source
theorem Polynomial.IsSplittingField.splits_iff {K : Type v} (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) [IsSplittingField K L f] :
Splits (RingHom.id K) f ↔ ⊤ = ⊥
source
theorem Polynomial.IsSplittingField.IsScalarTower.splits {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) [IsSplittingField K L ((mapAlg F K) f)] :
Splits (RingHom.id L) ((mapAlg F L) f)
source
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 g : Polynomial F) (hf : f ≠ 0) (hg : g ≠ 0) [IsSplittingField F K f] [IsSplittingField K L (Polynomial.map (algebraMap F K) g)] :
IsSplittingField F L (f * g)
source
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) [IsSplittingField K L f] (hf : 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

Instances For

source
theorem Polynomial.IsSplittingField.finiteDimensional {K : Type v} (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) [IsSplittingField K L f] :
FiniteDimensional K L
source
theorem Polynomial.IsSplittingField.IsScalarTower.isAlgebraic {F : Type u} {K : Type v} (L : Type w) [Field K] [Field L] [Field F] [Algebra K L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] [IsScalarTower F K L] (f : Polynomial K) [IsSplittingField K L f] :
Algebra.IsAlgebraic F L
source
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) [IsSplittingField K F p] :
IsSplittingField K L p
source
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) [IsSplittingField K L f] (i : L →ₐ[K] F) :
Algebra.adjoin K (f.rootSet F) = i.range
source
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
source
theorem IntermediateField.splits_iff_mem {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) :
Polynomial.Splits (algebraMap K ↥F) p ↔ ∀ x ∈ p.rootSet L, x ∈ F
source
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
source
theorem isSplittingField_iff_intermediateField {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {p : Polynomial K} :
Polynomial.IsSplittingField K L p ↔ Polynomial.Splits (algebraMap K L) p ∧ IntermediateField.adjoin K (p.rootSet L) = ⊤

Characterize `IsSplittingField` with `IntermediateField.adjoin` instead of `Algebra.adjoin`.

source
theorem IntermediateField.isSplittingField_iff {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {p : Polynomial K} {F : IntermediateField K L} :
Polynomial.IsSplittingField K (↥F) p ↔ Polynomial.Splits (algebraMap K ↥F) p ∧ F = adjoin K (p.rootSet L)
source
theorem IntermediateField.adjoin_rootSet_isSplittingField {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {p : Polynomial K} (hp : Polynomial.Splits (algebraMap K L) p) :
Polynomial.IsSplittingField K (↥(adjoin K (p.rootSet L))) p
source
theorem Polynomial.isSplittingField_C {K : Type v} [Field K] (a : K) :
IsSplittingField K K (C a)