Documentation

Mathlib.NumberTheory.GaussSum

Gauss sums #

We define the Gauss sum associated to a multiplicative and an additive character of a finite field and prove some results about them.

Main definition #

Let R be a finite commutative ring and let R' be another commutative ring. If χ is a multiplicative character R → R' (type MulChar R R') and ψ is an additive character R → R' (type AddChar R R', which abbreviates (Multiplicative R) →* R'), then the Gauss sum of χ and ψ is ∑ a, χ a * ψ a.

Main results #

Some important results are as follows.

This machinery can be used to derive (a generalization of) the Law of Quadratic Reciprocity.

Tags #

additive character, multiplicative character, Gauss sum

Definition and first properties #

def gaussSum {R : Type u} [CommRing R] [Fintype R] {R' : Type v} [CommRing R'] (χ : MulChar R R') (ψ : AddChar R R') :
R'

Definition of the Gauss sum associated to a multiplicative and an additive character.

Equations
Instances For
    theorem gaussSum_mulShift {R : Type u} [CommRing R] [Fintype R] {R' : Type v} [CommRing R'] (χ : MulChar R R') (ψ : AddChar R R') (a : Rˣ) :
    χ a * gaussSum χ (ψ.mulShift a) = gaussSum χ ψ

    Replacing ψ by mulShift ψ a and multiplying the Gauss sum by χ a does not change it.

    The product of two Gauss sums #

    theorem gaussSum_mul {R : Type u} [CommRing R] [Fintype R] {R' : Type v} [CommRing R'] (χ : MulChar R R') (φ : MulChar R R') (ψ : AddChar R R') :
    gaussSum χ ψ * gaussSum φ ψ = t : R, x : R, χ x * φ (t - x) * ψ t

    A formula for the product of two Gauss sums with the same additive character.

    theorem mul_gaussSum_inv_eq_gaussSum {R : Type u} [Field R] [Fintype R] {R' : Type v} [CommRing R'] (χ : MulChar R R') (ψ : AddChar R R') :
    χ (-1) * gaussSum χ ψ⁻¹ = gaussSum χ ψ
    theorem gaussSum_mul_gaussSum_eq_card {R : Type u} [Field R] [Fintype R] {R' : Type v} [CommRing R'] [IsDomain R'] {χ : MulChar R R'} (hχ : χ 1) {ψ : AddChar R R'} (hψ : ψ.IsPrimitive) :

    We have gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = Fintype.card R when χ is nontrivial and ψ is primitive (and R is a field).

    theorem gaussSum_mul_gaussSum_pow_orderOf_sub_one {R : Type u} [Field R] [Fintype R] {R' : Type v} [CommRing R'] [IsDomain R'] {χ : MulChar R R'} {ψ : AddChar R R'} (hχ : χ 1) (hψ : ψ.IsPrimitive) :
    gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ = χ (-1) * (Fintype.card R)

    If χ is a multiplicative character of order n on a finite field F, then g(χ) * g(χ^(n-1)) = χ(-1)*#F

    theorem gaussSum_ne_zero_of_nontrivial {R : Type u} [Field R] [Fintype R] {R' : Type v} [CommRing R'] [IsDomain R'] (h : (Fintype.card R) 0) {χ : MulChar R R'} (hχ : χ 1) {ψ : AddChar R R'} (hψ : ψ.IsPrimitive) :
    gaussSum χ ψ 0

    The Gauss sum of a nontrivial character on a finite field does not vanish.

    theorem gaussSum_sq {R : Type u} [Field R] [Fintype R] {R' : Type v} [CommRing R'] [IsDomain R'] {χ : MulChar R R'} (hχ₁ : χ 1) (hχ₂ : χ.IsQuadratic) {ψ : AddChar R R'} (hψ : ψ.IsPrimitive) :
    gaussSum χ ψ ^ 2 = χ (-1) * (Fintype.card R)

    When χ is a nontrivial quadratic character, then the square of gaussSum χ ψ is χ(-1) times the cardinality of R.

    Gauss sums and Frobenius #

    theorem gaussSum_frob {R : Type u} [CommRing R] [Fintype R] {R' : Type v} [CommRing R'] (p : ) [fp : Fact (Nat.Prime p)] [hch : CharP R' p] (χ : MulChar R R') (ψ : AddChar R R') :
    gaussSum χ ψ ^ p = gaussSum (χ ^ p) (ψ ^ p)

    When R' has prime characteristic p, then the pth power of the Gauss sum of χ and ψ is the Gauss sum of χ^p and ψ^p.

    theorem MulChar.IsQuadratic.gaussSum_frob {R : Type u} [CommRing R] [Fintype R] {R' : Type v} [CommRing R'] (p : ) [fp : Fact (Nat.Prime p)] [hch : CharP R' p] (hp : IsUnit p) {χ : MulChar R R'} (hχ : χ.IsQuadratic) (ψ : AddChar R R') :
    gaussSum χ ψ ^ p = χ p * gaussSum χ ψ

    For a quadratic character χ and when the characteristic p of the target ring is a unit in the source ring, the pth power of the Gauss sum ofχ and ψ is χ p times the original Gauss sum.

    theorem MulChar.IsQuadratic.gaussSum_frob_iter {R : Type u} [CommRing R] [Fintype R] {R' : Type v} [CommRing R'] (p : ) [fp : Fact (Nat.Prime p)] [hch : CharP R' p] (n : ) (hp : IsUnit p) {χ : MulChar R R'} (hχ : χ.IsQuadratic) (ψ : AddChar R R') :
    gaussSum χ ψ ^ p ^ n = χ (p ^ n) * gaussSum χ ψ

    For a quadratic character χ and when the characteristic p of the target ring is a unit in the source ring and n is a natural number, the p^nth power of the Gauss sum ofχ and ψ is χ (p^n) times the original Gauss sum.

    Values of quadratic characters #

    theorem Char.card_pow_char_pow {R : Type u} [CommRing R] [Fintype R] {R' : Type v} [CommRing R'] [IsDomain R'] {χ : MulChar R R'} (hχ : χ.IsQuadratic) (ψ : AddChar R R') (p : ) (n : ) [fp : Fact (Nat.Prime p)] [hch : CharP R' p] (hp : IsUnit p) (hp' : p 2) (hg : gaussSum χ ψ ^ 2 = χ (-1) * (Fintype.card R)) :
    (χ (-1) * (Fintype.card R)) ^ (p ^ n / 2) = χ (p ^ n)

    If the square of the Gauss sum of a quadratic character is χ(-1) * #R, then we get, for all n : ℕ, the relation (χ(-1) * #R) ^ (p^n/2) = χ(p^n), where p is the (odd) characteristic of the target ring R'. This version can be used when R is not a field, e.g., ℤ/8ℤ.

    theorem Char.card_pow_card {F : Type u_1} [Field F] [Fintype F] {F' : Type u_2} [Field F'] [Fintype F'] {χ : MulChar F F'} (hχ₁ : χ 1) (hχ₂ : χ.IsQuadratic) (hch₁ : ringChar F' ringChar F) (hch₂ : ringChar F' 2) :
    (χ (-1) * (Fintype.card F)) ^ (Fintype.card F' / 2) = χ (Fintype.card F')

    When F and F' are finite fields and χ : F → F' is a nontrivial quadratic character, then (χ(-1) * #F)^(#F'/2) = χ #F'.

    The quadratic character of 2 #

    This section proves the following result.

    For every finite field F of odd characteristic, we have 2^(#F/2) = χ₈#F in F. This can be used to show that the quadratic character of F takes the value χ₈#F at 2.

    The proof uses the Gauss sum of χ₈ and a primitive additive character on ℤ/8ℤ; in this way, the result is reduced to card_pow_char_pow.

    theorem FiniteField.two_pow_card {F : Type u_1} [Fintype F] [Field F] (hF : ringChar F 2) :
    2 ^ (Fintype.card F / 2) = (ZMod.χ₈ (Fintype.card F))

    For every finite field F of odd characteristic, we have 2^(#F/2) = χ₈ #F in F.