Solvability by radicals

TheoremAbel–Ruffini, contrapositive form#✓fully proved

Let \(F\) be a field, let \(E\) be a field extension of \(F\), and let \(n \ge 5\). If \(p \in F[X]\) is irreducible and the Galois group of \(p\) over \(F\) is isomorphic to the symmetric group \(S_n\), then no root of \(p\) in \(E\) is solvable by radicals over \(F\).

theorem not_solvableByRad_of_gal_iso_perm {F E : Type*} [Field F] [Field E]
    [Algebra F E] {n : ℕ} (hn : 5 ≤ n) {p : Polynomial F} (hp : Irreducible p)
    (hiso : p.Gal ≃* Equiv.Perm (Fin n)) {x : E} (hpx : Polynomial.aeval x p = 0) :
    x ∉ solvableByRad F E

Used by 1

Used byAbel–Ruffini for \(S_5\)

TheoremAbel–Ruffini for \(S_5\)#✓fully proved

Let \(F\) be a field and let \(E\) be a field extension of \(F\). If \(p \in F[X]\) is irreducible and the Galois group of \(p\) over \(F\) is isomorphic to the symmetric group \(S_5\), then no root of \(p\) in \(E\) is solvable by radicals over \(F\).

theorem not_solvableByRad_of_gal_iso_S5 {F E : Type*} [Field F] [Field E]
    [Algebra F E] {p : Polynomial F} (hp : Irreducible p)
    (hiso : p.Gal ≃* Equiv.Perm (Fin 5)) {x : E} (hpx : Polynomial.aeval x p = 0) :
    x ∉ solvableByRad F E

Uses 1

Proof usesAbel–Ruffini, contrapositive form

TheoremAbel–Ruffini theorem#●ready to prove

Let \(n \ge 1\) be a natural number. Every complex root of every polynomial with rational coefficients of degree exactly \(n\) is expressible by radicals over \(\mathbb{Q}\) if and only if \(n \le 4\). Here a complex number is expressible by radicals over \(\mathbb{Q}\) when it lies in the smallest subfield \(S\) of \(\mathbb{C}\) such that \(z \in S\) whenever \(z \in \mathbb{C}\) and \(z^k \in S\) for some integer \(k \ge 1\).

The direction from radical solvability to \(n \le 4\) is the classical insolvability of the general quintic, extended to higher degrees; the converse follows from the explicit formulas of Cardano and Ferrari for degrees at most four.

public theorem_wanted abel_ruffini (n : ℕ) (_hn : 1 ≤ n) :
    (∀ p : ℚ[X], p.natDegree = n → ∀ x : ℂ, aeval x p = 0 →
        x ∈ solvableByRad ℚ ℂ) ↔ n ≤ 4

Sources

• P. Ruffini (1799), N. H. Abel (1824), É. Galois (1832). Listed as §57 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf); the general-quintic insolvability is #16 on Freek Wiedijk's Formalizing 100 Theorems list (https://www.cs.ru.nl/~freek/100/). Problem abel_ruffini of the lean-eval benchmark.

TheoremSolvable extensions ↔ solvable groups#●ready to prove

Let \(F\) be a field of characteristic zero and let \(p \in F[X]\) be a nonzero polynomial. Every root of \(p\) in an algebraic closure \(\overline{F}\) of \(F\) is solvable by radicals over \(F\) (obtainable from \(F\) by field operations and \(n\)-th roots inside \(\overline{F}\)) if and only if the Galois group of \(p\) over \(F\) is solvable.

public theorem_wanted solvable_iff_solvableByRad (F : Type*) [Field F] [CharZero F]
    (p : F[X]) (_hp : p ≠ 0) :
    (∀ x : AlgebraicClosure F, aeval x p = 0 →
        x ∈ solvableByRad F (AlgebraicClosure F)) ↔ Group.IsSolvable p.Gal

Sources

• É. Galois (1832); the iff appears in standard texts such as Stewart, Galois Theory (Theorem 18.10); Lang, Algebra (VI §7); Rotman, Galois Theory (Theorem 73). Listed as §58 (additional statement 2) in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem solvable_by_radicals_converse of the lean-eval benchmark.

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.