# Additive characters of finite rings and fields #

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 AddChar.

## Main definitions and results #

We define mulShift ψ a, where ψ : AddChar R R' and a : R, to be the character defined by x ↦ ψ (a * x). An additive character ψ is 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 #

def AddChar (R : Type u) [] (R' : Type v) [] :
Type (max u v)

Define AddChar 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 AddChar R R' carries a structure of commutative monoid. The trivial additive character (sending everything to 1) is (1 : AddChar R R').

Instances For
instance AddChar.instCommMonoidAddChar (R : Type u) [] (R' : Type v) [] :
instance AddChar.instInhabitedAddChar (R : Type u) [] (R' : Type v) [] :
def AddChar.toMonoidHom {R : Type u} [] {R' : Type v} [] :

Interpret an additive character as a monoid homomorphism.

Instances For
def AddChar.toFun {R : Type u} [] {R' : Type v} [] (ψ : AddChar R R') (x : R) :
R'
Instances For
instance AddChar.hasCoeToFun {R : Type u} [] {R' : Type v} [] :
CoeFun (AddChar R R') fun x => RR'

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 ofAdd a when we want to apply an additive character.

theorem AddChar.coe_to_fun_apply {R : Type u} [] {R' : Type v} [] (ψ : AddChar R R') (a : R) :
ψ a = ↑() (Multiplicative.ofAdd a)
theorem AddChar.mul_apply {R : Type u} [] {R' : Type v} [] (ψ : AddChar R R') (φ : AddChar R R') (a : R) :
↑(ψ * φ) a = ψ a * φ a
@[simp]
theorem AddChar.one_apply {R : Type u} [] {R' : Type v} [] (a : R) :
1 a = 1
instance AddChar.monoidHomClass {R : Type u} [] {R' : Type v} [] :
MonoidHomClass (AddChar R R') () R'
theorem AddChar.ext {R : Type u} [] {R' : Type v} [] (f : AddChar R R') (g : AddChar R R') (h : ∀ (x : R), f x = g x) :
f = g
@[simp]
theorem AddChar.map_zero_one {R : Type u} [] {R' : Type v} [] (ψ : AddChar R R') :
ψ 0 = 1

An additive character maps 0 to 1.

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

An additive character maps sums to products.

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

An additive character maps multiples by natural numbers to powers.

instance AddChar.hasInv {R : Type u} [] {R' : Type v} [] :

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

theorem AddChar.inv_apply {R : Type u} [] {R' : Type v} [] (ψ : AddChar R R') (x : R) :
ψ⁻¹ x = ψ (-x)
@[simp]
theorem AddChar.map_zsmul_zpow {R : Type u} [] {R' : Type v} [] (ψ : AddChar R R') (n : ) (x : R) :
ψ (n x) = ψ x ^ n

An additive character maps multiples by integers to powers.

instance AddChar.commGroup {R : Type u} [] {R' : Type v} [] :

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

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

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

Instances For
theorem AddChar.isNontrivial_iff_ne_trivial {R : Type u} [] {R' : Type v} [CommRing R'] (ψ : AddChar R R') :
ψ 1

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

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

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

Instances For
@[simp]
theorem AddChar.mulShift_apply {R : Type u} [] {R' : Type v} [CommRing R'] {ψ : AddChar R R'} {a : R} {x : R} :
↑() x = ψ (a * x)
theorem AddChar.inv_mulShift {R : Type u} [] {R' : Type v} [CommRing R'] (ψ : AddChar R R') :
ψ⁻¹ =

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

theorem AddChar.mulShift_spec' {R : Type u} [] {R' : Type v} [CommRing R'] (ψ : AddChar R R') (n : ) (x : R) :
↑() x = ψ x ^ n

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

theorem AddChar.pow_mulShift {R : Type u} [] {R' : Type v} [CommRing R'] (ψ : AddChar R R') (n : ) :
ψ ^ n =

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

theorem AddChar.mulShift_mul {R : Type u} [] {R' : Type v} [CommRing R'] (ψ : AddChar R R') (a : R) (b : R) :
= AddChar.mulShift ψ (a + b)

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

@[simp]
theorem AddChar.mulShift_zero {R : Type u} [] {R' : Type v} [CommRing R'] (ψ : AddChar R R') :
= 1

mulShift ψ 0 is the trivial character.

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

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

Instances For
theorem AddChar.to_mulShift_inj_of_isPrimitive {R : Type u} [] {R' : Type v} [CommRing R'] {ψ : AddChar R R'} (hψ : ) :

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

theorem AddChar.IsNontrivial.isPrimitive {R' : Type v} [CommRing R'] {F : Type u} [] {ψ : AddChar F R'} (hψ : ) :

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

def 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.

Instances For
noncomputable def AddChar.PrimitiveAddChar.n {R : Type u} [] {R' : Type v} [Field R'] :

The first projection from PrimitiveAddChar, giving the cyclotomic field.

Instances For
noncomputable def AddChar.PrimitiveAddChar.char {R : Type u} [] {R' : Type v} [Field R'] (χ : ) :

The second projection from PrimitiveAddChar, giving the character.

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

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

### Additive characters on ZMod 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.

Instances For
theorem AddChar.zmodChar_apply {C : Type v} [] {n : ℕ+} {ζ : C} (hζ : ζ ^ n = 1) (a : ZMod n) :
↑() a = ζ ^

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 : ) :
↑() a = ζ ^ a
theorem AddChar.zmod_char_isNontrivial_iff {C : Type v} [] (n : ℕ+) (ψ : AddChar (ZMod n) C) :
ψ 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ψ : ) (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) :

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

Instances For

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

noncomputable def AddChar.primitiveCharFiniteField (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.

Instances For

### The sum of all character values #

theorem AddChar.sum_eq_zero_of_isNontrivial {R : Type u} [] {R' : Type v} [CommRing R'] [] [IsDomain R'] {ψ : AddChar R R'} (hψ : ) :
(Finset.sum Finset.univ fun a => ψ 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_is_trivial {R : Type u} [] {R' : Type v} [CommRing R'] [] {ψ : AddChar R R'} (hψ : ) :
(Finset.sum Finset.univ fun a => ψ a) = ↑()

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

theorem AddChar.sum_mulShift {R : Type u} [] {R' : Type v} [CommRing R'] [] [] [IsDomain R'] {ψ : AddChar R R'} (b : R) (hψ : ) :
(Finset.sum Finset.univ fun x => ψ (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.