# Additive characters of finite rings and fields #

This file collects some results on additive characters whose domain is (the additive group of) a finite ring or field.

## Main definitions and results #

We define an additive character ψ to be primitive if mulShift ψ a is trivial only when a = 0.

We show that when ψ is primitive, then the map a ↦ mulShift ψ a is injective (AddChar.to_mulShift_inj_of_isPrimitive) and that ψ is primitive when R is a field and ψ is nontrivial (AddChar.IsNontrivial.isPrimitive).

We also show that there are primitive additive characters on R (with suitable target R') when R is a field or R = ZMod n (AddChar.primitiveCharFiniteField and AddChar.primitiveZModChar).

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

## Tags #

theorem AddChar.val_mem_rootsOfUnity {R : Type u} [] {R' : Type v} [] (φ : AddChar R R') (a : R) (h : 0 < ) :
.unit rootsOfUnity (ringChar R).toPNat' R'

The values of an additive character on a ring of positive characteristic are roots of unity.

def AddChar.IsPrimitive {R : Type u} [] {R' : Type v} [] (ψ : AddChar R R') :

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

Equations
• ψ.IsPrimitive = ∀ ⦃a : R⦄, a 0ψ.mulShift a 1
Instances For
theorem AddChar.IsPrimitive.compMulHom_of_isPrimitive {R : Type u} [] {R' : Type v} [] {R'' : Type u_1} [CommMonoid R''] {φ : AddChar R R'} {f : R' →* R''} (hφ : φ.IsPrimitive) (hf : ) :

The composition of a primitive additive character with an injective mooid homomorphism is also primitive.

theorem AddChar.to_mulShift_inj_of_isPrimitive {R : Type u} [] {R' : Type v} [] {ψ : AddChar R R'} (hψ : ψ.IsPrimitive) :
Function.Injective ψ.mulShift

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

theorem AddChar.IsPrimitive.of_ne_one {R' : Type v} [] {F : Type u} [] {ψ : AddChar F R'} (hψ : ψ 1) :
ψ.IsPrimitive

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

theorem AddChar.not_isPrimitive_mulShift {R : Type u} [] {R' : Type v} [] [] (e : AddChar R R') {r : R} (hr : ¬) :
¬(e.mulShift r).IsPrimitive

If r is not a unit, then e.mulShift r is not primitive.

structure AddChar.PrimitiveAddChar (R : Type u) [] (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.

• n : ℕ+

The first projection from PrimitiveAddChar, giving the cyclotomic field.

• char : AddChar R (CyclotomicField self.n R')

The second projection from PrimitiveAddChar, giving the character.

• prim : self.char.IsPrimitive

The third projection from PrimitiveAddChar, showing that χ.char is primitive.

Instances For
theorem AddChar.PrimitiveAddChar.prim {R : Type u} [] {R' : Type v} [Field R'] (self : ) :
self.char.IsPrimitive

The third projection from PrimitiveAddChar, showing that χ.char is primitive.

### Additive characters on ZMod n#

theorem AddChar.exists_divisor_of_not_isPrimitive {N : } [] {R : Type u_1} [] (e : AddChar (ZMod N) R) (he : ¬e.IsPrimitive) :
∃ (d : ), d N d < N e.mulShift d = 1

If e is not primitive, then e.mulShift d = 1 for some proper divisor d of N.

def AddChar.zmodChar {C : Type v} [] (n : ) [] {ζ : C} (hζ : ζ ^ n = 1) :

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

Equations
• = { toFun := fun (a : ZMod n) => ζ ^ a.val, map_zero_eq_one' := , map_add_eq_mul' := }
Instances For
theorem AddChar.zmodChar_apply {C : Type v} [] {n : } [] {ζ : C} (hζ : ζ ^ n = 1) (a : ZMod n) :
(AddChar.zmodChar n ) a = ζ ^ a.val

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

theorem AddChar.zmodChar_apply' {C : Type v} [] {n : } [] {ζ : C} (hζ : ζ ^ n = 1) (a : ) :
(AddChar.zmodChar n ) a = ζ ^ a
theorem AddChar.zmod_char_ne_one_iff {C : Type v} [] (n : ) [] (ψ : AddChar (ZMod n) C) :
ψ 1 ψ 1 1

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

theorem AddChar.IsPrimitive.zmod_char_eq_one_iff {C : Type v} [] (n : ) [] {ψ : AddChar (ZMod n) C} (hψ : ψ.IsPrimitive) (a : ZMod n) :
ψ a = 1 a = 0

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

theorem AddChar.zmod_char_primitive_of_eq_one_only_at_zero {C : Type v} [] (n : ) (ψ : AddChar (ZMod n) C) (hψ : ∀ (a : ZMod n), ψ a = 1a = 0) :
ψ.IsPrimitive

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

theorem AddChar.zmodChar_primitive_of_primitive_root {C : Type v} [] (n : ) [] {ζ : C} (h : ) :

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

noncomputable def AddChar.primitiveZModChar (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
• = { n := n, char := , prim := }
Instances For

### Existence of a primitive additive character on a finite field #

noncomputable def AddChar.FiniteField.primitiveChar (F : Type u_1) (F' : Type u_2) [] [] [Field F'] (h : ringChar 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
• One or more equations did not get rendered due to their size.
Instances For
def AddChar.primitiveCharFiniteField (F : Type u_1) (F' : Type u_2) [] [] [Field F'] (h : ringChar F' ) :

Alias of AddChar.FiniteField.primitiveChar.

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
Instances For

### The sum of all character values #

theorem AddChar.sum_eq_zero_of_ne_one {R : Type u_1} [] [] {R' : Type u_2} [CommRing R'] [IsDomain R'] {ψ : AddChar R R'} (hψ : ψ 1) :
a : R, ψ a = 0

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

theorem AddChar.sum_eq_card_of_eq_one {R : Type u_1} [] [] {R' : Type u_2} [CommRing R'] {ψ : AddChar R R'} (hψ : ψ = 1) :
a : R, ψ a = (Fintype.card R)

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

theorem AddChar.sum_mulShift {R : Type u_1} [] [] [] {R' : Type u_2} [CommRing R'] [IsDomain R'] {ψ : AddChar R R'} (b : R) (hψ : ψ.IsPrimitive) :
x : R, ψ (x * b) = (if b = 0 then else 0)

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

theorem AddChar.starComp_eq_inv {R : Type u_1} [] (hR : 0 < ) {φ : } :
Post-composing an additive character to ℂ with complex conjugation gives the inverse character.
A primitive additive character on the finite field F with values in ℂ.