feat(ring_theory/polynomial/chebyshev/dickson): Introduce generalised…

… Dickson polynomials (#5869)

and replace lambdashev with dickson 1 1. 



Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Julian <kuelsha@mathematik.uni-stuttgart.de>

docs/references.bib

@@ -545,6 +545,21 @@ @misc{scholze2011perfectoid
       primaryClass={math.AG}
 }
 
+@book {MR1237403,
+    AUTHOR = {Lidl, R. and Mullen, G. L. and Turnwald, G.},
+     TITLE = {Dickson polynomials},
+    SERIES = {Pitman Monographs and Surveys in Pure and Applied Mathematics},
+    VOLUME = {65},
+ PUBLISHER = {Longman Scientific \& Technical, Harlow; copublished in the
+              United States with John Wiley \& Sons, Inc., New York},
+      YEAR = {1993},
+     PAGES = {vi+207},
+      ISBN = {0-582-09119-5},
+   MRCLASS = {11T06 (12E05 13B25 33C80 94A60)},
+  MRNUMBER = {1237403},
+MRREVIEWER = {S. D. Cohen}
+}
+
 @misc{ponton2020chebyshev,
       title={Roots of {C}hebyshev polynomials: a purely algebraic approach},
       author={Lionel Ponton},

src/ring_theory/polynomial/chebyshev/basic.lean

@@ -5,6 +5,7 @@ Authors: Johan Commelin
 -/
 
 import ring_theory.polynomial.chebyshev.defs
+import ring_theory.polynomial.chebyshev.dickson
 import analysis.special_functions.trigonometric
 import ring_theory.localization
 import data.zmod.basic
@@ -17,14 +18,15 @@ The Chebyshev polynomials are two families of polynomials indexed by `ℕ`,
 with integral coefficients.
 In this file, we only consider Chebyshev polynomials of the first kind.
 
-## Main declarations
+## Main statements
 
 * `polynomial.chebyshev₁_mul`, the `(m * n)`-th Chebyshev polynomial is the composition
   of the `m`-th and `n`-th Chebyshev polynomials.
-* `polynomial.lambdashev_mul`, the `(m * n)`-th lambdashev polynomial is the composition
-  of the `m`-th and `n`-th lambdashev polynomials.
-* `polynomial.lambdashev_char_p`, for a prime number `p`, the `p`-th lambdashev polynomial
-  is congruent to `X ^ p` modulo `p`.
+* `polynomial.dickson_one_one_mul`, the `(m * n)`-th Dickson polynomial of the first kind for
+  parameter `1 : R` is the composition of the `m`-th and `n`-th Dickson polynomials of the first
+  kind for `1 : R`.
+* `polynomial.dickson_one_one_char_p`, for a prime number `p`, the `p`-th Dickson polynomial of the
+  first kind associated to parameter `1 : R` is congruent to `X ^ p` modulo `p`.
 
 ## Implementation details
 
@@ -54,67 +56,72 @@ begin
   apply polynomial.funext,
   intro z,
   obtain ⟨θ, rfl⟩ := cos_surjective z,
-  simp only [chebyshev₁_complex_cos, nat.cast_mul, eval_comp, mul_assoc],
+  simp only [chebyshev₁_complex_cos, nat.cast_mul, eval_comp, mul_assoc]
 end
 
-section lambdashev
+section dickson
 /-!
 
 ### A Lambda structure on `polynomial ℤ`
 
 Mathlib doesn't currently know what a Lambda ring is.
 But once it does, we can endow `polynomial ℤ` with a Lambda structure
-in terms of the `lambdashev` polynomials defined below.
+in terms of the `dickson 1 1` polynomials defined below.
 There is exactly one other Lambda structure on `polynomial ℤ` in terms of binomial polynomials.
 
 -/
 
 variables {R}
 
-lemma lambdashev_eval_add_inv (x y : R) (h : x * y = 1) :
-  ∀ n, (lambdashev R n).eval (x + y) = x ^ n + y ^ n
-| 0       := by simp only [bit0, eval_one, eval_add, pow_zero, lambdashev_zero]
-| 1       := by simp only [eval_X, lambdashev_one, pow_one]
+lemma dickson_one_one_eval_add_inv (x y : R) (h : x * y = 1) :
+  ∀ n, (dickson 1 (1 : R) n).eval (x + y) = x ^ n + y ^ n
+| 0       := by { simp only [bit0, eval_one, eval_add, pow_zero, dickson_zero], norm_num }
+| 1       := by simp only [eval_X, dickson_one, pow_one]
 | (n + 2) :=
 begin
-  simp only [eval_sub, eval_mul, lambdashev_eval_add_inv, eval_X, lambdashev_add_two],
+  simp only [eval_sub, eval_mul, dickson_one_one_eval_add_inv, eval_X, dickson_add_two, C_1,
+    eval_one],
   conv_lhs { simp only [pow_succ, add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul] },
   ring_exp
 end
 
 variables (R)
 
-lemma lambdashev_eq_chebyshev₁ [invertible (2 : R)] :
-  ∀ n, lambdashev R n = 2 * (chebyshev₁ R n).comp (C (⅟2) * X)
-| 0       := by simp only [chebyshev₁_zero, mul_one, one_comp, lambdashev_zero]
-| 1       := by rw [lambdashev_one, chebyshev₁_one, X_comp, ← mul_assoc, ← C_1, ← C_bit0, ← C_mul,
+lemma dickson_one_one_eq_chebyshev₁ [invertible (2 : R)] :
+  ∀ n, dickson 1 (1 : R) n = 2 * (chebyshev₁ R n).comp (C (⅟2) * X)
+| 0       := by { simp only [chebyshev₁_zero, mul_one, one_comp, dickson_zero], norm_num }
+| 1       := by rw [dickson_one, chebyshev₁_one, X_comp, ← mul_assoc, ← C_1, ← C_bit0, ← C_mul,
                     mul_inv_of_self, C_1, one_mul]
 | (n + 2) :=
 begin
-  simp only [lambdashev_add_two, chebyshev₁_add_two, lambdashev_eq_chebyshev₁ (n + 1),
-    lambdashev_eq_chebyshev₁ n, sub_comp, mul_comp, add_comp, X_comp, bit0_comp, one_comp],
+  simp only [dickson_add_two, chebyshev₁_add_two, dickson_one_one_eq_chebyshev₁ (n + 1),
+    dickson_one_one_eq_chebyshev₁ n, sub_comp, mul_comp, add_comp, X_comp, bit0_comp, one_comp],
   simp only [← C_1, ← C_bit0, ← mul_assoc, ← C_mul, mul_inv_of_self],
   rw [C_1, one_mul],
   ring
 end
 
-lemma chebyshev₁_eq_lambdashev [invertible (2 : R)] (n : ℕ) :
-  chebyshev₁ R n = C (⅟2) * (lambdashev R n).comp (2 * X) :=
+lemma chebyshev₁_eq_dickson_one_one [invertible (2 : R)] (n : ℕ) :
+  chebyshev₁ R n = C (⅟2) * (dickson 1 1 n).comp (2 * X) :=
 begin
-  rw lambdashev_eq_chebyshev₁,
+  rw dickson_one_one_eq_chebyshev₁,
   simp only [comp_assoc, mul_comp, C_comp, X_comp, ← mul_assoc, ← C_1, ← C_bit0, ← C_mul],
   rw [inv_of_mul_self, C_1, one_mul, one_mul, comp_X]
 end
 
-/-- the `(m * n)`-th lambdashev polynomial is the composition of the `m`-th and `n`-th -/
-lemma lambdashev_mul (m n : ℕ) :
-  lambdashev R (m * n) = (lambdashev R m).comp (lambdashev R n) :=
+/-- The `(m * n)`-th Dickson polynomial of the first kind is the composition of the `m`-th and
+`n`-th. -/
+lemma dickson_one_one_mul (m n : ℕ) :
+  dickson 1 (1 : R) (m * n) = (dickson 1 1 m).comp (dickson 1 1 n) :=
 begin
-  simp only [← map_lambdashev (int.cast_ring_hom R), ← map_comp],
+  have h : (1 : R) = int.cast_ring_hom R (1),
+    simp only [ring_hom.eq_int_cast, int.cast_one],
+  rw h,
+  simp only [← map_dickson (int.cast_ring_hom R), ← map_comp],
   congr' 1,
   apply map_injective (int.cast_ring_hom ℚ) int.cast_injective,
-  simp only [map_lambdashev, map_comp, lambdashev_eq_chebyshev₁, chebyshev₁_mul, two_mul,
-    ← add_comp],
+  simp only [map_dickson, map_comp, ring_hom.eq_int_cast, int.cast_one,
+    dickson_one_one_eq_chebyshev₁, chebyshev₁_mul, two_mul, ← add_comp],
   simp only [← two_mul, ← comp_assoc],
   apply eval₂_congr rfl rfl,
   rw [comp_assoc],
@@ -123,14 +130,14 @@ begin
       inv_of_mul_self, C_1, one_mul]
 end
 
-lemma lambdashev_comp_comm (m n : ℕ) :
-  (lambdashev R m).comp (lambdashev R n) = (lambdashev R n).comp (lambdashev R m) :=
-by rw [← lambdashev_mul, mul_comm, lambdashev_mul]
+lemma dickson_one_one_comp_comm (m n : ℕ) :
+  (dickson 1 (1 : R) m).comp (dickson 1 1 n) = (dickson 1 1 n).comp (dickson 1 1 m) :=
+by rw [← dickson_one_one_mul, mul_comm, dickson_one_one_mul]
 
-lemma lambdashev_zmod_p (p : ℕ) [fact p.prime] :
-  lambdashev (zmod p) p = X ^ p :=
+lemma dickson_one_one_zmod_p (p : ℕ) [fact p.prime] :
+  dickson 1 (1 : zmod p) p = X ^ p :=
 begin
-  -- Recall that `lambdashev_eval_add_inv` characterises `lambdashev R p`
+  -- Recall that `dickson_eval_add_inv` characterises `dickson 1 1 p`
   -- as a polynomial that maps `x + x⁻¹` to `x ^ p + (x⁻¹) ^ p`.
   -- Since `X ^ p` also satisfies this property in characteristic `p`,
   -- we can use a variant on `polynomial.funext` to conclude that these polynomials are equal.
@@ -144,13 +151,14 @@ begin
     refine ⟨K, _, _, _⟩; apply_instance },
   resetI,
   apply map_injective (zmod.cast_hom (dvd_refl p) K) (ring_hom.injective _),
-  rw [map_lambdashev, map_pow, map_X],
+  rw [map_dickson, map_pow, map_X],
   apply eq_of_infinite_eval_eq,
   -- The two polynomials agree on all `x` of the form `x = y + y⁻¹`.
   apply @set.infinite_mono _ {x : K | ∃ y, x = y + y⁻¹ ∧ y ≠ 0},
   { rintro _ ⟨x, rfl, hx⟩,
     simp only [eval_X, eval_pow, set.mem_set_of_eq, @add_pow_char K _ p,
-      lambdashev_eval_add_inv _ _ (mul_inv_cancel hx)] },
+      dickson_one_one_eval_add_inv _ _ (mul_inv_cancel hx), inv_pow', zmod.cast_hom_apply,
+      zmod.cast_one'] },
   -- Now we need to show that the set of such `x` is infinite.
   -- If the set is finite, then we will show that `K` is also finite.
   { intro h,
@@ -195,10 +203,14 @@ begin
         exact ⟨_, rfl, hx⟩ } } }
 end
 
