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

additive character

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

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

Equations

• ψ.IsPrimitive = ∀ (a : R), a ≠ 0 → (ψ.mulShift a).IsNontrivial

theorem AddChar.to_mulShift_inj_of_isPrimitive {R : Type u} [CommRing R] {R' : Type v} [CommMonoid R'] {ψ : 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.IsNontrivial.isPrimitive {R' : Type v} [CommMonoid R'] {F : Type u} [Field F] {ψ : AddChar F R'} (hψ : ψ.IsNontrivial) : ψ.IsPrimitive

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

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

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

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

• AddChar.PrimitiveAddChar R R' = ((n : ℕ+) × (char : AddChar R (CyclotomicField n R')) ×' char.IsPrimitive)

noncomputable def AddChar.PrimitiveAddChar.n {R : Type u} [CommRing R] {R' : Type v} [Field R'] : AddChar.PrimitiveAddChar R R' → ℕ+

The first projection from PrimitiveAddChar, giving the cyclotomic field.

Equations

• χ.n = χ.fst

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

The second projection from PrimitiveAddChar, giving the character.

Equations

• χ.char = χ.snd.fst

theorem AddChar.PrimitiveAddChar.prim {R : Type u} [CommRing R] {R' : Type v} [Field R'] (χ : AddChar.PrimitiveAddChar R R') : χ.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} [CommRing R] (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} [CommMonoid C] (n : ℕ+) {ζ : C} (hζ : ζ ^ ↑n = 1) : AddChar (ZMod ↑n) C

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

Equations

• AddChar.zmodChar n hζ = { toFun := fun (a : ZMod ↑n) => ζ ^ a.val, map_zero_one' := ⋯, map_add_mul' := ⋯ }

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

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

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

theorem AddChar.zmod_char_isNontrivial_iff {C : Type v} [CommMonoid C] (n : ℕ+) (ψ : AddChar (ZMod ↑n) C) : ψ.IsNontrivial ↔ ψ 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} [CommMonoid C] (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} [CommMonoid C] (n : ℕ) (ψ : AddChar (ZMod n) C) (hψ : ∀ (a : ZMod n), ψ a = 1 → a = 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} [CommMonoid C] (n : ℕ+) {ζ : C} (h : IsPrimitiveRoot ζ ↑n) : (AddChar.zmodChar n ⋯).IsPrimitive

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) : AddChar.PrimitiveAddChar (ZMod ↑n) F'

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

Equations

• AddChar.primitiveZModChar n F' h = ⟨n, ⟨AddChar.zmodChar n ⋯, ⋯⟩⟩

Existence of a primitive additive character on a finite field

noncomputable def AddChar.primitiveCharFiniteField (F : Type u_1) (F' : Type u_2) [Field F] [Finite F] [Field F'] (h : ringChar F' ≠ ringChar F) : AddChar.PrimitiveAddChar 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

• One or more equations did not get rendered due to their size.

The sum of all character values

theorem AddChar.sum_eq_zero_of_isNontrivial {R : Type u_1} [AddGroup R] [Fintype R] {R' : Type u_2} [CommRing R'] [IsDomain R'] {ψ : AddChar R R'} (hψ : ψ.IsNontrivial) : (Finset.univ.sum fun (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_is_trivial {R : Type u_1} [AddGroup R] [Fintype R] {R' : Type u_2} [CommRing R'] {ψ : AddChar R R'} (hψ : ¬ψ.IsNontrivial) : (Finset.univ.sum fun (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} [CommRing R] [Fintype R] [DecidableEq R] {R' : Type u_2} [CommRing R'] [IsDomain R'] {ψ : AddChar R R'} (b : R) (hψ : ψ.IsPrimitive) : (Finset.univ.sum fun (x : R) => ψ (x * b)) = ↑(if b = 0 then Fintype.card R else 0)

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