Inverse Galois problem

Reference: Wikipedia

structure GaloisRealization (K : Type u_1) (G : Type u_2) [Field K] [Group G] : Type (max (max u_1 u_2) (u_3 + 1))

• L : Type u_3
• to_field : Field self.L
• to_algebra : Algebra K self.L
• to_isGalois : IsGalois K self.L
• iso : G ≃* self.L ≃ₐ[K] self.L

class IsRealizable (K : Type u_1) (G : Type u_2) [Field K] [Group G] : Prop

Say a group G is realizable over a field K if it is isomorphic to the Galois group of a Galois extension of K

• exists_realization : Nonempty (GaloisRealization K G)

theorem inverse_galois_problem {G : Type u_1} [Fintype G] [Group G] : IsRealizable ℚ G

The Inverse Galois Problem: every finite group is isomorphic to the Galois group of a Galois extension of the rationals.

theorem inverse_galois_problem.variants.cyclic {G : Type u_1} [Fintype G] [Group G] [IsCyclic G] : IsRealizable ℚ G

Every finite cyclic group is realizable.

theorem inverse_galois_problem.variants.abelian {G : Type u_1} [Fintype G] [CommGroup G] : IsRealizable ℚ G

Every finite abelian group is realizable.

theorem inverse_galois_problem.variants.symmetric_group {S : Type u_1} [Fintype S] : IsRealizable ℚ (S ≃ S)

Every finite symmetric group is realizable.

theorem inverse_galois_problem.variants.complex_rational_functions {G : Type u_1} [Fintype G] [Group G] : IsRealizable (RatFunc ℂ) G

Every finite group is realisable over the field of rational functions with complex coefficients.

theorem inverse_galois_problem.variants.complex_function_field {G : Type u_1} {K : Type u_2} [Field K] [CharZero K] [Fintype G] [Group G] : IsRealizable (RatFunc K) G

Every finite group is realisable over the field of rational functions with coefficients K, where K is any field of characteristic 0.