Construction of an algebraic number that is not solvable by radicals. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The main ingredients are:

solvable_by_rad.is_solvable' in field_theory/abel_ruffini : an irreducible polynomial with an is_solvable_by_rad root has solvable Galois group
gal_action_hom_bijective_of_prime_degree' in field_theory/polynomial_galois_group : an irreducible polynomial of prime degree with 1-3 non-real roots has full Galois group
equiv.perm.not_solvable in group_theory/solvable : the symmetric group is not solvable

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

source

noncomputable def abel_ruffini.Φ (R : Type u_1) [comm_ring R] (a b : ℕ) :

polynomial R

A quintic polynomial that we will show is irreducible

Equations

abel_ruffini.Φ R a b = polynomial.X ^ 5 - ⇑polynomial.C ↑a * polynomial.X + ⇑polynomial.C ↑b

source

@[simp]

theorem abel_ruffini.map_Phi {R : Type u_1} [comm_ring R] (a b : ℕ) {S : Type u_2} [comm_ring S] (f : R →+* S) :

polynomial.map f (abel_ruffini.Φ R a b) = abel_ruffini.Φ S a b

source

@[simp]

theorem abel_ruffini.coeff_zero_Phi {R : Type u_1} [comm_ring R] (a b : ℕ) :

(abel_ruffini.Φ R a b).coeff 0 = ↑b

source

@[simp]

theorem abel_ruffini.coeff_five_Phi {R : Type u_1} [comm_ring R] (a b : ℕ) :

(abel_ruffini.Φ R a b).coeff 5 = 1

source

theorem abel_ruffini.degree_Phi {R : Type u_1} [comm_ring R] (a b : ℕ) [nontrivial R] :

(abel_ruffini.Φ R a b).degree = ↑5

source

theorem abel_ruffini.nat_degree_Phi {R : Type u_1} [comm_ring R] (a b : ℕ) [nontrivial R] :

(abel_ruffini.Φ R a b).nat_degree = 5

source

theorem abel_ruffini.leading_coeff_Phi {R : Type u_1} [comm_ring R] (a b : ℕ) [nontrivial R] :

(abel_ruffini.Φ R a b).leading_coeff = 1

source

theorem abel_ruffini.monic_Phi {R : Type u_1} [comm_ring R] (a b : ℕ) [nontrivial R] :

(abel_ruffini.Φ R a b).monic

source

theorem abel_ruffini.irreducible_Phi (a b p : ℕ) (hp : nat.prime p) (hpa : p ∣ a) (hpb : p ∣ b) (hp2b : ¬p ^ 2 ∣ b) :

irreducible (abel_ruffini.Φ ℚ a b)

source

theorem abel_ruffini.real_roots_Phi_le (a b : ℕ) :

fintype.card ↥((abel_ruffini.Φ ℚ a b).root_set ℝ) ≤ 3

source

theorem abel_ruffini.real_roots_Phi_ge_aux (a b : ℕ) (hab : b < a) :

∃ (x y : ℝ), x ≠ y ∧ ⇑(polynomial.aeval x) (abel_ruffini.Φ ℚ a b) = 0 ∧ ⇑(polynomial.aeval y) (abel_ruffini.Φ ℚ a b) = 0

source

theorem abel_ruffini.real_roots_Phi_ge (a b : ℕ) (hab : b < a) :

2 ≤ fintype.card ↥((abel_ruffini.Φ ℚ a b).root_set ℝ)

source

theorem abel_ruffini.complex_roots_Phi (a b : ℕ) (h : (abel_ruffini.Φ ℚ a b).separable) :

fintype.card ↥((abel_ruffini.Φ ℚ a b).root_set ℂ) = 5

source

theorem abel_ruffini.gal_Phi (a b : ℕ) (hab : b < a) (h_irred : irreducible (abel_ruffini.Φ ℚ a b)) :

function.bijective ⇑(polynomial.gal.gal_action_hom (abel_ruffini.Φ ℚ a b) ℂ)

source

theorem abel_ruffini.not_solvable_by_rad (a b p : ℕ) (x : ℂ) (hx : ⇑(polynomial.aeval x) (abel_ruffini.Φ ℚ a b) = 0) (hab : b < a) (hp : nat.prime p) (hpa : p ∣ a) (hpb : p ∣ b) (hp2b : ¬p ^ 2 ∣ b) :

¬is_solvable_by_rad ℚ x

source

theorem abel_ruffini.not_solvable_by_rad' (x : ℂ) (hx : ⇑(polynomial.aeval x) (abel_ruffini.Φ ℚ 4 2) = 0) :

¬is_solvable_by_rad ℚ x

source

theorem abel_ruffini.exists_not_solvable_by_rad :

∃ (x : ℂ), is_algebraic ℚ x ∧ ¬is_solvable_by_rad ℚ x

Abel-Ruffini Theorem