# mathlib3documentation

field_theory.splitting_field.construction

# Splitting fields #

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

In this file we prove the existence and uniqueness of splitting fields.

## Main definitions #

• polynomial.splitting_field f: A fixed splitting field of the polynomial f.

## Main statements #

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

## Implementation details #

We construct a splitting_field_aux without worrying about whether the instances satisfy nice definitional equalities. Then the actual splitting_field is defined to be a quotient of a mv_polynomial ring by the kernel of the obvious map into splitting_field_aux. Because the actual splitting_field will be a quotient of a mv_polynomial, it has nice instances on it.

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.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) :
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} {n : } (hfn : f.nat_degree = n + 1) :
noncomputable def polynomial.splitting_field_aux_aux (n : ) {K : Type u} [field K] (f : polynomial K) :
Σ (L : Type u) (inst : field L), L

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

It constructs the type, proves that is a field and algebra over the base field.

Uses recursion on the degree.

Equations
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. It is the type constructed in splitting_field_aux_aux.

Equations
Instances for polynomial.splitting_field_aux
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.field (n : ) {K : Type u} [field K] (f : polynomial K) :
Equations
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.inhabited (n : ) {K : Type u} [field K] (f : polynomial K) :
Equations
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.algebra (n : ) {K : Type u} [field K] (f : polynomial K) :
Equations
theorem polynomial.splitting_field_aux.succ {K : Type v} [field K] (n : ) (f : polynomial K) :
@[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]
@[protected]
theorem polynomial.splitting_field_aux.splits (n : ) {K : Type u} [field K] (f : polynomial K) (hfn : f.nat_degree = n) :
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.of_mv_polynomial {K : Type v} [field K] (f : polynomial K) :

The natural map from mv_polynomial (f.root_set (splitting_field_aux f.nat_degree f)) to splitting_field_aux f.nat_degree f sendind a variable to the corresponding root.

Equations

The algebra isomorphism between the quotient of mv_polynomial (f.root_set (splitting_field_aux f.nat_degree f)) K by the kernel of of_mv_polynomial f and splitting_field_aux f.nat_degree f. It is used to transport all the algebraic structures from the latter to f.splitting_field, that is defined as the former.

Equations
def polynomial.splitting_field {K : Type v} [field K] (f : polynomial K) :

A splitting field of a polynomial.

Equations
Instances for polynomial.splitting_field
@[protected, instance]
noncomputable def polynomial.splitting_field.comm_ring {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.has_smul {K : Type v} [field K] (f : polynomial K) {S : Type u_1} [ K] [ K] :
Equations
@[protected, instance]
noncomputable def polynomial.splitting_field.algebra {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] :
Equations
@[protected, instance]
def polynomial.splitting_field.is_scalar_tower {K : Type v} [field K] (f : polynomial K) {R : Type u_1} [ K] :

The algebra equivalence with splitting_field_aux, which we will use to construct the field structure.

Equations
@[protected, instance]
noncomputable def polynomial.splitting_field.field {K : Type v} [field K] (f : polynomial K) :
Equations
@[protected, instance]
@[protected, instance]
@[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
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
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
@[protected, instance]