mathlib documentation

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

Main statements #

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

Non-computably choose an irreducible factor from a polynomial.

Equations
theorem polynomial.factor_dvd_of_not_is_unit {K : Type v} [field K] {f : polynomial K} (hf1 : ¬is_unit f) :
theorem polynomial.factor_dvd_of_degree_ne_zero {K : Type v} [field K] {f : polynomial K} (hf : f.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.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) :

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
Instances for polynomial.splitting_field_aux
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.algebra (n : ) (R : Type u_1) {K : Type u} [comm_semiring R] [field K] [algebra R K] {f : polynomial K} :
Equations
@[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] [is_scalar_tower R₁ R₂ K] {f : polynomial K} :
@[protected, instance]
Equations
@[protected, instance]
noncomputable def polynomial.splitting_field.algebra' {K : Type v} [field K] (f : polynomial K) {R : Type u_1} [comm_semiring R] [algebra R 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
noncomputable def polynomial.splitting_field.lift {K : Type v} {L : Type w} [field K] [field L] (f : polynomial K) [algebra K L] (hb : polynomial.splits (algebra_map K L) f) :

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

Equations
@[protected, instance]
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)] :
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) :

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

Equations

Any splitting field is isomorphic to splitting_field f.

Equations
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) :