-lemma lambdashev_char_p (p : ℕ) [fact p.prime] [char_p R p] :
-  lambdashev R p = X ^ p :=
-by rw [← map_lambdashev (zmod.cast_hom (dvd_refl p) R), lambdashev_zmod_p, map_pow, map_X]
+lemma dickson_one_one_char_p (p : ℕ) [fact p.prime] [char_p R p] :
+  dickson 1 (1 : R) p = X ^ p :=
+begin
+  have h : (1 : R) = zmod.cast_hom (dvd_refl p) R (1),
+    simp only [zmod.cast_hom_apply, zmod.cast_one'],
+  rw [h, ← map_dickson (zmod.cast_hom (dvd_refl p) R), dickson_one_one_zmod_p, map_pow, map_X]
+end
 
-end lambdashev
+end dickson
 
 end polynomial

src/ring_theory/polynomial/chebyshev/defs.lean

@@ -19,8 +19,7 @@ See the file `ring_theory.polynomial.chebyshev.basic` for more properties.
 
 * `polynomial.chebyshev₁`: the Chebyshev polynomials of the first kind.
 * `polynomial.chebyshev₂`: the Chebyshev polynomials of the second kind.
-* `polynomial.lambdashev`: a variant on the Chebyshev polynomials that define a Lambda structure
-  on `polynomial ℤ`.
+
 
 ## Main statements
 
@@ -46,10 +45,6 @@ and import that file in turn, in `ring_theory.polynomial.chebyshev.basic`.
 * Compute zeroes and extrema of Chebyshev polynomials.
 * Prove that the roots of the Chebyshev polynomials (except 0) are irrational.
 * Prove minimax properties of Chebyshev polynomials.
-* Define a variant of Chebyshev polynomials of the second kind removing the 2
-  (sometimes Dickson polynomials of the second kind) or even more general Dickson polynomials.
-* Prove that the adjacency matrices of simply laced Dynkin diagrams are precisely the adjacency
-  matrices of simple connected graphs which annihilate the Dickson polynomials.
 -/
 
 
@@ -93,45 +88,6 @@ begin
   rw [map_chebyshev₁ (n + 1), map_chebyshev₁ n],
 end
 
-variables (R)
-
-/-- `lambdashev R n` is equal to `2 * (chebyshev₁ R n).comp (X / 2)`.
-It is a family of polynomials that satisfies
-`lambdashev (zmod p) p = X ^ p`, and therefore defines a Lambda structure on `polynomial ℤ`. -/
-noncomputable def lambdashev : ℕ → polynomial R
-| 0       := 2
-| 1       := X
-| (n + 2) := X * lambdashev (n + 1) - lambdashev n
-
-@[simp] lemma lambdashev_zero : lambdashev R 0 = 2 := rfl
-@[simp] lemma lambdashev_one : lambdashev R 1 = X := rfl
-lemma lambdashev_two : lambdashev R 2 = X ^ 2 - 2 :=
-by simp only [lambdashev, sub_left_inj, pow_two, mul_assoc]
-@[simp] lemma lambdashev_add_two (n : ℕ) :
-  lambdashev R (n + 2) = X * lambdashev R (n + 1) - lambdashev R n :=
-by rw lambdashev
-
-lemma lambdashev_eq_two_le (n : ℕ) (h : 2 ≤ n) :
-  lambdashev R n = X * lambdashev R (n - 1) - lambdashev R (n - 2) :=
-begin
-  obtain ⟨n, rfl⟩ := nat.exists_eq_add_of_le h,
-  rw add_comm,
-  exact lambdashev_add_two R n
-end
-
-variables {R S}
-
-lemma map_lambdashev (f : R →+* S) :
-  ∀ (n : ℕ), map f (lambdashev R n) = lambdashev S n
-| 0       := by simp only [lambdashev_zero, bit0, map_add, map_one]
-| 1       := by simp only [lambdashev_one, map_X]
-| (n + 2) :=
-begin
-  simp only [lambdashev_add_two, map_mul, map_sub, map_X, bit0, map_add, map_one],
-  rw [map_lambdashev (n + 1), map_lambdashev n],
-end
-
-
 end polynomial
 
 namespace polynomial

src/ring_theory/polynomial/chebyshev/dickson.lean

@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2021 Julian Kuelshammer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Julian Kuelshammer
+-/
+
+import data.polynomial.eval
+import ring_theory.polynomial.chebyshev.defs
+
+/-!
+# Dickson polynomials
+
+The (generalised) Dickson polynomials are a family of polynomials indexed by `ℕ × ℕ`,
+with coefficients in a commutative ring `R` depending on an element `a∈R`. More precisely, the
+they satisfy the recursion `dickson k a (n + 2) = X * (dickson k a n + 1) - a * (dickson k a n)`
+with starting values `dickson k a 0 = 3 - k` and `dickson k a 1 = X`. In the literature,
+`dickson k a n` is called the `n`-th Dickson polynomial of the `k`-th kind associated to the
+parameter `a : R`. They are closely related to the Chebyshev polynomials in the case that `a=1`.
+When `a=0` they are just the family of monomials `X ^ n`.
+
+## Main definition
+
+* `polynomial.dickson`: the generalised Dickson polynomials.
+
+## References
+
+* [R. Lidl, G. L. Mullen and G. Turnwald, _Dickson polynomials_][MR1237403]
+
+## TODO
+
+* Redefine `dickson` in terms of `linear_recurrence`.
+* Show that `dickson 2 1` is equal to the characteristic polynomial of the adjacency matrix of a
+  type A Dynkin diagram.
+* Prove that the adjacency matrices of simply laced Dynkin diagrams are precisely the adjacency
+  matrices of simple connected graphs which annihilate `dickson 2 1`.
+-/
+
+noncomputable theory
+
+namespace polynomial
+
+variables {R S : Type*} [comm_ring R] [comm_ring S] (k : ℕ) (a : R)
+
+/-- `dickson` is the `n`the (generalised) Dickson polynomial of the `k`-th kind associated to the
+element `a ∈ R`. -/
+noncomputable def dickson : ℕ → polynomial R
+| 0       := 3 - k
+| 1       := X
+| (n + 2) := X * dickson (n + 1) - (C a) * dickson n
+
+@[simp] lemma dickson_zero : dickson k a 0 = 3 - k := rfl
+@[simp] lemma dickson_one : dickson k a 1 = X := rfl
+lemma dickson_two : dickson k a 2 = X ^ 2 - C a * (3 - k) :=
+by simp only [dickson, pow_two]
+@[simp] lemma dickson_add_two (n : ℕ) :
+  dickson k a (n + 2) = X * dickson k a (n + 1) - C a * dickson k a n :=
+by rw dickson
+
+lemma dickson_of_two_le {n : ℕ} (h : 2 ≤ n) :
+  dickson k a n = X * dickson k a (n - 1) - C a * dickson k a (n - 2) :=
+begin
+  obtain ⟨n, rfl⟩ := nat.exists_eq_add_of_le h,
+  rw add_comm,
+  exact dickson_add_two k a n
+end
+
+variables {R S k a}
+
+lemma map_dickson (f : R →+* S) :
+  ∀ (n : ℕ), map f (dickson k a n) = dickson k (f a) n
+| 0       := by simp only [dickson_zero, map_sub, map_nat_cast, bit1, bit0, map_add, map_one]
+| 1       := by simp only [dickson_one, map_X]
+| (n + 2) :=
+begin
+  simp only [dickson_add_two, map_sub, map_mul, map_X, map_C],
+  rw [map_dickson, map_dickson]
+end
+
+variable {R}
+
+@[simp] lemma dickson_two_zero :
+  ∀ (n : ℕ), dickson 2 (0 : R) n = X ^ n
+| 0       := by { simp only [dickson_zero, pow_zero], norm_num }
+| 1       := by simp only [dickson_one, pow_one]
+| (n + 2) :=
+begin
+  simp only [dickson_add_two, C_0, zero_mul, sub_zero],
+  rw [dickson_two_zero, pow_add X (n + 1) 1, mul_comm, pow_one]
+end
+
+end polynomial