Shafarevich's theorem on solvable Galois groups

shafarevich_solvable_galois

Submitter: Ryan Smith.

Notes: Every finite solvable group is realizable as a Galois group over ℚ: the solvable case of the inverse Galois problem. Mathlib has IsSolvable and the Galois correspondence, but nothing about realizability — no embedding problems, no Scholz–Reichardt construction, no inverse-Galois API at all — so a solver builds the extensions from scratch. Distinct from the two other Shafarevich problems in the catalog: shafarevich_relation_rank_bound (the cohomological relation-rank inequality for the maximal unramified pro-p extension) and golod_shafarevich_inequality. Shafarevich's original 1954 proof contained an error at the prime 2, which he later corrected; the source field cites both the correction and a modern complete proof.

Source: I. R. Shafarevich, 'Construction of fields of algebraic numbers with given solvable Galois group', Izv. Akad. Nauk SSSR Ser. Mat. 18 (1954), no. 6, 525–578, https://www.mathnet.ru/eng/im3517. The prime-2 correction appears in Shafarevich's Collected Mathematical Papers, Springer (1989). For a complete corrected proof, see A. Schmidt and K. Wingberg, 'Šafarevič's theorem on solvable groups as Galois groups' (1998), https://arxiv.org/abs/math/9809211.

Informal solution: Reduce the realization problem to split finite embedding problems with nilpotent kernels. For each p-primary kernel, construct controlled Scholz solutions and solve successive central embedding problems. When an obstruction appears, Shafarevich's shrinking procedure modifies earlier stages so that the obstruction vanishes; the corrected argument handles the prime 2. Iterating along a solvable series yields a finite Galois extension K/ℚ with Galois group G.

theorem declaration uses `sorry`shafarevich_solvable_galois (G : Type*) [Group G] [Finite G] [IsSolvable G] :
    ∃ (K : Type) (_ : Field K) (_ : Algebra ℚ K) (_ : FiniteDimensional ℚ K) (_ : IsGalois ℚ K),
      Nonempty (G ≃* (K ≃ₐ[ℚ] K)) := byG:Type u_1inst✝²:Group Ginst✝¹:Finite Ginst✝:IsSolvable G⊢ ∃ K x x_1, ∃ (_ : FiniteDimensional ℚ K) (_ : IsGalois ℚ K), Nonempty (G ≃* Gal(K/ℚ))
  sorryAll goals completed! 🐙

Solved by

Not yet solved.