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').