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 isSolvable_gal_of_irreducible: 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] : Group.IsSolvable (Polynomial.Gal 0)

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

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

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

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

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

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

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

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

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

theorem gal_X_pow_sub_one_isSolvable {F : Type u_1} [Field F] (n : ℕ) : Group.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.map (RingHom.id F) (Polynomial.X ^ n - 1)).Splits) : Group.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.map i (Polynomial.X ^ n - Polynomial.C a)).Splits) : (Polynomial.map i (Polynomial.X ^ n - 1)).Splits

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

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

The intermediate field of elements solvable by radicals, defined as the smallest subfield which is closed under n-th roots.

Equations

• solvableByRad F E = sInf {s : IntermediateField F E | ∀ (x : E) (n : ℕ), n ≠ 0 → x ^ n ∈ s → x ∈ s}

theorem solvableByRad_le {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {s : IntermediateField F E} (H : ∀ (x : E) (n : ℕ), n ≠ 0 → x ^ n ∈ s → x ∈ s) : solvableByRad F E ≤ s

theorem solvableByRad.rad_mem {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {x : E} {n : ℕ} (hn : n ≠ 0) (hx : x ^ n ∈ solvableByRad F E) : x ∈ solvableByRad F E

theorem solvableByRad_le_algClosure (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] : solvableByRad F E ≤ algebraicClosure F E

theorem isAlgebraic_solvableByRad {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] : (solvableByRad F E).IsAlgebraic

theorem isIntegral_of_mem_solvableByRad {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {x : E} (hx : x ∈ solvableByRad F E) : IsIntegral F x

theorem solvableByRad.induction {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (motive : (x : E) → x ∈ solvableByRad F E → Prop) (mem : ∀ (x : F), motive ((algebraMap F E) x) ⋯) (add : ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x + y) ⋯) (mul : ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x * y) ⋯) (rad : ∀ (n : ℕ) (x : E) (hn : n ≠ 0) (hx : x ^ n ∈ solvableByRad F E), motive (x ^ n) hx → motive x ⋯) {x : E} (hx : x ∈ solvableByRad F E) : motive x hx

An induction principle for solvableByRad.

theorem isSolvable_gal_minpoly {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {x : E} (hx : x ∈ solvableByRad F E) : Group.IsSolvable (minpoly F x).Gal

theorem isSolvable_gal_of_irreducible {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {x : E} (hx : x ∈ solvableByRad F E) {q : Polynomial F} (q_irred : Irreducible q) (q_aeval : (Polynomial.aeval x) q = 0) : Group.IsSolvable q.Gal

Abel-Ruffini Theorem (one direction): An irreducible polynomial with a solvableByRad root has a solvable Galois group.