mathlib documentation

number_theory.legendre_symbol.gauss_sum

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 mul_char R R') and ψ is an additive character R → R' (type add_char 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 gauss_sum {R : Type u} [comm_ring R] [fintype R] {R' : Type v} [comm_ring R'] (χ : mul_char R R') (ψ : add_char R R') :
R'

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

Equations
theorem gauss_sum_mul_shift {R : Type u} [comm_ring R] [fintype R] {R' : Type v} [comm_ring R'] (χ : mul_char R R') (ψ : add_char R R') (a : Rˣ) :

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

The product of two Gauss sums #

theorem gauss_sum_mul_gauss_sum_eq_card {R : Type u} [field R] [fintype R] {R' : Type v} [comm_ring R'] [is_domain R'] {χ : mul_char R R'} (hχ : χ.is_nontrivial) {ψ : add_char R R'} (hψ : ψ.is_primitive) :

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

theorem gauss_sum_sq {R : Type u} [field R] [fintype R] {R' : Type v} [comm_ring R'] [is_domain R'] {χ : mul_char R R'} (hχ₁ : χ.is_nontrivial) (hχ₂ : χ.is_quadratic) {ψ : add_char R R'} (hψ : ψ.is_primitive) :
gauss_sum χ ψ ^ 2 = χ (-1) * (fintype.card R)

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

Gauss sums and Frobenius #

theorem gauss_sum_frob {R : Type u} [comm_ring R] [fintype R] {R' : Type v} [comm_ring R'] (p : ) [fp : fact (nat.prime p)] [hch : char_p R' p] (χ : mul_char R R') (ψ : add_char R R') :
gauss_sum χ ψ ^ p = gauss_sum ^ 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 mul_char.is_quadratic.gauss_sum_frob {R : Type u} [comm_ring R] [fintype R] {R' : Type v} [comm_ring R'] (p : ) [fp : fact (nat.prime p)] [hch : char_p R' p] (hp : is_unit p) {χ : mul_char R R'} (hχ : χ.is_quadratic) (ψ : add_char R R') :
gauss_sum χ ψ ^ p = χ p * gauss_sum χ ψ

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 mul_char.is_quadratic.gauss_sum_frob_iter {R : Type u} [comm_ring R] [fintype R] {R' : Type v} [comm_ring R'] (p : ) [fp : fact (nat.prime p)] [hch : char_p R' p] (n : ) (hp : is_unit p) {χ : mul_char R R'} (hχ : χ.is_quadratic) (ψ : add_char R R') :
gauss_sum χ ψ ^ p ^ n = χ (p ^ n) * gauss_sum χ ψ

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} [comm_ring R] [fintype R] {R' : Type v} [comm_ring R'] [is_domain R'] {χ : mul_char R R'} (hχ : χ.is_quadratic) (ψ : add_char R R') (p n : ) [fp : fact (nat.prime p)] [hch : char_p R' p] (hp : is_unit p) (hp' : p 2) (hg : gauss_sum χ ψ ^ 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} [field F] [fintype F] {F' : Type} [field F'] [fintype F'] {χ : mul_char F F'} (hχ₁ : χ.is_nontrivial) (hχ₂ : χ.is_quadratic) (hch₁ : ring_char F' ring_char F) (hch₂ : ring_char 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 finite_field.two_pow_card {F : Type u_1} [fintype F] [field F] (hF : ring_char F 2) :

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