mathlib3 documentation

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 #

Main statements #

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.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) :
noncomputable def polynomial.splitting_field_aux_aux (n : ) {K : Type u} [field K] (f : polynomial K) :
Σ (L : Type u) (inst : field L), algebra K 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
@[protected, instance]
Equations

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
@[protected, instance]
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} [comm_semiring R] [algebra R K] :
Equations
@[protected, instance]

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]
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

Any splitting field is isomorphic to splitting_field f.

Equations
@[protected, instance]