Construction of an algebraic number that is not solvable by radicals

The main ingredients are:

• isSolvable_gal_of_irreducible in Mathlib/FieldTheory/AbelRuffini.lean: an irreducible polynomial with an IsSolvableByRad root has solvable Galois group.
• galActionHom_bijective_of_prime_degree' in Mathlib/FieldTheory/PolynomialGaloisGroup.lean : an irreducible polynomial of prime degree with 1-3 non-real roots has full Galois group.
• Equiv.Perm.not_solvable in Mathlib/GroupTheory/Solvable.lean : the symmetric group is not solvable.

Then all that remains is the construction of a specific polynomial satisfying the conditions of galActionHom_bijective_of_prime_degree', which is done in this file.

noncomputable def AbelRuffini.Φ (R : Type u_1) [CommRing R] (a b : ℕ) : Polynomial R

A quintic polynomial that we will show is irreducible

Equations

• AbelRuffini.Φ R a b = Polynomial.X ^ 5 - Polynomial.C ↑a * Polynomial.X + Polynomial.C ↑b

@[simp]

theorem AbelRuffini.map_Phi {R : Type u_1} [CommRing R] (a b : ℕ) {S : Type u_2} [CommRing S] (f : R →+* S) : Polynomial.map f (Φ R a b) = Φ S a b

@[simp]

theorem AbelRuffini.coeff_zero_Phi {R : Type u_1} [CommRing R] (a b : ℕ) : (Φ R a b).coeff 0 = ↑b

@[simp]

theorem AbelRuffini.coeff_five_Phi {R : Type u_1} [CommRing R] (a b : ℕ) : (Φ R a b).coeff 5 = 1

theorem AbelRuffini.degree_Phi {R : Type u_1} [CommRing R] (a b : ℕ) [Nontrivial R] : (Φ R a b).degree = ↑5

theorem AbelRuffini.natDegree_Phi {R : Type u_1} [CommRing R] (a b : ℕ) [Nontrivial R] : (Φ R a b).natDegree = 5

theorem AbelRuffini.leadingCoeff_Phi {R : Type u_1} [CommRing R] (a b : ℕ) [Nontrivial R] : (Φ R a b).leadingCoeff = 1

theorem AbelRuffini.monic_Phi {R : Type u_1} [CommRing R] (a b : ℕ) [Nontrivial R] : (Φ R a b).Monic

theorem AbelRuffini.irreducible_Phi (a b p : ℕ) (hp : Nat.Prime p) (hpa : p ∣ a) (hpb : p ∣ b) (hp2b : ¬p ^ 2 ∣ b) : Irreducible (Φ ℚ a b)

theorem AbelRuffini.real_roots_Phi_le (a b : ℕ) : Fintype.card ↑((Φ ℚ a b).rootSet ℝ) ≤ 3

theorem AbelRuffini.real_roots_Phi_ge_aux (a b : ℕ) (hab : b < a) : ∃ (x : ℝ) (y : ℝ), x ≠ y ∧ (Polynomial.aeval x) (Φ ℚ a b) = 0 ∧ (Polynomial.aeval y) (Φ ℚ a b) = 0

theorem AbelRuffini.real_roots_Phi_ge (a b : ℕ) (hab : b < a) : 2 ≤ Fintype.card ↑((Φ ℚ a b).rootSet ℝ)

theorem AbelRuffini.complex_roots_Phi (a b : ℕ) (h : (Φ ℚ a b).Separable) : Fintype.card ↑((Φ ℚ a b).rootSet ℂ) = 5

theorem AbelRuffini.gal_Phi (a b : ℕ) (hab : b < a) (h_irred : Irreducible (Φ ℚ a b)) : Function.Bijective ⇑(Polynomial.Gal.galActionHom (Φ ℚ a b) ℂ)

theorem AbelRuffini.not_solvable_by_rad (a b p : ℕ) (x : ℂ) (hx : (Polynomial.aeval x) (Φ ℚ a b) = 0) (hab : b < a) (hp : Nat.Prime p) (hpa : p ∣ a) (hpb : p ∣ b) (hp2b : ¬p ^ 2 ∣ b) : x ∉ solvableByRad ℚ ℂ

theorem AbelRuffini.not_solvable_by_rad' (x : ℂ) (hx : (Polynomial.aeval x) (Φ ℚ 4 2) = 0) : x ∉ solvableByRad ℚ ℂ

theorem AbelRuffini.exists_not_solvable_by_rad : ∃ (x : ℂ), IsAlgebraic ℚ x ∧ x ∉ solvableByRad ℚ ℂ

Abel-Ruffini Theorem