feat(data/polynomial/unit_trinomial): Irreducibility of X^n-X-1 (#15318)

This PR adds a proves irreducibility of X^n-X-1, superseding #6421.

src/data/polynomial/unit_trinomial.lean

@@ -6,7 +6,6 @@ Authors: Thomas Browning
 
 import analysis.complex.polynomial
 import data.polynomial.mirror
-import ring_theory.roots_of_unity
 
 /-!
 # Unit Trinomials
@@ -21,7 +20,6 @@ This file defines irreducible trinomials and proves an irreducibility criterion.
 
 - `polynomial.irreducible_of_coprime`: An irreducibility criterion for unit trinomials.
 
-TODO: Irreducibility of x^n-x-1
 -/
 
 namespace polynomial
@@ -89,6 +87,13 @@ lemma trinomial_trailing_coeff (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) :
   (trinomial k m n u v w).trailing_coeff = u :=
 by rw [trailing_coeff, trinomial_nat_trailing_degree hkm hmn hu, trinomial_trailing_coeff' hkm hmn]
 
+lemma trinomial_monic (hkm : k < m) (hmn : m < n) : (trinomial k m n u v 1).monic :=
+begin
+  casesI subsingleton_or_nontrivial R with h h,
+  { apply subsingleton.elim },
+  { exact trinomial_leading_coeff hkm hmn one_ne_zero },
+end
+
 lemma trinomial_mirror (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) (hw : w ≠ 0) :
   (trinomial k m n u v w).mirror = trinomial k (n - m + k) n w v u :=
 by rw [mirror, trinomial_nat_trailing_degree hkm hmn hu, reverse, trinomial_nat_degree hkm hmn hw,
@@ -233,7 +238,7 @@ lemma irreducible_aux2 {k m m' n : ℕ}
   (h : p * p.mirror = q * q.mirror) :
   q = p ∨ q = p.mirror :=
 begin
-  let f : polynomial ℤ → polynomial ℤ :=
+  let f : ℤ[X] → ℤ[X] :=
   λ p, ⟨finsupp.filter (set.Ioo (k + n) (n + n)) p.to_finsupp⟩,
   replace h := congr_arg f h,
   replace h := (irreducible_aux1 hkm hmn u v w hp).trans h,
@@ -321,10 +326,38 @@ begin
     { exact or.inr (or.inr (or.inr p.mirror_neg)) } },
 end
 
+/-- A unit trinomial is irreducible if it is coprime with its mirror -/
 lemma irreducible_of_is_coprime (hp : p.is_unit_trinomial) (h : is_coprime p p.mirror) :
   irreducible p :=
 irreducible_of_coprime hp (λ q, h.is_unit_of_dvd')
 
+/-- A unit trinomial is irreducible if it has no complex roots in common with its mirror -/
+lemma irreducible_of_coprime' (hp : is_unit_trinomial p)
+  (h : ∀ z : ℂ, ¬ (aeval z p = 0 ∧ aeval z (mirror p) = 0)) : irreducible p :=
+begin
+  refine hp.irreducible_of_coprime (λ q hq hq', _),
+  suffices : ¬ (0 < q.nat_degree),
+  { rcases hq with ⟨p, rfl⟩,
+    replace hp := hp.leading_coeff_is_unit,
+    rw leading_coeff_mul at hp,
+    replace hp := is_unit_of_mul_is_unit_left hp,
+    rw [not_lt, nat.le_zero_iff] at this,
+    rwa [eq_C_of_nat_degree_eq_zero this, is_unit_C, ←this] },
+  intro hq'',
+  rw nat_degree_pos_iff_degree_pos at hq'',
+  rw ← degree_map_eq_of_injective (algebra_map ℤ ℂ).injective_int at hq'',
+  cases complex.exists_root hq'' with z hz,
+  rw [is_root, eval_map, ←aeval_def] at hz,
+  refine h z ⟨_, _⟩,
+  { cases hq with g' hg',
+    rw [hg', aeval_mul, hz, zero_mul] },
+  { cases hq' with g' hg',
+    rw [hg', aeval_mul, hz, zero_mul] },
+end
+
+-- TODO: Develop more theory (e.g., it suffices to check that `aeval z p ≠ 0` for `z = 0`
+-- and `z` a root of unity)
+
 end is_unit_trinomial
 
 end polynomial

src/ring_theory/polynomial/selmer.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2022 Thomas Browning. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Browning
+-/
+
+import data.polynomial.unit_trinomial
+import tactic.linear_combination
+
+/-!
+# Irreducibility of Selmer Polynomials
+
+This file proves irreducibility of the Selmer polynomials `X ^ n - X - 1`.
+
+## Main results
+
+- `polynomial.selmer_irreducible`: The Selmer polynomials `X ^ n - X - 1` are irreducible.
+
+TODO: Show that the Selmer polynomials have full Galois group.
+-/
+
+namespace polynomial
+open_locale polynomial
+
+variables {n : ℕ}
+
+lemma X_pow_sub_X_sub_one_irreducible_aux (z : ℂ) : ¬ (z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0) :=
+begin
+  rintros ⟨h1, h2⟩,
+  replace h3 : z ^ 3 = 1,
+  { linear_combination (1 - z - z ^ 2 - z ^ n) * h1 + (z ^ n - 2) * h2 }, -- thanks polyrith!
+  have key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2,
+  { rw [←nat.mod_add_div n 3, pow_add, pow_mul, h3, one_pow, mul_one],
+    have : n % 3 < 3 := nat.mod_lt n zero_lt_three,
+    interval_cases n % 3; simp only [h, pow_zero, pow_one, eq_self_iff_true, or_true, true_or] },
+  have z_ne_zero : z ≠ 0 :=
+  λ h, zero_ne_one ((zero_pow zero_lt_three).symm.trans (show (0 : ℂ) ^ 3 = 1, from h ▸ h3)),
+  rcases key with key | key | key,
+  { exact z_ne_zero (by rwa [key, self_eq_add_left] at h1) },
+  { exact one_ne_zero (by rwa [key, self_eq_add_right] at h1) },
+  { exact z_ne_zero (pow_eq_zero (by rwa [key, add_self_eq_zero] at h2)) },
+end
+
+lemma X_pow_sub_X_sub_one_irreducible (hn1 : n ≠ 1) : irreducible (X ^ n - X - 1 : ℤ[X]) :=
+begin
+  by_cases hn0 : n = 0,
+  { rw [hn0, pow_zero, sub_sub, add_comm, ←sub_sub, sub_self, zero_sub],
+    exact associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X },
+  have hn : 1 < n := nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩,
+  have hp : (X ^ n - X - 1 : ℤ[X]) = trinomial 0 1 n (-1) (-1) 1 :=
+    by simp only [trinomial, C_neg, C_1]; ring,
+  rw hp,
+  apply is_unit_trinomial.irreducible_of_coprime' ⟨0, 1, n, zero_lt_one, hn, -1, -1, 1, rfl⟩,
+  rintros z ⟨h1, h2⟩,
+  apply X_pow_sub_X_sub_one_irreducible_aux z,
+  rw [trinomial_mirror zero_lt_one hn (-1 : ℤˣ).ne_zero (1 : ℤˣ).ne_zero] at h2,
+  simp_rw [trinomial, aeval_add, aeval_mul, aeval_X_pow, aeval_C] at h1 h2,
+  simp_rw [units.coe_neg, units.coe_one, map_neg, map_one] at h1 h2,
+  replace h1 : z ^ n = z + 1 := by linear_combination h1,
+  replace h2 := mul_eq_zero_of_left h2 z,
+  rw [add_mul, add_mul, add_zero, mul_assoc (-1 : ℂ), ←pow_succ', nat.sub_add_cancel hn.le] at h2,
+  rw h1 at h2 ⊢,
+  exact ⟨rfl, by linear_combination -h2⟩,
+end
+
+lemma X_pow_sub_X_sub_one_irreducible_rat (hn1 : n ≠ 1) : irreducible (X ^ n - X - 1 : ℚ[X]) :=
+begin
+  by_cases hn0 : n = 0,
+  { rw [hn0, pow_zero, sub_sub, add_comm, ←sub_sub, sub_self, zero_sub],
+    exact associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X },
+  have hp : (X ^ n - X - 1 : ℤ[X]) = trinomial 0 1 n (-1) (-1) 1 :=
+  by simp only [trinomial, C_neg, C_1]; ring,
+  have hn : 1 < n := nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩,
+  have h := (is_primitive.int.irreducible_iff_irreducible_map_cast _).mp
+    (X_pow_sub_X_sub_one_irreducible hn1),
+  { rwa [polynomial.map_sub, polynomial.map_sub, polynomial.map_pow, polynomial.map_one,
+      polynomial.map_X] at h },
+  { exact hp.symm ▸ (trinomial_monic zero_lt_one hn).is_primitive },
+end
+
+end polynomial