feat(NumberTheory/{GaussSum|JacobiSum/Basic}): formula for g(χ)^ord(χ) (

#17336)

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

@@ -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) :

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