Documentation

Mathlib.NumberTheory.JacobiSum.Basic

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

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 #

source
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
Instances For
    source
    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 ψ χ
    source
    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 #

    source
    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}.

    source
    theorem jacobiSum_trivial_trivial {F : Type u_1} {R : Type u_2} [Field F] [Fintype F] [DecidableEq 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.

    source
    theorem jacobiSum_one_one {F : Type u_1} {R : Type u_2} [Field F] [Fintype F] [DecidableEq 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.

    source
    theorem jacobiSum_one_nontrivial {F : Type u_1} {R : Type u_2} [Field F] [Fintype F] [DecidableEq 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.

    source
    theorem jacobiSum_nontrivial_inv {F : Type u_1} {R : Type u_2} [Field F] [Fintype F] [DecidableEq 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).

    source
    theorem jacobiSum_mul_nontrivial {F : Type u_1} {R : Type u_2} [Field F] [Fintype F] [DecidableEq 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(φ).