# 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 #

@[protected, instance]
def add_char.inhabited (R : Type u) [add_monoid R] (R' : Type v) [comm_monoid R'] :
@[protected, instance]
def add_char.comm_monoid (R : Type u) [add_monoid R] (R' : Type v) [comm_monoid R'] :
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
def add_char.to_monoid_hom {R : Type u} [add_monoid R] {R' : Type v} [comm_monoid R'] :
R' →* R'

Interpret an additive character as a monoid homomorphism.

Equations
@[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 : 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
theorem add_char.coe_to_fun_apply {R : Type u} [add_monoid R] {R' : Type v} [comm_monoid R'] (ψ : R') (a : R) :
ψ a =
@[protected, instance]
Equations
@[simp]
theorem add_char.map_zero_one {R : Type u} [add_monoid R] {R' : Type v} [comm_monoid R'] (ψ : R') :
ψ 0 = 1

An additive character maps 0 to 1.

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

An additive character maps sums to products.

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

An additive character maps multiples by natural numbers to powers.

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

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
theorem add_char.inv_apply {R : Type u} {R' : Type v} [comm_monoid R'] (ψ : R') (x : R) :
ψ⁻¹ x = ψ (-x)
@[simp]
theorem add_char.map_zsmul_zpow {R : Type u} {R' : Type v} [comm_group R'] (ψ : R') (n : ) (x : R) :
ψ (n x) = ψ x ^ n

An additive character maps multiples by integers to powers.

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

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

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

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

Equations
theorem add_char.is_nontrivial_iff_ne_trivial {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] (ψ : R') :

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

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

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

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

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

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

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

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

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

theorem add_char.mul_shift_mul {R : Type u} [comm_ring R] {R' : Type v} [comm_ring 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).

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

mul_shift ψ 0 is the trivial character.

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

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

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

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

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

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

@[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
def add_char.primitive_add_char.n {R : Type u} [comm_ring R] {R' : Type v} [field R'] :

The first projection from primitive_add_char, giving the cyclotomic field.

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

The second projection from primitive_add_char, giving the character.

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

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

### Additive characters on zmod n#

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

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

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

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

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

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

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.

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

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

theorem add_char.zmod_char_primitive_of_primitive_root {C : Type v} [comm_ring C] (n : ℕ+) {ζ : C} (h : n) :

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

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

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 #

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

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 #

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'] {ψ : 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.

theorem add_char.sum_eq_card_of_is_trivial {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] [fintype 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.

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'] {ψ : 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.