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 ℤ.

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

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.

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

@[simp]

theorem quadraticCharFun_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] : quadraticCharFun F 0 = 0

@[simp]

theorem quadraticCharFun_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] : quadraticCharFun F 1 = 1

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.

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

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.

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' := ⋯ }

@[simp]

theorem quadraticChar_apply (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] (a : F) : (quadraticChar F) a = quadraticCharFun F a

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.

theorem quadraticChar_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] : (quadraticChar F) 0 = 0

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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)

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.

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.

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.

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.

theorem quadraticChar_sum_comp_eq_zero_of_odd {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ¬IsSquare (-1)) {f : F → F} (hf : Function.Odd f) : ∑ x : F, (quadraticChar F) (f x) = 0

The sum of the quadratic character over the values of an odd function is zero when -1 is not a square.

Special values of the quadratic character

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

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

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.