# mathlibdocumentation

field_theory.splitting_field

# 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 : polynomial K 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 : polynomial K is called a splitting field if it is the smallest field extension of K such that f splits.

## Main definitions #

• polynomial.splits i f: A predicate on a field homomorphism i : K → L and a polynomial f saying that f is zero or all of its irreducible factors over L have degree 1.
• polynomial.splitting_field f: A fixed splitting field of the polynomial f.
• polynomial.is_splitting_field: A predicate on a field to be a splitting field of a polynomial f.

## Main statements #

• polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C: If a polynomial has as many roots as its degree, it can be written as the product of its leading coefficient with ∏ (X - a) where a ranges through its roots.
• lift_of_splits: If K and L are field extensions of a field F and for some finite subset S of K, the minimal polynomial of every x ∈ K splits as a polynomial with coefficients in L, then algebra.adjoin F S embeds into L.
• polynomial.is_splitting_field.lift: An embedding of a splitting field of the polynomial f into another field such that f splits.
• polynomial.is_splitting_field.alg_equiv: Every splitting field of a polynomial f is isomorphic to splitting_field f and thus, being a splitting field is unique up to isomorphism.
def polynomial.splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) (f : polynomial K) :
Prop

A polynomial splits iff it is zero or all of its irreducible factors have degree 1.

Equations
@[simp]
theorem polynomial.splits_zero {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) :
@[simp]
theorem polynomial.splits_C {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) (a : K) :
theorem polynomial.splits_of_degree_eq_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : f.degree = 1) :
theorem polynomial.splits_of_degree_le_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : f.degree 1) :
theorem polynomial.splits_of_nat_degree_le_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : f.nat_degree 1) :
theorem polynomial.splits_of_nat_degree_eq_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : f.nat_degree = 1) :
theorem polynomial.splits_mul {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hf : f) (hg : g) :
(f * g)
theorem polynomial.splits_of_splits_mul {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hfg : f * g 0) (h : (f * g)) :
theorem polynomial.splits_of_splits_of_dvd {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hf0 : f 0) (hf : f) (hgf : g f) :
theorem polynomial.splits_of_splits_gcd_left {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hf0 : f 0) (hf : f) :
theorem polynomial.splits_of_splits_gcd_right {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hg0 : g 0) (hg : g) :
theorem polynomial.splits_map_iff {F : Type u} {K : Type v} {L : Type w} [field K] [field L] [field F] (i : K →+* L) (j : L →+* F) {f : polynomial K} :
theorem polynomial.splits_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) :
theorem polynomial.splits_of_is_unit {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {u : polynomial K} (hu : is_unit u) :
theorem polynomial.splits_X_sub_C {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {x : K} :
theorem polynomial.splits_X {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) :
theorem polynomial.splits_id_iff_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} :
f)
theorem polynomial.splits_mul_iff {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hf : f 0) (hg : g 0) :
(f * g)
theorem polynomial.splits_prod {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {ι : Type u} {s : ι → } {t : finset ι} :
(∀ (j : ι), j t (s j)) (t.prod (λ (x : ι), s x))
theorem polynomial.splits_pow {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : f) (n : ) :
(f ^ n)
theorem polynomial.splits_X_pow {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) (n : ) :
theorem polynomial.splits_prod_iff {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {ι : Type u} {s : ι → } {t : finset ι} :
(∀ (j : ι), j ts j 0) (t.prod (λ (x : ι), s x)) ∀ (j : ι), j t (s j))
theorem polynomial.degree_eq_one_of_irreducible_of_splits {L : Type w} [field L] {p : polynomial L} (hp : irreducible p) (hp_splits : p) :
p.degree = 1
theorem polynomial.exists_root_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hs : f) (hf0 : f.degree 0) :
∃ (x : L), f = 0
theorem polynomial.roots_ne_zero_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hs : f) (hf0 : f.nat_degree 0) :
f).roots 0
noncomputable def polynomial.root_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : f) (hfd : f.degree 0) :
L

Pick a root of a polynomial that splits.

