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 ℤ.
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_mul
.
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.
Some basic API lemmas
For nonzero a : F
, quadratic_char F a = 1 ↔ is_square a
.
The quadratic character takes the value 1
on nonzero squares.
If ring_char F = 2
, then quadratic_char F
takes the value 1
on nonzero elements.
If ring_char F
is odd, then quadratic_char F a
can be computed in
terms of a ^ (fintype.card F / 2)
.
The quadratic character is multiplicative.
The quadratic character is a homomorphism of monoids with zero.
Equations
- char.quadratic_char_hom = {to_fun := char.quadratic_char F (λ (a : F), is_square_decidable a), map_zero' := _, map_one' := _, map_mul' := _}
The square of the quadratic character on nonzero arguments is 1
.
The quadratic character is 1
or -1
on nonzero arguments.
A variant
For a : F
, quadratic_char F a = -1 ↔ ¬ is_square a
.
If F
has odd characteristic, then quadratic_char F
takes the value -1
.
The number of solutions to x^2 = a
is determined by the quadratic character.
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 χ₄
.
The value of the quadratic character at -1
The interpretation in terms of whether -1
is a square in F