From 3309ce274362523bd5efacb14b78097e01f076ee Mon Sep 17 00:00:00 2001 From: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com> Date: Wed, 3 Mar 2021 10:36:52 +0000 Subject: [PATCH] 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`. --- .../special_functions/trigonometric.lean | 2 +- .../{chebyshev/defs.lean => chebyshev.lean} | 77 +++++++++- .../polynomial/chebyshev/default.lean | 1 - .../polynomial/chebyshev/dickson.lean | 91 ----------- .../{chebyshev/basic.lean => dickson.lean} | 143 +++++++++--------- 5 files changed, 141 insertions(+), 173 deletions(-) rename src/ring_theory/polynomial/{chebyshev/defs.lean => chebyshev.lean} (74%) delete mode 100644 src/ring_theory/polynomial/chebyshev/default.lean delete mode 100644 src/ring_theory/polynomial/chebyshev/dickson.lean rename src/ring_theory/polynomial/{chebyshev/basic.lean => dickson.lean} (65%) diff --git a/src/analysis/special_functions/trigonometric.lean b/src/analysis/special_functions/trigonometric.lean index 79909f586a469..2894d326a8c19 100644 --- a/src/analysis/special_functions/trigonometric.lean +++ b/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 /-! diff --git a/src/ring_theory/polynomial/chebyshev/defs.lean b/src/ring_theory/polynomial/chebyshev.lean similarity index 74% rename from src/ring_theory/polynomial/chebyshev/defs.lean rename to src/ring_theory/polynomial/chebyshev.lean index c4418ed557c10..981d5f24016af 100644 --- a/src/ring_theory/polynomial/chebyshev/defs.lean +++ b/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 diff --git a/src/ring_theory/polynomial/chebyshev/default.lean b/src/ring_theory/polynomial/chebyshev/default.lean deleted file mode 100644 index 05ad32d9f4d11..0000000000000 --- a/src/ring_theory/polynomial/chebyshev/default.lean +++ /dev/null @@ -1 +0,0 @@ -import ring_theory.polynomial.chebyshev.basic diff --git a/src/ring_theory/polynomial/chebyshev/dickson.lean b/src/ring_theory/polynomial/chebyshev/dickson.lean deleted file mode 100644 index 54c1b4bff9eda..0000000000000 --- a/src/ring_theory/polynomial/chebyshev/dickson.lean +++ /dev/null @@ -1,91 +0,0 @@ -/- -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 diff --git a/src/ring_theory/polynomial/chebyshev/basic.lean b/src/ring_theory/polynomial/dickson.lean similarity index 65% rename from src/ring_theory/polynomial/chebyshev/basic.lean rename to src/ring_theory/polynomial/dickson.lean index 5245b8e2cd205..fae3d62422f0f 100644 --- a/src/ring_theory/polynomial/chebyshev/basic.lean +++ b/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