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.

Main statements

• 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_charP, 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.

References

• R. Lidl, G. L. Mullen and G. Turnwald, Dickson polynomials

TODO

• Redefine dickson in terms of LinearRecurrence.
• 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 def Polynomial.dickson {R : Type u_1} [CommRing R] (k : ℕ) (a : R) : ℕ → Polynomial R

dickson is the n-th (generalised) Dickson polynomial of the k-th kind associated to the element a ∈ R.

Equations

• Polynomial.dickson k a 0 = 3 - ↑k
• Polynomial.dickson k a 1 = Polynomial.X
• Polynomial.dickson k a n.succ.succ = Polynomial.X * Polynomial.dickson k a (n + 1) - Polynomial.C a * Polynomial.dickson k a n

@[simp]

theorem Polynomial.dickson_zero {R : Type u_1} [CommRing R] (k : ℕ) (a : R) : Polynomial.dickson k a 0 = 3 - ↑k

@[simp]

theorem Polynomial.dickson_one {R : Type u_1} [CommRing R] (k : ℕ) (a : R) : Polynomial.dickson k a 1 = Polynomial.X

theorem Polynomial.dickson_two {R : Type u_1} [CommRing R] (k : ℕ) (a : R) : Polynomial.dickson k a 2 = Polynomial.X ^ 2 - Polynomial.C a * (3 - ↑k)

@[simp]

theorem Polynomial.dickson_add_two {R : Type u_1} [CommRing R] (k : ℕ) (a : R) (n : ℕ) : Polynomial.dickson k a (n + 2) = Polynomial.X * Polynomial.dickson k a (n + 1) - Polynomial.C a * Polynomial.dickson k a n

theorem Polynomial.dickson_of_two_le {R : Type u_1} [CommRing R] (k : ℕ) (a : R) {n : ℕ} (h : 2 ≤ n) : Polynomial.dickson k a n = Polynomial.X * Polynomial.dickson k a (n - 1) - Polynomial.C a * Polynomial.dickson k a (n - 2)

theorem Polynomial.map_dickson {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {k : ℕ} {a : R} (f : R →+* S) (n : ℕ) : Polynomial.map f (Polynomial.dickson k a n) = Polynomial.dickson k (f a) n

@[simp]

theorem Polynomial.dickson_two_zero {R : Type u_1} [CommRing R] (n : ℕ) : Polynomial.dickson 2 0 n = Polynomial.X ^ n

A Lambda structure on ℤ[X]

Mathlib doesn't currently know what a Lambda ring is. But once it does, we can endow ℤ[X] with a Lambda structure in terms of the dickson 1 1 polynomials defined below. There is exactly one other Lambda structure on ℤ[X] in terms of binomial polynomials.

theorem Polynomial.dickson_one_one_eval_add_inv {R : Type u_1} [CommRing R] (x y : R) (h : x * y = 1) (n : ℕ) : Polynomial.eval (x + y) (Polynomial.dickson 1 1 n) = x ^ n + y ^ n

theorem Polynomial.dickson_one_one_eq_chebyshev_C (R : Type u_1) [CommRing R] (n : ℕ) : Polynomial.dickson 1 1 n = Polynomial.Chebyshev.C R ↑n

theorem Polynomial.dickson_one_one_eq_chebyshev_T (R : Type u_1) [CommRing R] [Invertible 2] (n : ℕ) : Polynomial.dickson 1 1 n = 2 * (Polynomial.Chebyshev.T R ↑n).comp (Polynomial.C ⅟2 * Polynomial.X)

theorem Polynomial.chebyshev_T_eq_dickson_one_one (R : Type u_1) [CommRing R] [Invertible 2] (n : ℕ) : Polynomial.Chebyshev.T R ↑n = Polynomial.C ⅟2 * (Polynomial.dickson 1 1 n).comp (2 * Polynomial.X)

theorem Polynomial.dickson_two_one_eq_chebyshev_S (R : Type u_1) [CommRing R] (n : ℕ) : Polynomial.dickson 2 1 n = Polynomial.Chebyshev.S R ↑n

theorem Polynomial.dickson_two_one_eq_chebyshev_U (R : Type u_1) [CommRing R] [Invertible 2] (n : ℕ) : Polynomial.dickson 2 1 n = (Polynomial.Chebyshev.U R ↑n).comp (Polynomial.C ⅟2 * Polynomial.X)

theorem Polynomial.chebyshev_U_eq_dickson_two_one (R : Type u_1) [CommRing R] (n : ℕ) : Polynomial.Chebyshev.U R ↑n = (Polynomial.dickson 2 1 n).comp (2 * Polynomial.X)

theorem Polynomial.dickson_one_one_mul (R : Type u_1) [CommRing R] (m n : ℕ) : Polynomial.dickson 1 1 (m * n) = (Polynomial.dickson 1 1 m).comp (Polynomial.dickson 1 1 n)

The (m * n)-th Dickson polynomial of the first kind is the composition of the m-th and n-th.

theorem Polynomial.dickson_one_one_comp_comm (R : Type u_1) [CommRing R] (m n : ℕ) : (Polynomial.dickson 1 1 m).comp (Polynomial.dickson 1 1 n) = (Polynomial.dickson 1 1 n).comp (Polynomial.dickson 1 1 m)

theorem Polynomial.dickson_one_one_zmod_p (p : ℕ) [Fact (Nat.Prime p)] : Polynomial.dickson 1 1 p = Polynomial.X ^ p

theorem Polynomial.dickson_one_one_charP (R : Type u_1) [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] : Polynomial.dickson 1 1 p = Polynomial.X ^ p