# Documentation

Mathlib.FieldTheory.SplittingField.Construction

# Splitting fields #

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

## Main definitions #

• Polynomial.SplittingField f: A fixed splitting field of the polynomial f.

## Main statements #

• Polynomial.IsSplittingField.algEquiv: Every splitting field of a polynomial f is isomorphic to SplittingField f and thus, being a splitting field is unique up to isomorphism.

## Implementation details #

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

def Polynomial.factor {K : Type v} [] (f : ) :

Non-computably choose an irreducible factor from a polynomial.

Instances For
theorem Polynomial.irreducible_factor {K : Type v} [] (f : ) :
theorem Polynomial.fact_irreducible_factor {K : Type v} [] (f : ) :

See note [fact non-instances].

theorem Polynomial.factor_dvd_of_not_isUnit {K : Type v} [] {f : } (hf1 : ¬) :
theorem Polynomial.factor_dvd_of_degree_ne_zero {K : Type v} [] {f : } (hf : ) :
theorem Polynomial.factor_dvd_of_natDegree_ne_zero {K : Type v} [] {f : } (hf : ) :
def Polynomial.removeFactor {K : Type v} [] (f : ) :

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

Instances For
theorem Polynomial.X_sub_C_mul_removeFactor {K : Type v} [] (f : ) (hf : ) :
(Polynomial.X - Polynomial.C ()) * =
theorem Polynomial.natDegree_removeFactor {K : Type v} [] (f : ) :
theorem Polynomial.natDegree_removeFactor' {K : Type v} [] {f : } {n : } (hfn : = n + 1) :
def Polynomial.SplittingFieldAuxAux (n : ) {K : Type u} [] :
(L : Type u) × (x : ) × 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.

Instances For
def Polynomial.SplittingFieldAux (n : ) {K : Type u} [] (f : ) :

Auxiliary construction to a splitting field of a polynomial, which removes n (arbitrarily-chosen) factors. It is the type constructed in SplittingFieldAuxAux.

Instances For
instance Polynomial.SplittingFieldAux.field (n : ) {K : Type u} [] (f : ) :
instance Polynomial.instInhabitedSplittingFieldAux (n : ) {K : Type u} [] (f : ) :
instance Polynomial.SplittingFieldAux.algebra (n : ) {K : Type u} [] (f : ) :
theorem Polynomial.SplittingFieldAux.succ {K : Type v} [] (n : ) (f : ) :
instance Polynomial.SplittingFieldAux.algebra''' {K : Type v} [] {n : } {f : } :
instance Polynomial.SplittingFieldAux.algebra' {K : Type v} [] {n : } {f : } :
instance Polynomial.SplittingFieldAux.algebra'' {K : Type v} [] {n : } {f : } :
instance Polynomial.SplittingFieldAux.scalar_tower' {K : Type v} [] {n : } {f : } :
theorem Polynomial.SplittingFieldAux.splits (n : ) {K : Type u} [] (f : ) (_hfn : ) :
theorem Polynomial.SplittingFieldAux.adjoin_rootSet (n : ) {K : Type u} [] (f : ) (_hfn : ) :
def Polynomial.SplittingField {K : Type v} [] (f : ) :

A splitting field of a polynomial.

Instances For
instance Polynomial.SplittingField.commRing {K : Type v} [] (f : ) :
instance Polynomial.SplittingField.inhabited {K : Type v} [] (f : ) :
instance Polynomial.SplittingField.instSMulSplittingField {K : Type v} [] (f : ) {S : Type u_1} [] [] :
instance Polynomial.SplittingField.algebra {K : Type v} [] (f : ) :
instance Polynomial.SplittingField.algebra' {K : Type v} [] (f : ) {R : Type u_1} [] [Algebra R K] :
instance Polynomial.SplittingField.isScalarTower {K : Type v} [] (f : ) {R : Type u_1} [] [Algebra R K] :

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

Instances For
instance Polynomial.SplittingField.instCharZero {K : Type v} [] (f : ) [] :
instance Polynomial.SplittingField.instCharP {K : Type v} [] (f : ) (p : ) [CharP K p] :
theorem Polynomial.SplittingField.splits {K : Type v} [] (f : ) :
def Polynomial.SplittingField.lift {K : Type v} {L : Type w} [] [] (f : ) [Algebra K L] (hb : Polynomial.Splits () f) :

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

Instances For
def Polynomial.IsSplittingField.algEquiv {K : Type v} (L : Type w) [] [] [Algebra K L] (f : ) [] :

Any splitting field is isomorphic to SplittingFieldAux f.

Instances For