<commit_before>/-
Copyright (c) 2021 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import field_theory.abel_ruffini
import analysis.calculus.local_extr
/-!
Construction of an algebraic number that is not solvable by radicals.

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.

-/

namespace abel_ruffini

open function polynomial polynomial.gal ideal

local attribute [instance] splits_ℚ_ℂ

variables (R : Type*) [comm_ring R] (a b : ℕ)

/-- A quintic polynomial that we will show is irreducible -/
noncomputable def Φ : polynomial R := X ^ 5 - C ↑a * X + C ↑b

variables {R}

@[simp] lemma map_Phi {S : Type*} [comm_ring S] (f : R →+* S) : (Φ R a b).map f = Φ S a b :=
by simp [Φ]

@[simp] lemma coeff_zero_Phi : (Φ R a b).coeff 0 = ↑b :=
by simp [Φ, coeff_X_pow]

@[simp] lemma coeff_five_Phi : (Φ R a b).coeff 5 = 1 :=
by simp [Φ, coeff_X, coeff_C, -C_eq_nat_cast, -ring_hom.map_nat_cast]

variables [nontrivial R]

lemma degree_Phi : (Φ R a b).degree = ↑5 :=
begin
  suffices : degree (X ^ 5 - C ↑a * X) = ↑5,
  { rwa [Φ, degree_add_eq_left_of_degree_lt],
    convert degree_C_le.trans_lt (with_bot.coe_lt_coe.mpr (nat.zero_lt_bit1 2)) },
  rw degree_sub_eq_left_of_degree_lt; rw degree_X_pow,
  exact (degree_C_mul_X_le _).trans_lt (with_bot.coe_lt_coe.mpr (nat.one_lt_bit1 two_ne_zero)),
end

lemma nat_degree_Phi : (Φ R a b).nat_degree = 5 :=
nat_degree_eq_of_degree_eq_some (degree_Phi a b)

lemma leading_coeff_Phi : (Φ R a b).leading_coeff = 1 :=
by rw [polynomial.leading_coeff, nat_degree_Phi, coeff_five_Phi]

lemma monic_Phi : (Φ R a b).monic :=
leading_coeff_Phi a b

lemma irreducible_Phi (p : ℕ) (hp : p.prime) (hpa : p ∣ a) (hpb : p ∣ b) (hp2b : ¬ p ^ 2 ∣ b) :
  irreducible (Φ ℚ a b) :=
