Solvable extensions ↔ solvable groups (the missing converse in Abel–Ruffini)

solvable_by_radicals_converse — a formalization challenge from the lean-eval benchmark.

Notes

§58 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement). For F : Field of characteristic zero and a nonzero p : F[X], every root of p in AlgebraicClosure F lies in solvableByRad F (AlgebraicClosure F) iff p.Gal is solvable. Mathlib has the → direction via isSolvable_gal_of_irreducible / isSolvable_gal_minpoly in Mathlib/FieldTheory/AbelRuffini.lean (the file header states it proves 'one direction' of Abel–Ruffini). The ← direction is the Kummer-theory content and is the missing piece. The polynomial-level iff is stronger than the irreducible/minpoly form already in mathlib.

Formal statement

/-- **Solvable extensions ↔ solvable groups.** For a field `F` of
characteristic zero and a nonzero `p : F[X]`, every root of `p` in
`AlgebraicClosure F` lies in `solvableByRad F (AlgebraicClosure F)`
iff `p.Gal` is solvable. -/
theorem 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)) ↔ IsSolvable p.Gal := by
  sorry

Informal solution sketch

Classical proof of the ← direction: assume p.Gal is solvable. Adjoin to F a sufficient root of unity (a primitive n-th root for n = |p.Gal|) to obtain F' = F(ζ); the Galois group of the splitting field L of p over F' is a subgroup of Gal(p over F) hence still solvable, and F'/F is a radical extension. Take a composition series G = G₀ ▹ G₁ ▹ ⋯ ▹ Gₖ = 1 of Gal(L/F') with each factor cyclic of prime order. The corresponding tower of fixed fields is F' = L^{G₀} ⊂ L^{G₁} ⊂ ⋯ ⊂ L^{Gₖ} = L, with each step Galois cyclic of prime order over a field containing the relevant root of unity; by Kummer theory each step is a pure radical extension. The splitting field of p sits inside L, so every root of p lies in solvableByRad F (AlgebraicClosure F). The → direction follows from the existing mathlib lemma isSolvable_gal_of_irreducible applied to each irreducible factor.

Source

É. 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).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: solvable_iff_solvableByRad
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.