# 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 : 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.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.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.
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) :
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
theorem polynomial.splitting_field_aux.succ {K : Type v} [field K] (n : ) (f : polynomial K) :

### Instances on splitting_field_aux#

In order to avoid diamond issues, we have to be careful to define each data field of algebraic instances on splitting_field_aux by recursion, rather than defining the whole structure by recursion at once.

The important detail is that the smul instances can be lifted before we create the algebraic instances; if we do not do this, this creates a mutual dependence on both on each other, and it is impossible to untangle this mess. In order to do this, we need that these smul instances are distributive in the sense of distrib_smul, which is weak enough to be guaranteed at this stage. This is sufficient to lift an action to adjoin_root f (remember that this is a quotient, so these conditions are equivalent to well-definedness), which is all we need.

@[protected]
noncomputable def polynomial.splitting_field_aux.zero (n : ) {K : Type u} [field K] {f : polynomial K} :

Splitting fields have a zero.

Equations
@[protected]
noncomputable def polynomial.splitting_field_aux.add (n : ) {K : Type u} [field K] {f : polynomial K} :

Equations
@[protected]
noncomputable def polynomial.splitting_field_aux.smul (n : ) (α : Type u_1) {K : Type u} [field K] [ K] [ K] {f : polynomial K} :

Splitting fields inherit scalar multiplication.

Equations
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.has_smul (α : Type u_1) (n : ) {K : Type u} [field K] [ K] [ 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} [has_smul R₁ R₂] [field K] [ K] [ K] [ K K] [ K K] [ R₂ K] {f : polynomial K} :
R₂
@[protected]
noncomputable def polynomial.splitting_field_aux.neg (n : ) {K : Type u} [field K] {f : polynomial K} :

Splitting fields have a negation.

Equations
@[protected]
noncomputable def polynomial.splitting_field_aux.sub (n : ) {K : Type u} [field K] {f : polynomial K} :

Splitting fields have subtraction.

Equations
@[protected]
noncomputable def polynomial.splitting_field_aux.one (n : ) {K : Type u} [field K] {f : polynomial K} :

Splitting fields have a one.

Equations
@[protected]
noncomputable def polynomial.splitting_field_aux.mul (n : ) {K : Type u} [field K] {f : polynomial K} :

Splitting fields have a multiplication.

Equations
@[protected]
noncomputable def polynomial.splitting_field_aux.npow (n : ) {K : Type u} [field K] {f : polynomial K} :

Splitting fields have a power operation.

Equations
@[protected]
noncomputable def polynomial.splitting_field_aux.mk (n : ) {K : Type u} [field K] {f : polynomial K} :

Splitting fields have an injection from the base field.

Equations
@[protected]
noncomputable def polynomial.splitting_field_aux.inv (n : ) {K : Type u} [field K] {f : polynomial K} :

Splitting fields have an inverse.

Equations
@[protected]
noncomputable def polynomial.splitting_field_aux.div (n : ) {K : Type u} [field K] {f : polynomial K} :

Splitting fields have a division.

Equations
@[protected]
noncomputable def polynomial.splitting_field_aux.zpow (n : ) {K : Type u} [field K] {f : polynomial K} :

Splitting fields have powers by integers.

Equations
@[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 {K : Type v} [field K] {n : } {f : polynomial K} :
Equations
@[protected]
noncomputable def polynomial.splitting_field_aux.mk_hom (n : ) {K : Type u} [field K] {f : polynomial K} :

The injection from the base field as a ring homomorphism.

Equations
@[simp]
theorem polynomial.splitting_field_aux.mk_hom_apply (n : ) {K : Type u} [field K] {f : polynomial K} (ᾰ : K) :
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.algebra (n : ) (R : Type u_1) {K : Type u} [field K] [ K] {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]
noncomputable def polynomial.splitting_field_aux.algebra'' {K : Type v} [field K] {n : } {f : polynomial K} :
Equations
@[protected, instance]
@[protected, instance]
@[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
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.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] :
Equations
@[protected, instance]
noncomputable def polynomial.splitting_field.algebra {K : Type v} [field K] (f : polynomial K) :
Equations
@[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
@[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)  :
@[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
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 L x F) :
p