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.

Equations
• = if H : ∃ (g : ), g f then else Polynomial.X
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.

Equations
• = /ₘ (Polynomial.X - Polynomial.C )
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.

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
Instances For
instance Polynomial.SplittingFieldAux.field (n : ) {K : Type u} [] (f : ) :
Equations
• = .snd.fst
instance Polynomial.instInhabitedSplittingFieldAux (n : ) {K : Type u} [] (f : ) :
Equations
• = { default := 0 }
instance Polynomial.SplittingFieldAux.algebra (n : ) {K : Type u} [] (f : ) :
Equations
• = .snd.snd
theorem Polynomial.SplittingFieldAux.succ {K : Type v} [] (n : ) (f : ) :
instance Polynomial.SplittingFieldAux.algebra''' {K : Type v} [] {n : } {f : } :
Equations
• Polynomial.SplittingFieldAux.algebra''' =
instance Polynomial.SplittingFieldAux.algebra' {K : Type v} [] {n : } {f : } :
Equations
• Polynomial.SplittingFieldAux.algebra' = Polynomial.SplittingFieldAux.algebra'''
instance Polynomial.SplittingFieldAux.algebra'' {K : Type v} [] {n : } {f : } :
Equations
• One or more equations did not get rendered due to their size.
instance Polynomial.SplittingFieldAux.scalar_tower' {K : Type v} [] {n : } {f : } :
Equations
• =
theorem Polynomial.SplittingFieldAux.splits (n : ) {K : Type u} [] (f : ) (_hfn : ) :
theorem Polynomial.SplittingFieldAux.adjoin_rootSet (n : ) {K : Type u} [] (f : ) (_hfn : ) :
Equations
• =
def Polynomial.SplittingField {K : Type v} [] (f : ) :

A splitting field of a polynomial.

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

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

Equations
Instances For
Equations
• = let e := ; let __spread.0 := ; GroupWithZero.mk zpowRec
instance Polynomial.SplittingField.instField {K : Type v} [] (f : ) :
Equations
• One or more equations did not get rendered due to their size.
instance Polynomial.SplittingField.instCharZero {K : Type v} [] (f : ) [] :
Equations
• =
instance Polynomial.SplittingField.instCharP {K : Type v} [] (f : ) (p : ) [CharP K p] :
Equations
• =
instance Polynomial.SplittingField.instExpChar {K : Type v} [] (f : ) (p : ) [ExpChar K p] :
Equations
• =
Equations
• =
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.

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

Any splitting field is isomorphic to SplittingFieldAux f.

Equations
Instances For