mathlib3 documentation

number_theory.legendre_symbol.add_character

Additive characters of finite rings and fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Let R be a finite commutative ring. An additive character of R with values in another commutative ring R' is simply a morphism from the additive group of R into the multiplicative monoid of R'.

The additive characters on R with values in R' form a commutative group.

We use the namespace add_char.

Main definitions and results #

We define mul_shift ψ a, where ψ : add_char R R' and a : R, to be the character defined by x ↦ ψ (a * x). An additive character ψ is primitive if mul_shift ψ a is trivial only when a = 0.

We show that when ψ is primitive, then the map a ↦ mul_shift ψ a is injective (add_char.to_mul_shift_inj_of_is_primitive) and that ψ is primitive when R is a field and ψ is nontrivial (add_char.is_nontrivial.is_primitive).

We also show that there are primitive additive characters on R (with suitable target R') when R is a field or R = zmod n (add_char.primitive_char_finite_field and add_char.primitive_zmod_char).

Finally, we show that the sum of all character values is zero when the character is nontrivial (and the target is a domain); see add_char.sum_eq_zero_of_is_nontrivial.

Tags #

additive character

source
@[protected, instance]
def add_char.inhabited (R : Type u) [add_monoid R] (R' : Type v) [comm_monoid R'] :
inhabited (add_char R R')
source
@[protected, instance]
def add_char.comm_monoid (R : Type u) [add_monoid R] (R' : Type v) [comm_monoid R'] :
comm_monoid (add_char R R')
source
def add_char (R : Type u) [add_monoid R] (R' : Type v) [comm_monoid R'] :
Type (max u v)

Define add_char R R' as (multiplicative R) →* R'. The definition works for an additive monoid R and a monoid R', but we will restrict to the case that both are commutative rings below. We assume right away that R' is commutative, so that add_char R R' carries a structure of commutative monoid. The trivial additive character (sending everything to 1) is (1 : add_char R R').

Equations
Instances for add_char
source
def add_char.to_monoid_hom {R : Type u} [add_monoid R] {R' : Type v} [comm_monoid R'] :
add_char R R' → multiplicative R →* R'

Interpret an additive character as a monoid homomorphism.

Equations
source
@[protected, instance]
def add_char.has_coe_to_fun {R : Type u} [add_monoid R] {R' : Type v} [comm_monoid R'] :
has_coe_to_fun (add_char R R') (λ (x : add_char R R'), R → R')

Define coercion to a function so that it includes the move from R to multiplicative R. After we have proved the API lemmas below, we don't need to worry about writing of_add a when we want to apply an additive character.

Equations
source
theorem add_char.coe_to_fun_apply {R : Type u} [add_monoid R] {R' : Type v} [comm_monoid R'] (ψ : add_char R R') (a : R) :
⇑ψ a = ⇑(ψ.to_monoid_hom) (⇑multiplicative.of_add a)
source
@[protected, instance]
def add_char.monoid_hom_class {R : Type u} [add_monoid R] {R' : Type v} [comm_monoid R'] :
monoid_hom_class (add_char R R') (multiplicative R) R'
Equations
source
@[simp]
theorem add_char.map_zero_one {R : Type u} [add_monoid R] {R' : Type v} [comm_monoid R'] (ψ : add_char R R') :
⇑ψ 0 = 1

An additive character maps 0 to 1.

source
@[simp]
theorem add_char.map_add_mul {R : Type u} [add_monoid R] {R' : Type v} [comm_monoid R'] (ψ : add_char R R') (x y : R) :
⇑ψ (x + y) = ⇑ψ x * ⇑ψ y

An additive character maps sums to products.

source
@[simp]
theorem add_char.map_nsmul_pow {R : Type u} [add_monoid R] {R' : Type v} [comm_monoid R'] (ψ : add_char R R') (n : ℕ) (x : R) :
⇑ψ (n • x) = ⇑ψ x ^ n

An additive character maps multiples by natural numbers to powers.

source
@[protected, instance]
def add_char.has_inv {R : Type u} [add_comm_group R] {R' : Type v} [comm_monoid R'] :
has_inv (add_char R R')

An additive character on a commutative additive group has an inverse.

Note that this is a different inverse to the one provided by monoid_hom.has_inv, as it acts on the domain instead of the codomain.

Equations
source
theorem add_char.inv_apply {R : Type u} [add_comm_group R] {R' : Type v} [comm_monoid R'] (ψ : add_char R R') (x : R) :
⇑ψ⁻¹ x = ⇑ψ (-x)
source
@[simp]
theorem add_char.map_zsmul_zpow {R : Type u} [add_comm_group R] {R' : Type v} [comm_group R'] (ψ : add_char R R') (n : ℤ) (x : R) :
⇑ψ (n • x) = ⇑ψ x ^ n

An additive character maps multiples by integers to powers.

source
@[protected, instance]
def add_char.comm_group {R : Type u} [add_comm_group R] {R' : Type v} [comm_monoid R'] :
comm_group (add_char R R')

The additive characters on a commutative additive group form a commutative group.

Equations
source
def add_char.is_nontrivial {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] (ψ : add_char R R') :
Prop

An additive character is nontrivial if it takes a value ≠ 1.

Equations
source
theorem add_char.is_nontrivial_iff_ne_trivial {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] (ψ : add_char R R') :
ψ.is_nontrivial ↔ ψ ≠ 1

An additive character is nontrivial iff it is not the trivial character.

source
def add_char.mul_shift {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] (ψ : add_char R R') (a : R) :
add_char R R'

Define the multiplicative shift of an additive character. This satisfies mul_shift ψ a x = ψ (a * x).

Equations
source
@[simp]
theorem add_char.mul_shift_apply {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] {ψ : add_char R R'} {a x : R} :
⇑(ψ.mul_shift a) x = ⇑ψ (a * x)
source
theorem add_char.inv_mul_shift {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] (ψ : add_char R R') :
ψ⁻¹ = ψ.mul_shift (-1)

ψ⁻¹ = mul_shift ψ (-1)).

source
theorem add_char.mul_shift_spec' {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] (ψ : add_char R R') (n : ℕ) (x : R) :
⇑(ψ.mul_shift ↑n) x = ⇑ψ x ^ n

If n is a natural number, then mul_shift ψ n x = (ψ x) ^ n.

source
theorem add_char.pow_mul_shift {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] (ψ : add_char R R') (n : ℕ) :
ψ ^ n = ψ.mul_shift ↑n

If n is a natural number, then ψ ^ n = mul_shift ψ n.

source
theorem add_char.mul_shift_mul {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] (ψ : add_char R R') (a b : R) :
ψ.mul_shift a * ψ.mul_shift b = ψ.mul_shift (a + b)

The product of mul_shift ψ a and mul_shift ψ b is mul_shift ψ (a + b).

source
@[simp]
theorem add_char.mul_shift_zero {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] (ψ : add_char R R') :
ψ.mul_shift 0 = 1

mul_shift ψ 0 is the trivial character.

source
def add_char.is_primitive {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] (ψ : add_char R R') :
Prop

An additive character is primitive iff all its multiplicative shifts by nonzero elements are nontrivial.

Equations
source
theorem add_char.to_mul_shift_inj_of_is_primitive {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] {ψ : add_char R R'} (hψ : ψ.is_primitive) :
function.injective ψ.mul_shift

The map associating to a : R the multiplicative shift of ψ by a is injective when ψ is primitive.

source
theorem add_char.is_nontrivial.is_primitive {R' : Type v} [comm_ring R'] {F : Type u} [field F] {ψ : add_char F R'} (hψ : ψ.is_nontrivial) :
ψ.is_primitive

When R is a field F, then a nontrivial additive character is primitive

source
@[nolint]
def add_char.primitive_add_char (R : Type u) [comm_ring R] (R' : Type v) [field R'] :
Type (max u v)

Definition for a primitive additive character on a finite ring R into a cyclotomic extension of a field R'. It records which cyclotomic extension it is, the character, and the fact that the character is primitive.

Equations
source
def add_char.primitive_add_char.n {R : Type u} [comm_ring R] {R' : Type v} [field R'] :
add_char.primitive_add_char R R' → ℕ+

The first projection from primitive_add_char, giving the cyclotomic field.

Equations
source
def add_char.primitive_add_char.char {R : Type u} [comm_ring R] {R' : Type v} [field R'] (χ : add_char.primitive_add_char R R') :
add_char R (cyclotomic_field χ.n R')

The second projection from primitive_add_char, giving the character.

Equations
source
theorem add_char.primitive_add_char.prim {R : Type u} [comm_ring R] {R' : Type v} [field R'] (χ : add_char.primitive_add_char R R') :
χ.char.is_primitive

The third projection from primitive_add_char, showing that χ.2 is primitive.

Additive characters on zmod n #

source
def add_char.zmod_char {C : Type v} [comm_ring C] (n : ℕ+) {ζ : C} (hζ : ζ ^ ↑n = 1) :
add_char (zmod ↑n) C

We can define an additive character on zmod n when we have an nth root of unity ζ : C.

Equations
source
theorem add_char.zmod_char_apply {C : Type v} [comm_ring C] {n : ℕ+} {ζ : C} (hζ : ζ ^ ↑n = 1) (a : zmod ↑n) :
⇑(add_char.zmod_char n hζ) a = ζ ^ a.val

The additive character on zmod n defined using ζ sends a to ζ^a.

source
theorem add_char.zmod_char_apply' {C : Type v} [comm_ring C] {n : ℕ+} {ζ : C} (hζ : ζ ^ ↑n = 1) (a : ℕ) :
⇑(add_char.zmod_char n hζ) ↑a = ζ ^ a
source
theorem add_char.zmod_char_is_nontrivial_iff {C : Type v} [comm_ring C] (n : ℕ+) (ψ : add_char (zmod ↑n) C) :
ψ.is_nontrivial ↔ ⇑ψ 1 ≠ 1

An additive character on zmod n is nontrivial iff it takes a value ≠ 1 on 1.

source
theorem add_char.is_primitive.zmod_char_eq_one_iff {C : Type v} [comm_ring C] (n : ℕ+) {ψ : add_char (zmod ↑n) C} (hψ : ψ.is_primitive) (a : zmod ↑n) :
⇑ψ a = 1 ↔ a = 0

A primitive additive character on zmod n takes the value 1 only at 0.

source
theorem add_char.zmod_char_primitive_of_eq_one_only_at_zero {C : Type v} [comm_ring C] (n : ℕ) (ψ : add_char (zmod n) C) (hψ : ∀ (a : zmod n), ⇑ψ a = 1 → a = 0) :
ψ.is_primitive

The converse: if the additive character takes the value 1 only at 0, then it is primitive.

source
theorem add_char.zmod_char_primitive_of_primitive_root {C : Type v} [comm_ring C] (n : ℕ+) {ζ : C} (h : is_primitive_root ζ ↑n) :
(add_char.zmod_char n _).is_primitive

The additive character on zmod n associated to a primitive nth root of unity is primitive

source
noncomputable def add_char.primitive_zmod_char (n : ℕ+) (F' : Type v) [field F'] (h : ↑n ≠ 0) :
add_char.primitive_add_char (zmod ↑n) F'

There is a primitive additive character on zmod n if the characteristic of the target does not divide n

Equations

Existence of a primitive additive character on a finite field #

source
noncomputable def add_char.primitive_char_finite_field (F : Type u_1) (F' : Type u_2) [field F] [fintype F] [field F'] (h : ring_char F' ≠ ring_char F) :
add_char.primitive_add_char F F'

There is a primitive additive character on the finite field F if the characteristic of the target is different from that of F. We obtain it as the composition of the trace from F to zmod p with a primitive additive character on zmod p, where p is the characteristic of F.

Equations

The sum of all character values #

source
theorem add_char.sum_eq_zero_of_is_nontrivial {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] [fintype R] [is_domain R'] {ψ : add_char R R'} (hψ : ψ.is_nontrivial) :
finset.univ.sum (λ (a : R), ⇑ψ a) = 0

The sum over the values of a nontrivial additive character vanishes if the target ring is a domain.

source
theorem add_char.sum_eq_card_of_is_trivial {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] [fintype R] {ψ : add_char R R'} (hψ : ¬ψ.is_nontrivial) :
finset.univ.sum (λ (a : R), ⇑ψ a) = ↑(fintype.card R)

The sum over the values of the trivial additive character is the cardinality of the source.

source
theorem add_char.sum_mul_shift {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] [fintype R] [decidable_eq R] [is_domain R'] {ψ : add_char R R'} (b : R) (hψ : ψ.is_primitive) :
finset.univ.sum (λ (x : R), ⇑ψ (x * b)) = ite (b = 0) ↑(fintype.card R) 0

The sum over the values of mul_shift ψ b for ψ primitive is zero when b ≠ 0 and #R otherwise.