refactor(ring_theory/polynomial/chebyshev): move lemmas around (#6510)

As discussed in #6501, split up the old file `ring_theory.polynomial.chebyshev.basic`, moving half its contents to `ring_theory.polynomial.chebyshev.defs` and the other half to `ring_theory.polynomial.chebyshev.dickson`.

src/analysis/special_functions/trigonometric.lean

@@ -6,7 +6,7 @@ Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin
 import analysis.special_functions.exp_log
 import data.set.intervals.infinite
 import algebra.quadratic_discriminant
-import ring_theory.polynomial.chebyshev.defs
+import ring_theory.polynomial.chebyshev
 import analysis.calculus.times_cont_diff
 
 /-!

src/ring_theory/polynomial/chebyshev/defs.lean → src/ring_theory/polynomial/chebyshev.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin
+Authors: Johan Commelin, Heather Macbeth
 -/
 
 import data.polynomial.derivative
@@ -13,24 +13,28 @@ import tactic.ring
 The Chebyshev polynomials are two families of polynomials indexed by `ℕ`,
 with integral coefficients.
 
-See the file `ring_theory.polynomial.chebyshev.basic` for more properties.
-
 ## Main definitions
 
 * `polynomial.chebyshev₁`: the Chebyshev polynomials of the first kind.
 * `polynomial.chebyshev₂`: the Chebyshev polynomials of the second kind.
 
-
 ## Main statements
 
 * The formal derivative of the Chebyshev polynomials of the first kind is a scalar multiple of the
   Chebyshev polynomials of the second kind.
+* `polynomial.mul_chebyshev₁`, the product of the `m`-th and `(m + k)`-th Chebyshev polynomials of
+  the first kind is the sum of the `(2 * m + k)`-th and `k`-th Chebyshev polynomials of the first
+  kind.
+* `polynomial.chebyshev₁_mul`, the `(m * n)`-th Chebyshev polynomial of the first kind is the
+  composition of the `m`-th and `n`-th Chebyshev polynomials of the first kind.
 
 ## Implementation details
 
-In this file we only give definitions and some very elementary simp-lemmas.
-This way, we can import this file in `analysis.special_functions.trigonometric`,
-and import that file in turn, in `ring_theory.polynomial.chebyshev.basic`.
+Since Chebyshev polynomials have interesting behaviour over the complex numbers and modulo `p`,
+we define them to have coefficients in an arbitrary commutative ring, even though
+technically `ℤ` would suffice.
+The benefit of allowing arbitrary coefficient rings, is that the statements afterwards are clean,
+and do not have `map (int.cast_ring_hom R)` interfering all the time.
 
 ## References
 
@@ -246,4 +250,63 @@ begin
             by ring,
 end
 
+variables (R)
+
+/-- The product of two Chebyshev polynomials is the sum of two other Chebyshev polynomials. -/
+lemma mul_chebyshev₁ :
+  ∀ m : ℕ, ∀ k,
+  2 * chebyshev₁ R m * chebyshev₁ R (m + k) = chebyshev₁ R (2 * m + k) + chebyshev₁ R k
+| 0 := by simp [two_mul, add_mul]
+| 1 := by simp [add_comm]
+| (m + 2) := begin
+  intros k,
+  -- clean up the `chebyshev₁` nat indices in the goal
+  suffices : 2 * chebyshev₁ R (m + 2) * chebyshev₁ R (m + k + 2)
+    = chebyshev₁ R (2 * m + k + 4) + chebyshev₁ R k,
+  { have h_nat₁ : 2 * (m + 2) + k = 2 * m + k + 4 := by ring,
+    have h_nat₂ : m + 2 + k = m + k + 2 := by simp [add_comm, add_assoc],
+    simpa [h_nat₁, h_nat₂] using this },
+  -- clean up the `chebyshev₁` nat indices in the inductive hypothesis applied to `m + 1` and
+  -- `k + 1`
+  have H₁ : 2 * chebyshev₁ R (m + 1) * chebyshev₁ R (m + k + 2)
+    = chebyshev₁ R (2 * m + k + 3) + chebyshev₁ R (k + 1),
+  { have h_nat₁ : m + 1 + (k + 1) = m + k + 2 := by ring,
+    have h_nat₂ : 2 * (m + 1) + (k + 1) = 2 * m + k + 3 := by ring,
+    simpa [h_nat₁, h_nat₂] using mul_chebyshev₁ (m + 1) (k + 1) },
+  -- clean up the `chebyshev₁` nat indices in the inductive hypothesis applied to `m` and `k + 2`
+  have H₂ : 2 * chebyshev₁ R m * chebyshev₁ R (m + k + 2)
+    = chebyshev₁ R (2 * m + k + 2) + chebyshev₁ R (k + 2),
+  { have h_nat₁ : 2 * m + (k + 2) = 2 * m + k + 2 := by simp [add_assoc],
+    have h_nat₂ : m + (k + 2) = m + k + 2 := by simp [add_assoc],
+    simpa [h_nat₁, h_nat₂] using mul_chebyshev₁ m (k + 2) },
+  -- state the `chebyshev₁` recurrence relation for a few useful indices
+  have h₁ := chebyshev₁_add_two R m,
+  have h₂ := chebyshev₁_add_two R (2 * m + k + 2),
+  have h₃ := chebyshev₁_add_two R k,
+  -- the desired identity is an appropriate linear combination of H₁, H₂, h₁, h₂, h₃
+  -- it would be really nice here to have a linear algebra tactic!!
+  apply_fun (λ p, 2 * X * p) at H₁,
+  apply_fun (λ p, 2 * chebyshev₁ R (m + k + 2) * p) at h₁,
+  have e₁ := congr (congr_arg has_add.add H₁) h₁,
+  have e₂ := congr (congr_arg has_sub.sub e₁) H₂,
+  have e₃ := congr (congr_arg has_sub.sub e₂) h₂,
+  have e₄ := congr (congr_arg has_sub.sub e₃) h₃,
+  rw ← sub_eq_zero at e₄ ⊢,
+  rw ← e₄,
+  ring,
+end
+
+/-- The `(m * n)`-th Chebyshev polynomial is the composition of the `m`-th and `n`-th -/
+lemma chebyshev₁_mul :
+  ∀ m : ℕ, ∀ n : ℕ, chebyshev₁ R (m * n) = (chebyshev₁ R m).comp (chebyshev₁ R n)
+| 0 := by simp
+| 1 := by simp
+| (m + 2) := begin
+  intros n,
+  have : 2 * chebyshev₁ R n * chebyshev₁ R ((m + 1) * n)
+    = chebyshev₁ R ((m + 2) * n) + chebyshev₁ R (m * n),
+  { convert mul_chebyshev₁ R n (m * n); ring },
+  simp [this, chebyshev₁_mul m, ← chebyshev₁_mul (m + 1)]
+end
+
 end polynomial

src/ring_theory/polynomial/chebyshev/basic.lean → src/ring_theory/polynomial/dickson.lean

@@ -1,105 +1,102 @@
 /-
-Copyright (c) 2020 Johan Commelin. All rights reserved.
+Copyright (c) 2021 Julian Kuelshammer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin, Heather Macbeth
+Authors: Julian Kuelshammer
 -/
 
-import ring_theory.polynomial.chebyshev.defs
-import ring_theory.polynomial.chebyshev.dickson
+import ring_theory.polynomial.chebyshev
 import ring_theory.localization
 import data.zmod.basic
 import algebra.invertible
 
+
 /-!
-# Chebyshev polynomials
+# 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`.
 
-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 definition
+
+* `polynomial.dickson`: the generalised Dickson polynomials.
 
 ## Main statements
 
-* `polynomial.mul_chebyshev₁`, the product of the `m`-th and `(m + k)`-th Chebyshev polynomials is
-  the sum of the `(2 * m + k)`-th and `k`-th Chebyshev polynomials
-* `polynomial.chebyshev₁_mul`, the `(m * n)`-th Chebyshev polynomial is the composition
-  of the `m`-th and `n`-th Chebyshev polynomials.
 * `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
+## References
 
-Since Chebyshev polynomials have interesting behaviour over the complex numbers and modulo `p`,
-we define them to have coefficients in an arbitrary commutative ring, even though
-technically `ℤ` would suffice.
-The benefit of allowing arbitrary coefficient rings, is that the statements afterwards are clean,
-and do not have `map (int.cast_ring_hom R)` interfering all the time.
+* [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]
-
-/-- The product of two Chebyshev polynomials is the sum of two other Chebyshev polynomials. -/
-lemma mul_chebyshev₁ :
-  ∀ m : ℕ, ∀ k,
-  2 * chebyshev₁ R m * chebyshev₁ R (m + k) = chebyshev₁ R (2 * m + k) + chebyshev₁ R k
-| 0 := by simp [two_mul, add_mul]
-| 1 := by simp [add_comm]
-| (m + 2) := begin
-  intros k,
-  -- clean up the `chebyshev₁` nat indices in the goal
-  suffices : 2 * chebyshev₁ R (m + 2) * chebyshev₁ R (m + k + 2)
-    = chebyshev₁ R (2 * m + k + 4) + chebyshev₁ R k,
-  { have h_nat₁ : 2 * (m + 2) + k = 2 * m + k + 4 := by ring,
-    have h_nat₂ : m + 2 + k = m + k + 2 := by simp [add_comm, add_assoc],
-    simpa [h_nat₁, h_nat₂] using this },
-  -- clean up the `chebyshev₁` nat indices in the inductive hypothesis applied to `m + 1` and
-  -- `k + 1`
-  have H₁ : 2 * chebyshev₁ R (m + 1) * chebyshev₁ R (m + k + 2)
-    = chebyshev₁ R (2 * m + k + 3) + chebyshev₁ R (k + 1),
-  { have h_nat₁ : m + 1 + (k + 1) = m + k + 2 := by ring,
-    have h_nat₂ : 2 * (m + 1) + (k + 1) = 2 * m + k + 3 := by ring,
-    simpa [h_nat₁, h_nat₂] using mul_chebyshev₁ (m + 1) (k + 1) },
-  -- clean up the `chebyshev₁` nat indices in the inductive hypothesis applied to `m` and `k + 2`
-  have H₂ : 2 * chebyshev₁ R m * chebyshev₁ R (m + k + 2)
-    = chebyshev₁ R (2 * m + k + 2) + chebyshev₁ R (k + 2),
-  { have h_nat₁ : 2 * m + (k + 2) = 2 * m + k + 2 := by simp [add_assoc],
-    have h_nat₂ : m + (k + 2) = m + k + 2 := by simp [add_assoc],
-    simpa [h_nat₁, h_nat₂] using mul_chebyshev₁ m (k + 2) },
-  -- state the `chebyshev₁` recurrence relation for a few useful indices
-  have h₁ := chebyshev₁_add_two R m,
-  have h₂ := chebyshev₁_add_two R (2 * m + k + 2),
-  have h₃ := chebyshev₁_add_two R k,
-  -- the desired identity is an appropriate linear combination of H₁, H₂, h₁, h₂, h₃
-  -- it would be really nice here to have a linear algebra tactic!!
-  apply_fun (λ p, 2 * X * p) at H₁,
-  apply_fun (λ p, 2 * chebyshev₁ R (m + k + 2) * p) at h₁,
-  have e₁ := congr (congr_arg has_add.add H₁) h₁,
-  have e₂ := congr (congr_arg has_sub.sub e₁) H₂,
-  have e₃ := congr (congr_arg has_sub.sub e₂) h₂,
-  have e₄ := congr (congr_arg has_sub.sub e₃) h₃,
-  rw ← sub_eq_zero at e₄ ⊢,
-  rw ← e₄,
-  ring,
+
+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
 
-/-- The `(m * n)`-th Chebyshev polynomial is the composition of the `m`-th and `n`-th -/
-lemma chebyshev₁_mul :
-  ∀ m : ℕ, ∀ n : ℕ, chebyshev₁ R (m * n) = (chebyshev₁ R m).comp (chebyshev₁ R n)
-| 0 := by simp
-| 1 := by simp
-| (m + 2) := begin
-  intros n,
-  have : 2 * chebyshev₁ R n * chebyshev₁ R ((m + 1) * n)
-    = chebyshev₁ R ((m + 2) * n) + chebyshev₁ R (m * n),
-  { convert mul_chebyshev₁ R n (m * n); ring },
-  simp [this, chebyshev₁_mul m, ← chebyshev₁_mul (m + 1)]
+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
 
 section dickson