mathlib documentation

number_theory.legendre_symbol.quadratic_char

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 quadratic_char_fun (α : Type u_1) [monoid_with_zero α] [decidable_eq α] [decidable_pred is_square] (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 quadratic_char_fun_mul.

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

Equations

quadratic_char_fun α a = ite (a = 0) 0 (ite (is_square a) 1 (-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 quadratic_char_fun_eq_zero_iff {F : Type u_1} [field F] [fintype F] [decidable_eq F] {a : F} :

quadratic_char_fun F a = 0 ↔ a = 0

Some basic API lemmas

@[simp]

theorem quadratic_char_fun_zero {F : Type u_1} [field F] [fintype F] [decidable_eq F] :

quadratic_char_fun F 0 = 0

@[simp]

theorem quadratic_char_fun_one {F : Type u_1} [field F] [fintype F] [decidable_eq F] :

quadratic_char_fun F 1 = 1

theorem quadratic_char_fun_eq_one_of_char_two {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F = 2) {a : F} (ha : a ≠ 0) :

quadratic_char_fun F a = 1

If ring_char F = 2, then quadratic_char_fun F takes the value 1 on nonzero elements.

theorem quadratic_char_fun_eq_pow_of_char_ne_two {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :

quadratic_char_fun F a = ite (a ^ (fintype.card F / 2) = 1) 1 (-1)

If ring_char F is odd, then quadratic_char_fun F a can be computed in terms of a ^ (fintype.card F / 2).

theorem quadratic_char_fun_mul {F : Type u_1} [field F] [fintype F] [decidable_eq F] (a b : F) :

quadratic_char_fun F (a * b) = quadratic_char_fun F a * quadratic_char_fun F b

The quadratic character is multiplicative.

def quadratic_char (F : Type u_1) [field F] [fintype F] [decidable_eq F] :

The quadratic character as a multiplicative character.

Equations

quadratic_char F = {to_monoid_hom := {to_fun := quadratic_char_fun F (λ (a : F), fintype.is_square.decidable_pred a), map_one' := _, map_mul' := _}, map_nonunit' := _}

@[simp]

theorem quadratic_char_apply (F : Type u_1) [field F] [fintype F] [decidable_eq F] (a : F) :

⇑(quadratic_char F) a = quadratic_char_fun F a

theorem quadratic_char_eq_zero_iff {F : Type u_1} [field F] [fintype F] [decidable_eq F] {a : F} :

⇑(quadratic_char F) a = 0 ↔ a = 0

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

@[simp]

theorem quadratic_char_zero {F : Type u_1} [field F] [fintype F] [decidable_eq F] :

⇑(quadratic_char F) 0 = 0

theorem quadratic_char_one_iff_is_square {F : Type u_1} [field F] [fintype F] [decidable_eq F] {a : F} (ha : a ≠ 0) :

⇑(quadratic_char F) a = 1 ↔ is_square a

For nonzero a : F, quadratic_char F a = 1 ↔ is_square a.

theorem quadratic_char_sq_one' {F : Type u_1} [field F] [fintype F] [decidable_eq F] {a : F} (ha : a ≠ 0) :

⇑(quadratic_char F) (a ^ 2) = 1

The quadratic character takes the value 1 on nonzero squares.

theorem quadratic_char_sq_one {F : Type u_1} [field F] [fintype F] [decidable_eq F] {a : F} (ha : a ≠ 0) :

⇑(quadratic_char F) a ^ 2 = 1

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

theorem quadratic_char_dichotomy {F : Type u_1} [field F] [fintype F] [decidable_eq F] {a : F} (ha : a ≠ 0) :

⇑(quadratic_char F) a = 1 ∨ ⇑(quadratic_char F) a = -1

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

theorem quadratic_char_eq_neg_one_iff_not_one {F : Type u_1} [field F] [fintype F] [decidable_eq F] {a : F} (ha : a ≠ 0) :

⇑(quadratic_char F) a = -1 ↔ ¬⇑(quadratic_char F) a = 1

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

theorem quadratic_char_neg_one_iff_not_is_square {F : Type u_1} [field F] [fintype F] [decidable_eq F] {a : F} :

⇑(quadratic_char F) a = -1 ↔ ¬is_square a

For a : F, quadratic_char F a = -1 ↔ ¬ is_square a.

theorem quadratic_char_exists_neg_one {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F ≠ 2) :

∃ (a : F), ⇑(quadratic_char F) a = -1

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

theorem quadratic_char_eq_one_of_char_two {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F = 2) {a : F} (ha : a ≠ 0) :

⇑(quadratic_char F) a = 1

If ring_char F = 2, then quadratic_char F takes the value 1 on nonzero elements.

theorem quadratic_char_eq_pow_of_char_ne_two {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :

⇑(quadratic_char F) a = ite (a ^ (fintype.card F / 2) = 1) 1 (-1)

If ring_char F is odd, then quadratic_char F a can be computed in terms of a ^ (fintype.card F / 2).

theorem quadratic_char_eq_pow_of_char_ne_two' {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F ≠ 2) (a : F) :

↑(⇑(quadratic_char F) a) = a ^ (fintype.card F / 2)

theorem quadratic_char_is_quadratic (F : Type u_1) [field F] [fintype F] [decidable_eq F] :

(quadratic_char F).is_quadratic

The quadratic character is quadratic as a multiplicative character.

theorem quadratic_char_is_nontrivial {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F ≠ 2) :

(quadratic_char F).is_nontrivial

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

theorem quadratic_char_card_sqrts {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F ≠ 2) (a : F) :

↑({x : F | x ^ 2 = a}.to_finset.card) = ⇑(quadratic_char F) a + 1

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

theorem quadratic_char_sum_zero {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F ≠ 2) :

finset.univ.sum (λ (a : F), ⇑(quadratic_char 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 quadratic_char F (-1) in terms of χ₄.

theorem quadratic_char_neg_one {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F ≠ 2) :

⇑(quadratic_char F) (-1) = ⇑zmod.χ₄ ↑(fintype.card F)

The value of the quadratic character at -1

theorem finite_field.is_square_neg_one_iff {F : Type u_1} [field F] [fintype F] :

is_square (-1) ↔ fintype.card F % 4 ≠ 3

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

theorem quadratic_char_two {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F ≠ 2) :

⇑(quadratic_char F) 2 = ⇑zmod.χ₈ ↑(fintype.card F)

The value of the quadratic character at 2

theorem finite_field.is_square_two_iff {F : Type u_1} [field F] [fintype F] :

is_square 2 ↔ fintype.card F % 8 ≠ 3 ∧ fintype.card F % 8 ≠ 5

2 is a square in F iff #F is not congruent to 3 or 5 mod 8.

theorem quadratic_char_neg_two {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F ≠ 2) :

⇑(quadratic_char F) (-2) = ⇑zmod.χ₈' ↑(fintype.card F)

The value of the quadratic character at -2

theorem finite_field.is_square_neg_two_iff {F : Type u_1} [field F] [fintype F] :

is_square (-2) ↔ fintype.card F % 8 ≠ 5 ∧ fintype.card F % 8 ≠ 7

-2 is a square in F iff #F is not congruent to 5 or 7 mod 8.

theorem quadratic_char_card_card {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F ≠ 2) {F' : Type u_2} [field F'] [fintype F'] [decidable_eq F'] (hF' : ring_char F' ≠ 2) (h : ring_char F' ≠ ring_char F) :

⇑(quadratic_char F) ↑(fintype.card F') = ⇑(quadratic_char F') (↑(⇑(quadratic_char F) (-1)) * ↑(fintype.card F))

The relation between the values of the quadratic character of one field F at the cardinality of another field F' and of the quadratic character of F' at the cardinality of F.

theorem quadratic_char_odd_prime {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F ≠ 2) {p : ℕ} [fact (nat.prime p)] (hp₁ : p ≠ 2) (hp₂ : ring_char F ≠ p) :

⇑(quadratic_char F) ↑p = ⇑(quadratic_char (zmod p)) (↑(⇑zmod.χ₄ ↑(fintype.card F)) * ↑(fintype.card F))

The value of the quadratic character at an odd prime p different from ring_char F.

theorem finite_field.is_square_odd_prime_iff {F : Type u_1} [field F] [fintype F] (hF : ring_char F ≠ 2) {p : ℕ} [fact (nat.prime p)] (hp : p ≠ 2) :

is_square ↑p ↔ ⇑(quadratic_char (zmod p)) (↑(⇑zmod.χ₄ ↑(fintype.card F)) * ↑(fintype.card F)) ≠ -1

An odd prime p is a square in F iff the quadratic character of zmod p does not take the value -1 on χ₄(#F) * #F.