Equations
• hfd =
theorem polynomial.map_root_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : f) (hfd : f.degree 0) :
hfd) f = 0
theorem polynomial.nat_degree_eq_card_roots {K : Type v} {L : Type w} [field K] [field L] {p : polynomial K} {i : K →+* L} (hsplit : p) :
theorem polynomial.degree_eq_card_roots {K : Type v} {L : Type w} [field K] [field L] {p : polynomial K} {i : K →+* L} (p_ne_zero : p 0) (hsplit : p) :
theorem polynomial.roots_map {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : f) :
f).roots =
theorem polynomial.image_root_set {F : Type u} {K : Type v} {L : Type w} [field K] [field L] [field F] [ K] [ L] {p : polynomial F} (h : p) (f : K →ₐ[F] L) :
theorem polynomial.adjoin_root_set_eq_range {F : Type u} {K : Type v} {L : Type w} [field K] [field L] [field F] [ K] [ L] {p : polynomial F} (h : p) (f : K →ₐ[F] L) :
(p.root_set L) = f.range (p.root_set K) =
theorem polynomial.eq_prod_roots_of_splits {K : Type v} {L : Type w} [field K] [field L] {p : polynomial K} {i : K →+* L} (hsplit : p) :
= * (multiset.map (λ (a : L), p).roots).prod
theorem polynomial.eq_prod_roots_of_splits_id {K : Type v} [field K] {p : polynomial K} (hsplit : p) :
p = * (multiset.map (λ (a : K), p.roots).prod
theorem polynomial.eq_prod_roots_of_monic_of_splits_id {K : Type v} [field K] {p : polynomial K} (m : p.monic) (hsplit : p) :
p = (multiset.map (λ (a : K), p.roots).prod
theorem polynomial.eq_X_sub_C_of_splits_of_single_root {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {x : K} {h : polynomial K} (h_splits : h) (h_roots : h).roots = {i x}) :
theorem polynomial.splits_of_exists_multiset {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} {s : multiset L} (hs : = * (multiset.map (λ (a : L), s).prod) :
theorem polynomial.splits_of_splits_id {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} :
theorem polynomial.splits_iff_exists_multiset {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} :
∃ (s : multiset L), = * (multiset.map (λ (a : L), s).prod
theorem polynomial.splits_comp_of_splits {F : Type u} {K : Type v} {L : Type w} [field K] [field L] [field F] (i : K →+* L) (j : L →+* F) {f : polynomial K} (h : f) :
theorem polynomial.splits_iff_card_roots {K : Type v} [field K] {p : polynomial K} :

A polynomial splits if and only if it has as many roots as its degree.

theorem polynomial.aeval_root_derivative_of_splits {K : Type v} {L : Type w} [field K] [field L] [ L] {P : polynomial K} (hmo : P.monic) (hP : P) {r : L} (hr : r (polynomial.map L) P).roots) :
= (multiset.map (λ (a : L), r - a) ((polynomial.map L) P).roots.erase r)).prod
theorem polynomial.prod_roots_eq_coeff_zero_of_monic_of_split {K : Type v} [field K] {P : polynomial K} (hmo : P.monic) (hP : P) :
P.coeff 0 = (-1) ^ P.nat_degree * P.roots.prod

If P is a monic polynomial that splits, then coeff P 0 equals the product of the roots.

theorem polynomial.sum_roots_eq_next_coeff_of_monic_of_split {K : Type v} [field K] {P : polynomial K} (hmo : P.monic) (hP : P) :

If P is a monic polynomial that splits, then P.next_coeff equals the sum of the roots.

noncomputable def alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly (F : Type u) [field F] {R : Type u_1} [comm_ring R] [ R] (x : R) :

If p is the minimal polynomial of a over F then F[a] ≃ₐ[F] F[x]/(p)

Equations
theorem finite_dimensional.of_subalgebra_to_submodule {K : Type u_1} {V : Type u_2} [field K] [ring V] [ V] {s : V} (h : (s.to_submodule)) :

If a subalgebra is finite_dimensional as a submodule then it is finite_dimensional.

theorem lift_of_splits {F : Type u_1} {K : Type u_2} {L : Type u_3} [field F] [field K] [field L] [ K] [ L] (s : finset K) :
(∀ (x : K), x s x (minpoly F x))nonempty ( s) →ₐ[F] L)

If K and L are field extensions of F and we have s : finset K such that the minimal polynomial of each x ∈ s splits in L then algebra.adjoin F s embeds in L.

noncomputable def polynomial.factor {K : Type v} [field K] (f : polynomial K) :

Non-computably choose an irreducible factor from a polynomial.

Equations
theorem polynomial.irreducible_factor {K : Type v} [field K] (f : polynomial K) :
theorem polynomial.fact_irreducible_factor {K : Type v} [field K] (f : polynomial K) :
theorem polynomial.factor_dvd_of_not_is_unit {K : Type v} [field K] {f : polynomial K} (hf1 : ¬) :
theorem polynomial.factor_dvd_of_degree_ne_zero {K : Type v} [field K] {f : polynomial K} (hf : f.degree 0) :
theorem polynomial.factor_dvd_of_nat_degree_ne_zero {K : Type v} [field K] {f : polynomial K} (hf : f.nat_degree 0) :
noncomputable def polynomial.remove_factor {K : Type v} [field K] (f : polynomial K) :

Divide a polynomial f by X - C r where r is a root of f in a bigger field extension.

Equations
theorem polynomial.X_sub_C_mul_remove_factor {K : Type v} [field K] (f : polynomial K) (hf : f.nat_degree 0) :
theorem polynomial.nat_degree_remove_factor {K : Type v} [field K] (f : polynomial K) :
theorem polynomial.nat_degree_remove_factor' {K : Type v} [field K] {f : polynomial K} {n : } (hfn : f.nat_degree = n + 1) :
def polynomial.splitting_field_aux (n : ) {K : Type u} [field K] (f : polynomial K) :
Type u

Auxiliary construction to a splitting field of a polynomial, which removes n (arbitrarily-chosen) factors.

Uses recursion on the degree. For better definitional behaviour, structures including splitting_field_aux (such as instances) should be defined using this recursion in each field, rather than defining the whole tuple through recursion.

Equations
• = n.rec_on (λ (K : Type u) (_x : field K) (_x : , K) (λ (n : ) (ih : Π {K : Type u} [_inst_4 : field K], Type u) (K : Type u) (_x : field K) (f : , ih f.remove_factor)
Instances for polynomial.splitting_field_aux
theorem polynomial.splitting_field_aux.succ {K : Type v} [field K] (n : ) (f : polynomial K) :
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.field (n : ) {K : Type u} [field K] {f : polynomial K} :
Equations
• = n.rec_on (λ (K : Type u) (_x : field K) (_x_1 : , _x) (λ (n : ) (ih : Π {K : Type u} [_inst_4 : field K] {f : , (K : Type u) (_x : field K) (f : , ih)
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.inhabited {K : Type v} [field K] {n : } {f : polynomial K} :
Equations
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.algebra (n : ) (R : Type u_1) {K : Type u} [field K] [ K] {f : polynomial K} :
Equations
• = n.rec_on (λ (R : Type u_1) (K : Type u) (_x : (_x_1 : field K) (_x : K) (_x_1 : , _x) (λ (n : ) (ih : Π (R : Type u_1) {K : Type u} [_inst_4 : [_inst_5 : field K] [_inst_6 : K] {f : , (R : Type u_1) (K : Type u) (_x : (_x_1 : field K) (_x_2 : K) (f : , ih R)
@[protected, instance]
def polynomial.splitting_field_aux.is_scalar_tower (n : ) (R₁ : Type u_1) (R₂ : Type u_2) {K : Type u} [comm_semiring R₁] [comm_semiring R₂] [has_smul R₁ R₂] [field K] [algebra R₁ K] [algebra R₂ K] [ R₂ K] {f : polynomial K} :
R₂
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.algebra''' {K : Type v} [field K] {n : } {f : polynomial K} :
Equations
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.algebra' {K : Type v} [field K] {n : } {f : polynomial K} :
Equations
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.algebra'' {K : Type v} [field K] {n : } {f : polynomial K} :
Equations
@[protected, instance]
def polynomial.splitting_field_aux.scalar_tower' {K : Type v} [field K] {n : } {f : polynomial K} :
@[protected, instance]
def polynomial.splitting_field_aux.scalar_tower {K : Type v} [field K] {n : } {f : polynomial K} :
f)
theorem polynomial.splitting_field_aux.algebra_map_succ {K : Type v} [field K] (n : ) (f : polynomial K) :
f) =
@[protected]
theorem polynomial.splitting_field_aux.splits (n : ) {K : Type u} [field K] (f : polynomial K) (hfn : f.nat_degree = n) :
theorem polynomial.splitting_field_aux.exists_lift (n : ) {K : Type u} [field K] (f : polynomial K) (hfn : f.nat_degree = n) {L : Type u_1} [field L] (j : K →+* L) (hf : f) :
∃ (k : , k.comp = j
theorem polynomial.splitting_field_aux.adjoin_roots (n : ) {K : Type u} [field K] (f : polynomial K) (hfn : f.nat_degree = n) :
def polynomial.splitting_field {K : Type v} [field K] (f : polynomial K) :
Type v

A splitting field of a polynomial.

Equations
Instances for polynomial.splitting_field
@[protected, instance]
noncomputable def polynomial.splitting_field.field {K : Type v} [field K] (f : polynomial K) :
Equations
@[protected, instance]
noncomputable def polynomial.splitting_field.inhabited {K : Type v} [field K] (f : polynomial K) :
Equations
@[protected, instance]
noncomputable def polynomial.splitting_field.algebra' {K : Type v} [field K] (f : polynomial K) {R : Type u_1} [ K] :

This should be an instance globally, but it creates diamonds with the ℕ, ℤ, and ℚ algebras (via their smul and to_fun fields):

example :
(algebra_nat : algebra ℕ (splitting_field f)) = splitting_field.algebra' f :=
rfl  -- fails

example :
(algebra_int _ : algebra ℤ (splitting_field f)) = splitting_field.algebra' f :=
rfl  -- fails

example [char_zero K] [char_zero (splitting_field f)] :
(algebra_rat : algebra ℚ (splitting_field f)) = splitting_field.algebra' f :=
rfl  -- fails


Until we resolve these diamonds, it's more convenient to only turn this instance on with local attribute [instance] in places where the benefit of having the instance outweighs the cost.

In the meantime, the splitting_field.algebra instance below is immune to these particular diamonds since K = ℕ and K = ℤ are not possible due to the field K assumption. Diamonds in algebra ℚ (splitting_field f) instances are still possible via this instance unfortunately, but these are less common as they require suitable char_zero instances to be present.

Equations
@[protected, instance]
noncomputable def polynomial.splitting_field.algebra {K : Type v} [field K] (f : polynomial K) :
Equations
@[protected]
theorem polynomial.splitting_field.splits {K : Type v} [field K] (f : polynomial K) :
noncomputable def polynomial.splitting_field.lift {K : Type v} {L : Type w} [field K] [field L] (f : polynomial K) [ L] (hb : f) :

Embeds the splitting field into any other field that splits the polynomial.

Equations
@[class]
structure polynomial.is_splitting_field (K : Type v) (L : Type w) [field K] [field L] [ L] (f : polynomial K) :
Prop

Typeclass characterising splitting fields.

Instances of this typeclass
@[protected, instance]
@[protected, instance]
def polynomial.is_splitting_field.map {F : Type u} {K : Type v} {L : Type w} [field K] [field L] [field F] [ L] [ K] [ L] [ L] (f : polynomial F)  :
theorem polynomial.is_splitting_field.splits_iff {K : Type v} (L : Type w) [field K] [field L] [ L] (f : polynomial K)  :
theorem polynomial.is_splitting_field.mul {F : Type u} {K : Type v} (L : Type w) [field K] [field L] [field F] [ L] [ K] [ L] [ L] (f g : polynomial F) (hf : f 0) (hg : g 0) [ (polynomial.map K) g)] :
(f * g)
noncomputable def polynomial.is_splitting_field.lift {F : Type u} {K : Type v} (L : Type w) [field K] [field L] [field F] [ L] [ F] (f : polynomial K) (hf : f) :

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

Equations
theorem polynomial.is_splitting_field.finite_dimensional {K : Type v} (L : Type w) [field K] [field L] [ L] (f : polynomial K)  :
noncomputable def polynomial.is_splitting_field.alg_equiv {K : Type v} (L : Type w) [field K] [field L] [ L] (f : polynomial K)  :

Any splitting field is isomorphic to splitting_field f.

Equations
theorem polynomial.is_splitting_field.of_alg_equiv {F : Type u} {K : Type v} (L : Type w) [field K] [field L] [field F] [ L] [ F] (p : polynomial K) (f : F ≃ₐ[K] L)  :
theorem intermediate_field.splits_of_splits {K : Type v} {L : Type w} [field K] [field L] [ L] {p : polynomial K} {F : L} (h : p) (hF : ∀ (x : L), x p.root_set Lx F) :
p