Jacobi Sums

This file defines the Jacobi sum of two multiplicative characters χ and ψ on a finite commutative ring R with values in another commutative ring R':

jacobiSum χ ψ = ∑ x : R, χ x * ψ (1 - x)

(see jacobiSum) and provides some basic results and API lemmas on Jacobi sums.

References

We essentially follow

• [K. Ireland, M. Rosen, A classical introduction to modern number theory (Section 8.3)][IrelandRosen1990]

but generalize where appropriate.

This is based on Lean code written as part of the bachelor's thesis of Alexander Spahl.

Jacobi sums: definition and first properties

def jacobiSum {R : Type u_1} {R' : Type u_2} [CommRing R] [Fintype R] [CommRing R'] (χ : MulChar R R') (ψ : MulChar R R') : R'

The Jacobi sum of two multiplicative characters on a finite commutative ring.

Equations

• jacobiSum χ ψ = ∑ x : R, χ x * ψ (1 - x)

theorem jacobiSum_comm {R : Type u_1} {R' : Type u_2} [CommRing R] [Fintype R] [CommRing R'] (χ : MulChar R R') (ψ : MulChar R R') : jacobiSum χ ψ = jacobiSum ψ χ

theorem jacobiSum_ringHomComp {R : Type u_1} {R' : Type u_2} [CommRing R] [Fintype R] [CommRing R'] {R'' : Type u_3} [CommRing R''] (χ : MulChar R R') (ψ : MulChar R R') (f : R' →+* R'') : jacobiSum (χ.ringHomComp f) (ψ.ringHomComp f) = f (jacobiSum χ ψ)

The Jacobi sum is compatible with ring homomorphisms.

Jacobi sums over finite fields

theorem jacobiSum_eq_sum_sdiff {F : Type u_1} {R : Type u_2} [CommRing F] [Nontrivial F] [Fintype F] [DecidableEq F] [CommRing R] (χ : MulChar F R) (ψ : MulChar F R) : jacobiSum χ ψ = ∑ x ∈ Finset.univ \ {0, 1}, χ x * ψ (1 - x)

The Jacobi sum of two multiplicative characters on a nontrivial finite commutative ring F can be written as a sum over F \ {0,1}.

theorem jacobiSum_trivial_trivial {F : Type u_1} {R : Type u_2} [Field F] [Fintype F] [CommRing R] : jacobiSum (MulChar.trivial F R) (MulChar.trivial F R) = ↑(Fintype.card F) - 2

The Jacobi sum of twice the trivial multiplicative character on a finite field F equals #F-2.

theorem jacobiSum_one_one {F : Type u_1} {R : Type u_2} [Field F] [Fintype F] [CommRing R] : jacobiSum 1 1 = ↑(Fintype.card F) - 2

If 1 is the trivial multiplicative character on a finite field F, then J(1,1) = #F-2.

theorem jacobiSum_one_nontrivial {F : Type u_1} {R : Type u_2} [Field F] [Fintype F] [CommRing R] [IsDomain R] {χ : MulChar F R} (hχ : χ ≠ 1) : jacobiSum 1 χ = -1

If χ is a nontrivial multiplicative character on a finite field F, then J(1,χ) = -1.

theorem jacobiSum_nontrivial_inv {F : Type u_1} {R : Type u_2} [Field F] [Fintype F] [CommRing R] [IsDomain R] {χ : MulChar F R} (hχ : χ ≠ 1) : jacobiSum χ χ⁻¹ = -χ (-1)

If χ is a nontrivial multiplicative character on a finite field F, then J(χ,χ⁻¹) = -χ(-1).

theorem jacobiSum_mul_nontrivial {F : Type u_1} {R : Type u_2} [Field F] [Fintype F] [CommRing R] [IsDomain R] {χ : MulChar F R} {φ : MulChar F R} (h : χ * φ ≠ 1) (ψ : AddChar F R) : gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ

If χ and φ are multiplicative characters on a finite field F such that χφ is nontrivial, then g(χφ) * J(χ,φ) = g(χ) * g(φ).

theorem jacobiSum_eq_gaussSum_mul_gaussSum_div_gaussSum {F : Type u_1} {F' : Type u_2} [Fintype F] [Field F] [Field F'] (h : ↑(Fintype.card F) ≠ 0) {χ : MulChar F F'} {φ : MulChar F F'} (hχφ : χ * φ ≠ 1) {ψ : AddChar F F'} (hψ : ψ.IsPrimitive) : jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ / gaussSum (χ * φ) ψ

If χ and φ are multiplicative characters on a finite field F with values in another field F' and such that χφ is nontrivial, then J(χ,φ) = g(χ) * g(φ) / g(χφ).

theorem jacobiSum_mul_jacobiSum_inv {F : Type u_1} {F' : Type u_2} [Fintype F] [Field F] [Field F'] (h : ringChar F' ≠ ringChar F) {χ : MulChar F F'} {φ : MulChar F F'} (hχ : χ ≠ 1) (hφ : φ ≠ 1) (hχφ : χ * φ ≠ 1) : jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = ↑(Fintype.card F)

If χ and φ are multiplicative characters on a finite field F with values in another field F' such that χ, φ and χφ are all nontrivial and char F' ≠ char F, then J(χ,φ) * J(χ⁻¹,φ⁻¹) = #F (in F').

theorem jacobiSum_mem_algebraAdjoin_of_pow_eq_one {F : Type u_1} {R : Type u_2} [Fintype F] [Field F] [CommRing R] [IsDomain R] {n : ℕ} (hn : n ≠ 0) {χ : MulChar F R} {φ : MulChar F R} (hχ : χ ^ n = 1) (hφ : φ ^ n = 1) {μ : R} (hμ : IsPrimitiveRoot μ n) : jacobiSum χ φ ∈ Algebra.adjoin ℤ {μ}

If χ and φ are multiplicative characters on a finite field F satisfying χ^n = φ^n = 1 and with values in an integral domain R, and μ is a primitive nth root of unity in R, then the Jacobi sum J(χ,φ) is in ℤ[μ] ⊆ R.

theorem exists_jacobiSum_eq_neg_one_add {F : Type u_1} {R : Type u_2} [Fintype F] [Field F] [CommRing R] [IsDomain R] {n : ℕ} (hn : 2 < n) {χ : MulChar F R} {ψ : MulChar F R} {μ : R} (hχ : χ ^ n = 1) (hψ : ψ ^ n = 1) (hn' : n ∣ Fintype.card F - 1) (hμ : IsPrimitiveRoot μ n) : ∃ z ∈ Algebra.adjoin ℤ {μ}, jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2

If χ and ψ are multiplicative characters of order dividing n on a finite field F with values in an integral domain R and μ is a primitive nth root of unity in R, then J(χ,ψ) = -1 + z*(μ - 1)^2 for some z ∈ ℤ[μ] ⊆ R. (We assume that #F ≡ 1 mod n.) Note that we do not state this as a divisibility in R, as this would give a weaker statement.

theorem gaussSum_pow_eq_prod_jacobiSum_aux {F : Type u_1} {R : Type u_2} [Fintype F] [Field F] [CommRing R] [IsDomain R] (χ : MulChar F R) (ψ : AddChar F R) {n : ℕ} (hn₁ : 0 < n) (hn₂ : n < orderOf χ) : gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Finset.Ico 1 n, jacobiSum χ (χ ^ j)

theorem gaussSum_pow_eq_prod_jacobiSum {F : Type u_1} {R : Type u_2} [Fintype F] [Field F] [CommRing R] [IsDomain R] {χ : MulChar F R} {ψ : AddChar F R} (hχ : 2 ≤ orderOf χ) (hψ : ψ.IsPrimitive) : gaussSum χ ψ ^ orderOf χ = χ (-1) * ↑(Fintype.card F) * ∏ i ∈ Finset.Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)

If χ is a multiplicative character of order n ≥ 2 on a finite field F, then g(χ)^n = χ(-1) * #F * J(χ,χ) * J(χ,χ²) * ... * J(χ,χⁿ⁻²).