Splitting fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.is_splitting_field: A predicate on a field to be a splitting field of a polynomial f.

Main statements #

polynomial.is_splitting_field.lift: An embedding of a splitting field of the polynomial f into another field such that f splits.

source

@[class]

structure polynomial.is_splitting_field (K : Type v) (L : Type w) [field K] [field L] [algebra K L] (f : polynomial K) :

Prop

splits : polynomial.splits (algebra_map K L) f
adjoin_root_set : algebra.adjoin K (f.root_set L) = ⊤

Typeclass characterising splitting fields.

Instances of this typeclass

source

@[protected, instance]

def polynomial.is_splitting_field.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] [is_scalar_tower F K L] (f : polynomial F) [polynomial.is_splitting_field F L f] :

polynomial.is_splitting_field K L (polynomial.map (algebra_map F K) f)

source

theorem polynomial.is_splitting_field.splits_iff {K : Type v} (L : Type w) [field K] [field L] [algebra K L] (f : polynomial K) [polynomial.is_splitting_field K L f] :

polynomial.splits (ring_hom.id K) f ↔ ⊤ = ⊥

source

theorem polynomial.is_splitting_field.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] [is_scalar_tower F K L] (f g : polynomial F) (hf : f ≠ 0) (hg : g ≠ 0) [polynomial.is_splitting_field F K f] [polynomial.is_splitting_field K L (polynomial.map (algebra_map F K) g)] :

polynomial.is_splitting_field F L (f * g)

source

noncomputable def polynomial.is_splitting_field.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.is_splitting_field K L f] (hf : polynomial.splits (algebra_map K F) f) :

L →ₐ[K] F

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

Equations

polynomial.is_splitting_field.lift L f hf = dite (f = 0) (λ (hf0 : f = 0), (algebra.of_id K F).comp (↑(algebra.bot_equiv K L).comp (_.mpr algebra.to_top))) (λ (hf0 : ¬f = 0), (_.mpr (classical.choice _)).comp algebra.to_top)

source

theorem polynomial.is_splitting_field.finite_dimensional {K : Type v} (L : Type w) [field K] [field L] [algebra K L] (f : polynomial K) [polynomial.is_splitting_field K L f] :

finite_dimensional K L

source

theorem polynomial.is_splitting_field.of_alg_equiv {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.is_splitting_field K F p] :

polynomial.is_splitting_field K L p

source

theorem intermediate_field.splits_of_splits {K : Type v} {L : Type w} [field K] [field L] [algebra K L] {p : polynomial K} {F : intermediate_field K L} (h : polynomial.splits (algebra_map K L) p) (hF : ∀ (x : L), x ∈ p.root_set L → x ∈ F) :

polynomial.splits (algebra_map K ↥F) p