# Quadratic characters of finite fields #

This file defines the quadratic character on a finite field `F` and proves some basic statements about it.

## Tags #

quadratic character

### Definition of the quadratic character #

We define the quadratic character of a finite field `F` with values in ℤ.

source
def quadraticCharFun (α : Type u_1) [MonoidWithZero α] [DecidableEq α] [DecidablePred IsSquare] (a : α) :
ℤ

Define the quadratic character with values in ℤ on a monoid with zero `α`. It takes the value zero at zero; for non-zero argument `a : α`, it is `1` if `a` is a square, otherwise it is `-1`.

This only deserves the name "character" when it is multiplicative, e.g., when `α` is a finite field. See `quadraticCharFun_mul`.

We will later define `quadraticChar` to be a multiplicative character of type `MulChar F ℤ`, when the domain is a finite field `F`.

Equations

- quadraticCharFun α a = if a = 0 then 0 else if IsSquare a then 1 else -1

Instances For

### Basic properties of the quadratic character #

We prove some properties of the quadratic character. We work with a finite field `F` here. The interesting case is when the characteristic of `F` is odd.

source
theorem quadraticCharFun_eq_zero_iff {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} :
quadraticCharFun F a = 0 ↔ a = 0

Some basic API lemmas

source
@[simp]
theorem quadraticCharFun_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] :
quadraticCharFun F 0 = 0
source
@[simp]
theorem quadraticCharFun_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] :
quadraticCharFun F 1 = 1
source
theorem quadraticCharFun_eq_one_of_char_two {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F = 2) {a : F} (ha : a ≠ 0) :
quadraticCharFun F a = 1

If `ringChar F = 2`, then `quadraticCharFun F` takes the value `1` on nonzero elements.

source
theorem quadraticCharFun_eq_pow_of_char_ne_two {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {a : F} (ha : a ≠ 0) :
quadraticCharFun F a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1

If `ringChar F` is odd, then `quadraticCharFun F a` can be computed in terms of `a ^ (Fintype.card F / 2)`.

source
theorem quadraticCharFun_mul {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (a b : F) :
quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

The quadratic character is multiplicative.

source
def quadraticChar (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] :
MulChar F ℤ

The quadratic character as a multiplicative character.

Equations

- quadraticChar F = { toFun := quadraticCharFun F, map_one' := ⋯, map_mul' := ⋯, map_nonunit' := ⋯ }

Instances For

source
@[simp]
theorem quadraticChar_apply (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] (a : F) :
(quadraticChar F) a = quadraticCharFun F a
source
theorem quadraticChar_eq_zero_iff {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} :
(quadraticChar F) a = 0 ↔ a = 0

The value of the quadratic character on `a` is zero iff `a = 0`.

source
theorem quadraticChar_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] :
(quadraticChar F) 0 = 0
source
theorem quadraticChar_one_iff_isSquare {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} (ha : a ≠ 0) :
(quadraticChar F) a = 1 ↔ IsSquare a

For nonzero `a : F`, `quadraticChar F a = 1 ↔ IsSquare a`.

source
theorem quadraticChar_sq_one' {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} (ha : a ≠ 0) :
(quadraticChar F) (a ^ 2) = 1

The quadratic character takes the value `1` on nonzero squares.

source
theorem quadraticChar_sq_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} (ha : a ≠ 0) :
(quadraticChar F) a ^ 2 = 1

The square of the quadratic character on nonzero arguments is `1`.

source
theorem quadraticChar_dichotomy {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} (ha : a ≠ 0) :
(quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1

The quadratic character is `1` or `-1` on nonzero arguments.

source
theorem quadraticChar_eq_neg_one_iff_not_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} (ha : a ≠ 0) :
(quadraticChar F) a = -1 ↔ ¬(quadraticChar F) a = 1

The quadratic character is `1` or `-1` on nonzero arguments.

source
theorem quadraticChar_neg_one_iff_not_isSquare {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} :
(quadraticChar F) a = -1 ↔ ¬IsSquare a

For `a : F`, `quadraticChar F a = -1 ↔ ¬ IsSquare a`.

source
theorem quadraticChar_exists_neg_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) :
∃ (a : F), (quadraticChar F) a = -1

If `F` has odd characteristic, then `quadraticChar F` takes the value `-1`.

source
theorem quadraticChar_exists_neg_one' {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) :
∃ (a : F ˣ), (quadraticChar F) ↑a = -1

If `F` has odd characteristic, then `quadraticChar F` takes the value `-1` on some unit.

source
theorem quadraticChar_eq_one_of_char_two {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F = 2) {a : F} (ha : a ≠ 0) :
(quadraticChar F) a = 1

If `ringChar F = 2`, then `quadraticChar F` takes the value `1` on nonzero elements.

source
theorem quadraticChar_eq_pow_of_char_ne_two {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {a : F} (ha : a ≠ 0) :
(quadraticChar F) a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1

If `ringChar F` is odd, then `quadraticChar F a` can be computed in terms of `a ^ (Fintype.card F / 2)`.

source
theorem quadraticChar_eq_pow_of_char_ne_two' {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (a : F) :
↑((quadraticChar F) a) = a ^ (Fintype.card F / 2)
source
theorem quadraticChar_isQuadratic (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] :
(quadraticChar F).IsQuadratic

The quadratic character is quadratic as a multiplicative character.

source
theorem quadraticChar_ne_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) :
quadraticChar F ≠ 1

The quadratic character is nontrivial as a multiplicative character when the domain has odd characteristic.

source
theorem quadraticChar_card_sqrts {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (a : F) :
↑{x : F | x ^ 2 = a}.toFinset.card = (quadraticChar F) a + 1

The number of solutions to `x^2 = a` is determined by the quadratic character.

source
theorem quadraticChar_sum_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) :
∑ a : F, (quadraticChar F) a = 0

The sum over the values of the quadratic character is zero when the characteristic is odd.

### Special values of the quadratic character #

We express `quadraticChar F (-1)` in terms of `χ₄`.

source
theorem quadraticChar_neg_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) :
(quadraticChar F) (-1) = ZMod.χ₄ ↑(Fintype.card F)

The value of the quadratic character at `-1`

source
theorem FiniteField.isSquare_neg_one_iff {F : Type u_1} [Field F] [Fintype F] :
IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3

`-1` is a square in `F` iff `#F` is not congruent to `3` mod `4`.