From 9593a645885b383cc56d09543a34af0c44c695bc Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Wed, 2 Oct 2024 05:35:43 +0000 Subject: [PATCH] =?UTF-8?q?feat(NumberTheory/{GaussSum|JacobiSum/Basic}):?= =?UTF-8?q?=20formula=20for=20g(=CF=87)^ord(=CF=87)=20(#17336)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We continue with adding properties of Gauss and Jacobi sums. This PR shows that `g(χ)^n = χ(-1) * #F * J(χ,χ) * J(χ,χ²) * ... * J(χ,χⁿ⁻²)` when `χ` is a multiplicative character on the finite field `F` of order `n` (and with values in a domain). --- Mathlib/NumberTheory/GaussSum.lean | 22 ++++++++++++-- Mathlib/NumberTheory/JacobiSum/Basic.lean | 35 +++++++++++++++++++++++ 2 files changed, 55 insertions(+), 2 deletions(-) diff --git a/Mathlib/NumberTheory/GaussSum.lean b/Mathlib/NumberTheory/GaussSum.lean index 5140078baa06e..6af4f9545d5ff 100644 --- a/Mathlib/NumberTheory/GaussSum.lean +++ b/Mathlib/NumberTheory/GaussSum.lean @@ -97,8 +97,15 @@ lemma gaussSum_mul {R : Type u} [CommRing R] [Fintype R] {R' : Type v} [CommRing · exact fun a _ ↦ by rw [add_sub_cancel_right, add_comm] rw [sum_congr rfl fun x _ ↦ sum_eq x, sum_comm] --- In the following, we need `R` to be a finite field and `R'` to be a domain. -variable {R : Type u} [Field R] [Fintype R] {R' : Type v} [CommRing R'] [IsDomain R'] +-- In the following, we need `R` to be a finite field. +variable {R : Type u} [Field R] [Fintype R] {R' : Type v} [CommRing R'] + +lemma mul_gaussSum_inv_eq_gaussSum (χ : MulChar R R') (ψ : AddChar R R') : + χ (-1) * gaussSum χ ψ⁻¹ = gaussSum χ ψ := by + rw [ψ.inv_mulShift, ← Units.coe_neg_one] + exact gaussSum_mulShift χ ψ (-1) + +variable [IsDomain R'] -- From now on, `R'` needs to be a domain. -- A helper lemma for `gaussSum_mul_gaussSum_eq_card` below -- Is this useful enough in other contexts to be public? @@ -130,6 +137,17 @@ theorem gaussSum_mul_gaussSum_eq_card {χ : MulChar R R'} (hχ : χ ≠ 1) {ψ : rw [Finset.sum_ite_eq' Finset.univ (1 : R)] simp only [Finset.mem_univ, map_one, one_mul, if_true] +/-- If `χ` is a multiplicative character of order `n` on a finite field `F`, +then `g(χ) * g(χ^(n-1)) = χ(-1)*#F` -/ +lemma gaussSum_mul_gaussSum_pow_orderOf_sub_one {χ : MulChar R R'} {ψ : AddChar R R'} + (hχ : χ ≠ 1) (hψ : ψ.IsPrimitive) : + gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ = χ (-1) * Fintype.card R := by + have h : χ ^ (orderOf χ - 1) = χ⁻¹ := by + refine (inv_eq_of_mul_eq_one_right ?_).symm + rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos χ.orderOf_pos, pow_orderOf_eq_one] + rw [h, ← mul_gaussSum_inv_eq_gaussSum χ⁻¹, mul_left_comm, gaussSum_mul_gaussSum_eq_card hχ hψ, + MulChar.inv_apply', inv_neg_one] + /-- The Gauss sum of a nontrivial character on a finite field does not vanish. -/ lemma gaussSum_ne_zero_of_nontrivial (h : (Fintype.card R : R') ≠ 0) {χ : MulChar R R'} (hχ : χ ≠ 1) {ψ : AddChar R R'} (hψ : ψ.IsPrimitive) : diff --git a/Mathlib/NumberTheory/JacobiSum/Basic.lean b/Mathlib/NumberTheory/JacobiSum/Basic.lean index 1859c852cef47..f9a173578aa98 100644 --- a/Mathlib/NumberTheory/JacobiSum/Basic.lean +++ b/Mathlib/NumberTheory/JacobiSum/Basic.lean @@ -298,3 +298,38 @@ lemma exists_jacobiSum_eq_neg_one_add [DecidableEq F] {n : ℕ} (hn : 2 < n) {χ ring end image + +section GaussSum + +variable {F R : Type*} [Fintype F] [Field F] [CommRing R] [IsDomain R] + +lemma gaussSum_pow_eq_prod_jacobiSum_aux (χ : MulChar F R) (ψ : AddChar F R) {n : ℕ} + (hn₁ : 0 < n) (hn₂ : n < orderOf χ) : + gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j) := by + induction n, hn₁ using Nat.le_induction with + | base => simp only [pow_one, le_refl, Ico_eq_empty_of_le, prod_empty, mul_one] + | succ n hn ih => + specialize ih <| lt_trans (Nat.lt_succ_self n) hn₂ + have gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ = + jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ := by + have hχn : χ * (χ ^ n) ≠ 1 := + pow_succ' χ n ▸ pow_ne_one_of_lt_orderOf n.add_one_ne_zero hn₂ + rw [mul_comm, ← jacobiSum_mul_nontrivial hχn, mul_comm, ← pow_succ'] + apply_fun (· * gaussSum χ ψ) at ih + rw [mul_right_comm, ← pow_succ, gauss_rw] at ih + rw [ih, Finset.prod_Ico_succ_top hn, mul_rotate, mul_assoc] + +/-- If `χ` is a multiplicative character of order `n ≥ 2` on a finite field `F`, +then `g(χ)^n = χ(-1) * #F * J(χ,χ) * J(χ,χ²) * ... * J(χ,χⁿ⁻²)`. -/ +theorem gaussSum_pow_eq_prod_jacobiSum {χ : MulChar F R} {ψ : AddChar F R} (hχ : 2 ≤ orderOf χ) + (hψ : ψ.IsPrimitive) : + gaussSum χ ψ ^ orderOf χ = + χ (-1) * Fintype.card F * ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i) := by + have := gaussSum_pow_eq_prod_jacobiSum_aux χ ψ (n := orderOf χ - 1) (by omega) (by omega) + apply_fun (gaussSum χ ψ * ·) at this + rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos (by omega)] at this + have hχ₁ : χ ≠ 1 := + fun h ↦ ((orderOf_one (G := MulChar F R) ▸ h ▸ hχ).trans_lt Nat.one_lt_two).false + rw [this, ← mul_assoc, gaussSum_mul_gaussSum_pow_orderOf_sub_one hχ₁ hψ] + +end GaussSum