# 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
• f.factor = if H : ∃ (g : ), g f then else Polynomial.X
Instances For
theorem Polynomial.irreducible_factor {K : Type v} [] (f : ) :
Irreducible f.factor
theorem Polynomial.fact_irreducible_factor {K : Type v} [] (f : ) :
Fact (Irreducible f.factor)

See note [fact non-instances].

theorem Polynomial.factor_dvd_of_not_isUnit {K : Type v} [] {f : } (hf1 : ¬) :
f.factor f
theorem Polynomial.factor_dvd_of_degree_ne_zero {K : Type v} [] {f : } (hf : f.degree 0) :
f.factor f
theorem Polynomial.factor_dvd_of_natDegree_ne_zero {K : Type v} [] {f : } (hf : f.natDegree 0) :
f.factor f
theorem Polynomial.isCoprime_iff_aeval_ne_zero {K : Type v} [] (f : ) (g : ) :
∀ {A : Type v} [inst : ] [inst_1 : ] [inst_2 : Algebra K A] (a : A), () f 0 () g 0
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
Instances For
theorem Polynomial.X_sub_C_mul_removeFactor {K : Type v} [] (f : ) (hf : f.natDegree 0) :
(Polynomial.X - Polynomial.C (AdjoinRoot.root f.factor)) * f.removeFactor = Polynomial.map (AdjoinRoot.of f.factor) f
theorem Polynomial.natDegree_removeFactor {K : Type v} [] (f : ) :
f.removeFactor.natDegree = f.natDegree - 1
theorem Polynomial.natDegree_removeFactor' {K : Type v} [] {f : } {n : } (hfn : f.natDegree = n + 1) :
f.removeFactor.natDegree = n
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 : } :
Algebra (AdjoinRoot f.factor) (Polynomial.SplittingFieldAux n f.removeFactor)
Equations
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
instance Polynomial.SplittingFieldAux.scalar_tower' {K : Type v} [] {n : } {f : } :
IsScalarTower K (AdjoinRoot f.factor) (Polynomial.SplittingFieldAux n f.removeFactor)
Equations
• =
theorem Polynomial.SplittingFieldAux.algebraMap_succ {K : Type v} [] (n : ) (f : ) :
algebraMap K () = (algebraMap (AdjoinRoot f.factor) (Polynomial.SplittingFieldAux n f.removeFactor)).comp (AdjoinRoot.of f.factor)
theorem Polynomial.SplittingFieldAux.splits (n : ) {K : Type u} [] (f : ) (_hfn : f.natDegree = n) :
theorem Polynomial.SplittingFieldAux.adjoin_rootSet (n : ) {K : Type u} [] (f : ) (_hfn : f.natDegree = n) :
def Polynomial.SplittingField {K : Type v} [] (f : ) :

A splitting field of a polynomial.

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

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

Equations
Instances For
instance Polynomial.SplittingField.instGroupWithZero {K : Type v} [] (f : ) :
GroupWithZero f.SplittingField
Equations
• = let e := ; let __spread.0 := ; GroupWithZero.mk zpowRec
instance Polynomial.SplittingField.instField {K : Type v} [] (f : ) :
Field f.SplittingField
Equations
• One or more equations did not get rendered due to their size.
instance Polynomial.SplittingField.instCharZero {K : Type v} [] (f : ) [] :
CharZero f.SplittingField
Equations
• =
instance Polynomial.SplittingField.instCharP {K : Type v} [] (f : ) (p : ) [CharP K p] :
CharP f.SplittingField p
Equations
• =
instance Polynomial.SplittingField.instExpChar {K : Type v} [] (f : ) (p : ) [ExpChar K p] :
ExpChar f.SplittingField p
Equations
• =
instance Polynomial.IsSplittingField.splittingField {K : Type v} [] (f : ) :
Polynomial.IsSplittingField K f.SplittingField f
Equations
• =
theorem Polynomial.SplittingField.splits {K : Type v} [] (f : ) :
Polynomial.Splits (algebraMap K f.SplittingField) f
def Polynomial.SplittingField.lift {K : Type v} {L : Type w} [] [] (f : ) [Algebra K L] (hb : Polynomial.Splits () f) :
f.SplittingField →ₐ[K] L

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

Equations
Instances For
theorem Polynomial.SplittingField.adjoin_rootSet {K : Type v} [] (f : ) :
Equations
• =
instance Polynomial.IsSplittingField.instFintypeSplittingField {K : Type v} [] [] (f : ) :
Fintype f.SplittingField
Equations
Equations
• =
def Polynomial.IsSplittingField.algEquiv {K : Type v} (L : Type w) [] [] [Algebra K L] (f : ) [h : ] :
L ≃ₐ[K] f.SplittingField

Any splitting field is isomorphic to SplittingFieldAux f.

Equations
Instances For