Dickson permutation lemmas

Mathlib already has the Dickson polynomials Polynomial.dickson 1 1 m together with

• Polynomial.dickson_one_one_eval_add_inv : x * y = 1 → (dickson 1 1 n).eval (x + y) = x ^ n + y ^ n
• Polynomial.dickson_one_one_mul : dickson 1 1 (m * n) = (dickson 1 1 m).comp (dickson 1 1 n)
• Nat.pow_sub_one_gcd_pow_sub_one

What it lacks, and what is proved here, is the permutation criterion D_m permutes a finite field K as soon as gcd(m, |K|² - 1) = 1, its two arithmetic instances for the exponents 2^k - 1 and (2^k+1)/3, and the consequence that D_(3h) and D_3 have the same value distribution whenever D_h is a permutation.

Auxiliary lemmas for the permutation criterion

theorem KasamiCyclicAdditive.exists_add_inv_eq (K : Type u_1) [Field K] (x : K) : ∃ (u : AlgebraicClosure K), u ≠ 0 ∧ u + u⁻¹ = (algebraMap K (AlgebraicClosure K)) x

Every element x of a finite field K is of the form u + u⁻¹ for a nonzero u in the algebraic closure of K: take u to be a root of Y² - x*Y + 1.

theorem KasamiCyclicAdditive.pow_card_sq_eq_self (K : Type u_1) [Field K] [Fintype K] (x : K) (u : AlgebraicClosure K) (hu0 : u ≠ 0) (hx : u + u⁻¹ = (algebraMap K (AlgebraicClosure K)) x) : u ^ Fintype.card K ^ 2 = u

If u + u⁻¹ lies in the finite field K (of cardinality q), then u lies in a quadratic extension of K, i.e. u ^ (q ^ 2) = u. Proof: the q-power map is a ring homomorphism fixing K, so it sends the root u of Y² - x*Y + 1 to a root, and the two roots are u and u⁻¹.

theorem KasamiCyclicAdditive.pow_card_sq_sub_one_eq_one (K : Type u_1) [Field K] [Fintype K] (x : K) {u : AlgebraicClosure K} (hu0 : u ≠ 0) (hux : u + u⁻¹ = (algebraMap K (AlgebraicClosure K)) x) : u ^ (Fintype.card K ^ 2 - 1) = 1

An element of the quadratic extension with u + u⁻¹ in K is an (q² - 1)-th root of unity.

theorem KasamiCyclicAdditive.dickson_eval_eq_pow_add_inv_pow (K : Type u_1) [Field K] (x : K) {u : AlgebraicClosure K} (hu0 : u ≠ 0) (hux : u + u⁻¹ = (algebraMap K (AlgebraicClosure K)) x) (m : ℕ) : (algebraMap K (AlgebraicClosure K)) (Polynomial.eval x (Polynomial.dickson 1 1 m)) = u ^ m + u⁻¹ ^ m

Dickson evaluation in the quadratic extension: D_m(u + u⁻¹) = u^m + u^(-m).

The permutation criterion

theorem KasamiCyclicAdditive.dickson_bijective {K : Type u_1} [Field K] [Fintype K] {m : ℕ} (hm : m.Coprime (Fintype.card K ^ 2 - 1)) : Function.Bijective fun (x : K) => Polynomial.eval x (Polynomial.dickson 1 1 m)

D_m permutes a finite field K as soon as m is coprime to |K|² - 1.

Proof sketch. Let q = |K| and let L be an extension of K with q² elements. Every x : K is u + u⁻¹ for some u : Lˣ: the polynomial Y² - x*Y + 1 has its roots in L, and their product is 1. By dickson_one_one_eval_add_inv, D_m(u + u⁻¹) = u^m + u^(-m). Coprimality of m with q² - 1 = |Lˣ| makes u ↦ u^m a bijection of Lˣ commuting with u ↦ u⁻¹, hence a bijection of the set of unordered pairs {u, u⁻¹}, which is exactly K under u ↦ u + u⁻¹. Since K is finite it is enough to prove injectivity.

The two arithmetic instances

theorem KasamiCyclicAdditive.coprime_two_pow_sub_one {k n : ℕ} (hkn : k.Coprime (2 * n)) : (2 ^ k - 1).Coprime (2 ^ (2 * n) - 1)

2^k - 1 is coprime to 2^(2n) - 1 when gcd(k, 2n) = 1.

Immediate from Nat.pow_sub_one_gcd_pow_sub_one: gcd(2^a - 1, 2^b - 1) = 2^gcd(a,b) - 1, here 2^1 - 1 = 1.

theorem KasamiCyclicAdditive.coprime_third_of_two_pow_add_one {k n h : ℕ} (hkn : k.Coprime n) (hh : 3 * h = 2 ^ k + 1) (h3 : ¬3 ∣ h) : h.Coprime (2 ^ (2 * n) - 1)

With 3 * h = 2^k + 1, gcd(k, n) = 1 and 3 ∤ h, the number h is coprime to 2^(2n) - 1.

This is where the normalisation k ≢ 3 (mod 6) enters: that condition is exactly 3 ∤ h.

Proof. 2^k + 1 divides 2^(2k) - 1, and by Nat.pow_sub_one_gcd_pow_sub_one, gcd(2^(2k) - 1, 2^(2n) - 1) = 2^(2 gcd(k,n)) - 1 = 3. So gcd(2^k + 1, 2^(2n) - 1) divides 3; it is 3, since 3 divides both. Hence gcd(3h, 2^(2n) - 1) = 3, so d := gcd(h, 2^(2n) - 1) divides 3 and is 1 or 3. It is 3 only if 3 ∣ h, which is excluded.

The payoff

theorem KasamiCyclicAdditive.sum_dickson_eq_cubic {K : Type u_1} [Field K] [Fintype K] {M : Type u_2} [AddCommMonoid M] {e h : ℕ} (he : e = 3 * h) (hh : h.Coprime (Fintype.card K ^ 2 - 1)) (f : K → M) : ∑ x : K, f (Polynomial.eval x (Polynomial.dickson 1 1 e)) = ∑ x : K, f (Polynomial.eval x (Polynomial.dickson 1 1 3))

If e = 3h and D_h permutes K, then D_e and D_3 have the same value distribution, in the strong sense that they give equal sums against any function.

dickson_one_one_mul gives D_e = D_3 ∘ D_h, so the substitution y = D_h x — a bijection by dickson_bijective — turns one sum into the other.