The Abel-Ruffini Theorem

This file proves one direction of the Abel-Ruffini theorem, namely that if an element is solvable by radicals, then its minimal polynomial has solvable Galois group.

Main definitions

• solvableByRad F E : the intermediate field of solvable-by-radicals elements

Main results

• the Abel-Ruffini Theorem solvableByRad.isSolvable' : An irreducible polynomial with a root that is solvable by radicals has a solvable Galois group.

theorem gal_zero_isSolvable {F : Type u_1} [Field F] : IsSolvable (Polynomial.Gal 0)

theorem gal_one_isSolvable {F : Type u_1} [Field F] : IsSolvable (Polynomial.Gal 1)

theorem gal_C_isSolvable {F : Type u_1} [Field F] (x : F) : IsSolvable (Polynomial.C x).Gal

theorem gal_X_isSolvable {F : Type u_1} [Field F] : IsSolvable Polynomial.X.Gal

theorem gal_X_sub_C_isSolvable {F : Type u_1} [Field F] (x : F) : IsSolvable (Polynomial.X - Polynomial.C x).Gal

theorem gal_X_pow_isSolvable {F : Type u_1} [Field F] (n : ℕ) : IsSolvable (Polynomial.X ^ n).Gal

theorem gal_mul_isSolvable {F : Type u_1} [Field F] {p q : Polynomial F} : IsSolvable p.Gal → IsSolvable q.Gal → IsSolvable (p * q).Gal

theorem gal_prod_isSolvable {F : Type u_1} [Field F] {s : Multiset (Polynomial F)} (hs : ∀ p ∈ s, IsSolvable p.Gal) : IsSolvable s.prod.Gal

theorem gal_isSolvable_of_splits {F : Type u_1} [Field F] {p q : Polynomial F} : Fact (Polynomial.Splits (algebraMap F q.SplittingField) p) → ∀ (hq : IsSolvable q.Gal), IsSolvable p.Gal

theorem gal_isSolvable_tower {F : Type u_1} [Field F] (p q : Polynomial F) (hpq : Polynomial.Splits (algebraMap F q.SplittingField) p) (hp : IsSolvable p.Gal) (hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal) : IsSolvable q.Gal

theorem gal_X_pow_sub_one_isSolvable {F : Type u_1} [Field F] (n : ℕ) : IsSolvable (Polynomial.X ^ n - 1).Gal

theorem gal_X_pow_sub_C_isSolvable_aux {F : Type u_1} [Field F] (n : ℕ) (a : F) (h : Polynomial.Splits (RingHom.id F) (Polynomial.X ^ n - 1)) : IsSolvable (Polynomial.X ^ n - Polynomial.C a).Gal

theorem splits_X_pow_sub_one_of_X_pow_sub_C {F : Type u_3} [Field F] {E : Type u_4} [Field E] (i : F →+* E) (n : ℕ) {a : F} (ha : a ≠ 0) (h : Polynomial.Splits i (Polynomial.X ^ n - Polynomial.C a)) : Polynomial.Splits i (Polynomial.X ^ n - 1)

theorem gal_X_pow_sub_C_isSolvable {F : Type u_1} [Field F] (n : ℕ) (x : F) : IsSolvable (Polynomial.X ^ n - Polynomial.C x).Gal

inductive IsSolvableByRad (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] : E → Prop

Inductive definition of solvable by radicals

• base: ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : F), IsSolvableByRad F ((algebraMap F E) α)
• add: ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α β : E), IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α + β)
• neg: ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E), IsSolvableByRad F α → IsSolvableByRad F (-α)
• mul: ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α β : E), IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α * β)
• inv: ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E), IsSolvableByRad F α → IsSolvableByRad F α⁻¹
• rad: ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E) (n : ℕ), n ≠ 0 → IsSolvableByRad F (α ^ n) → IsSolvableByRad F α

def solvableByRad (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] : IntermediateField F E

The intermediate field of solvable-by-radicals elements

Equations

• solvableByRad F E = { carrier := IsSolvableByRad F, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯, inv_mem' := ⋯ }

theorem solvableByRad.induction {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (P : ↥(solvableByRad F E) → Prop) (base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)) (add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)) (neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)) (mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)) (inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹) (rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α) (α : ↥(solvableByRad F E)) : P α

theorem solvableByRad.isIntegral {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : ↥(solvableByRad F E)) : IsIntegral F α

def solvableByRad.P {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : ↥(solvableByRad F E)) : Prop

The statement to be proved inductively

Equations

• solvableByRad.P α = IsSolvable (minpoly F α).Gal

theorem solvableByRad.induction3 {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : ↥(solvableByRad F E)} {n : ℕ} (hn : n ≠ 0) (hα : solvableByRad.P (α ^ n)) : solvableByRad.P α

An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.

theorem solvableByRad.induction2 {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α β γ : ↥(solvableByRad F E)} (hγ : γ ∈ F⟮α, β⟯) (hα : solvableByRad.P α) (hβ : solvableByRad.P β) : solvableByRad.P γ

An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.

theorem solvableByRad.induction1 {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α β : ↥(solvableByRad F E)} (hβ : β ∈ F⟮α⟯) (hα : solvableByRad.P α) : solvableByRad.P β

An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.

theorem solvableByRad.isSolvable {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : ↥(solvableByRad F E)) : IsSolvable (minpoly F α).Gal

theorem solvableByRad.isSolvable' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {q : Polynomial F} (q_irred : Irreducible q) (q_aeval : (Polynomial.aeval α) q = 0) (hα : IsSolvableByRad F α) : IsSolvable q.Gal

Abel-Ruffini Theorem (one direction): An irreducible polynomial with an IsSolvableByRad root has solvable Galois group