begin
  rw [←map_Phi a b (int.cast_ring_hom ℚ), ←is_primitive.int.irreducible_iff_irreducible_map_cast],
  apply irreducible_of_eisenstein_criterion,
  { rwa [span_singleton_prime (int.coe_nat_ne_zero.mpr hp.ne_zero), int.prime_iff_nat_abs_prime] },
  { rw [leading_coeff_Phi, mem_span_singleton],
    exact_mod_cast mt nat.dvd_one.mp (hp.ne_one) },
  { intros n hn,
    rw mem_span_singleton,
    rw [degree_Phi, with_bot.coe_lt_coe] at hn,
    interval_cases n with hn;
    simp [Φ, coeff_X_pow, coeff_C, int.coe_nat_dvd.mpr, hpb, hpa, -ring_hom.eq_int_cast] },
  { simp only [degree_Phi, ←with_bot.coe_zero, with_bot.coe_lt_coe, nat.succ_pos'] },
  { rw [coeff_zero_Phi, span_singleton_pow, mem_span_singleton, int.nat_cast_eq_coe_nat],
    exact mt int.coe_nat_dvd.mp hp2b },
  all_goals { exact monic.is_primitive (monic_Phi a b) },
end

lemma real_roots_Phi_le : fintype.card ((Φ ℚ a b).root_set ℝ) ≤ 3 :=
begin
  rw [←map_Phi a b (algebra_map ℤ ℚ), Φ, ←one_mul (X ^ 5), ←C_1],
  refine (card_root_set_le_derivative _).trans
    (nat.succ_le_succ ((card_root_set_le_derivative _).trans (nat.succ_le_succ _))),
  suffices : ((C ((algebra_map ℤ ℚ) 20) * X ^ 3).root_set ℝ).subsingleton,
  { norm_num [fintype.card_le_one_iff_subsingleton, ← mul_assoc, *] at * },
  rw root_set_C_mul_X_pow; norm_num,
end
<commit_msg>feat(archive/abel_ruffini): speedup by squeezing  (#9709)<commit_after>/-
Copyright (c) 2021 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import field_theory.abel_ruffini
import analysis.calculus.local_extr
/-!
Construction of an algebraic number that is not solvable by radicals.

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.

-/

namespace abel_ruffini

open function polynomial polynomial.gal ideal

local attribute [instance] splits_ℚ_ℂ

variables (R : Type*) [comm_ring R] (a b : ℕ)

/-- A quintic polynomial that we will show is irreducible -/
noncomputable def Φ : polynomial R := X ^ 5 - C ↑a * X + C ↑b

variables {R}

@[simp] lemma map_Phi {S : Type*} [comm_ring S] (f : R →+* S) : (Φ R a b).map f = Φ S a b :=
by simp [Φ]

@[simp] lemma coeff_zero_Phi : (Φ R a b).coeff 0 = ↑b :=
by simp [Φ, coeff_X_pow]

@[simp] lemma coeff_five_Phi : (Φ R a b).coeff 5 = 1 :=
by simp [Φ, coeff_X, coeff_C, -C_eq_nat_cast, -ring_hom.map_nat_cast]

variables [nontrivial R]

lemma degree_Phi : (Φ R a b).degree = ↑5 :=
begin
  suffices : degree (X ^ 5 - C ↑a * X) = ↑5,
  { rwa [Φ, degree_add_eq_left_of_degree_lt],
    convert degree_C_le.trans_lt (with_bot.coe_lt_coe.mpr (nat.zero_lt_bit1 2)) },
  rw degree_sub_eq_left_of_degree_lt; rw degree_X_pow,
  exact (degree_C_mul_X_le _).trans_lt (with_bot.coe_lt_coe.mpr (nat.one_lt_bit1 two_ne_zero)),
end

lemma nat_degree_Phi : (Φ R a b).nat_degree = 5 :=
nat_degree_eq_of_degree_eq_some (degree_Phi a b)

lemma leading_coeff_Phi : (Φ R a b).leading_coeff = 1 :=
by rw [polynomial.leading_coeff, nat_degree_Phi, coeff_five_Phi]

lemma monic_Phi : (Φ R a b).monic :=
leading_coeff_Phi a b

lemma irreducible_Phi (p : ℕ) (hp : p.prime) (hpa : p ∣ a) (hpb : p ∣ b) (hp2b : ¬ p ^ 2 ∣ b) :
  irreducible (Φ ℚ a b) :=
begin
  rw [←map_Phi a b (int.cast_ring_hom ℚ), ←is_primitive.int.irreducible_iff_irreducible_map_cast],
  apply irreducible_of_eisenstein_criterion,
  { rwa [span_singleton_prime (int.coe_nat_ne_zero.mpr hp.ne_zero), int.prime_iff_nat_abs_prime] },
  { rw [leading_coeff_Phi, mem_span_singleton],
    exact_mod_cast mt nat.dvd_one.mp (hp.ne_one) },
  { intros n hn,
    rw mem_span_singleton,
    rw [degree_Phi, with_bot.coe_lt_coe] at hn,
    interval_cases n with hn;
    simp only [Φ, coeff_X_pow, coeff_C, int.coe_nat_dvd.mpr, hpb, if_true, coeff_C_mul, if_false,
      nat.zero_ne_bit1, eq_self_iff_true, coeff_X_zero, hpa, coeff_add, zero_add, mul_zero,
      int.nat_cast_eq_coe_nat, coeff_sub, sub_self, nat.one_ne_zero, add_zero, coeff_X_one, mul_one,
      zero_sub, dvd_neg, nat.one_eq_bit1, bit0_eq_zero, neg_zero, nat.bit0_ne_bit1,
      dvd_mul_of_dvd_left, nat.bit1_eq_bit1, nat.one_ne_bit0, nat.bit1_ne_zero], },
  { simp only [degree_Phi, ←with_bot.coe_zero, with_bot.coe_lt_coe, nat.succ_pos'] },
  { rw [coeff_zero_Phi, span_singleton_pow, mem_span_singleton, int.nat_cast_eq_coe_nat],
    exact mt int.coe_nat_dvd.mp hp2b },
  all_goals { exact monic.is_primitive (monic_Phi a b) },
end

lemma real_roots_Phi_le : fintype.card ((Φ ℚ a b).root_set ℝ) ≤ 3 :=
begin
  rw [←map_Phi a b (algebra_map ℤ ℚ), Φ, ←one_mul (X ^ 5), ←C_1],
  refine (card_root_set_le_derivative _).trans
    (nat.succ_le_succ ((card_root_set_le_derivative _).trans (nat.succ_le_succ _))),
  suffices : ((C ((algebra_map ℤ ℚ) 20) * X ^ 3).root_set ℝ).subsingleton,
  { norm_num [fintype.card_le_one_iff_subsingleton, ← mul_assoc, *] at * },
  rw root_set_C_mul_X_pow; norm_num,
end

{'fraction_non_alphanumeric': 0.10944952945726441, 'fraction_numerical': 0.009153023075931417, 'mean_word_length': 4.593366979091565, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5992330', 'n_tokens_mistral': 3394, 'n_tokens_neox': 3201, 'n_words': 840}