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

theorem AddChar.val_mem_rootsOfUnity {R : Type u} [CommRing R] {R' : Type v} [CommMonoid R'] (φ : AddChar R R') (a : R) (h : 0 < ringChar R) : ⋯.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} [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 ≠ 1

theorem AddChar.IsPrimitive.compMulHom_of_isPrimitive {R : Type u} [CommRing R] {R' : Type v} [CommMonoid R'] {R'' : Type u_1} [CommMonoid R''] {φ : AddChar R R'} {f : R' →* R''} (hφ : φ.IsPrimitive) (hf : Function.Injective ⇑f) : (f.compAddChar φ).IsPrimitive

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} [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.IsPrimitive.of_ne_one {R' : Type v} [CommMonoid R'] {F : Type u} [Field F] {ψ : 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} [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.

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

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

Additive characters on ZMod n

theorem AddChar.exists_divisor_of_not_isPrimitive {N : ℕ} [NeZero 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 : ℕ) [NeZero 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_eq_one' := ⋯, map_add_eq_mul' := ⋯ }

theorem AddChar.zmodChar_apply {C : Type v} [CommMonoid C] {n : ℕ} [NeZero 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 : ℕ} [NeZero n] {ζ : C} (hζ : ζ ^ n = 1) (a : ℕ) : (AddChar.zmodChar n hζ) ↑a = ζ ^ a

theorem AddChar.zmod_char_ne_one_iff {C : Type v} [CommMonoid C] (n : ℕ) [NeZero 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} [CommMonoid C] (n : ℕ) [NeZero 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 : ℕ) [NeZero 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 := n, char := AddChar.zmodChar ↑n ⋯, prim := ⋯ }

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] [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.

@[deprecated AddChar.FiniteField.primitiveChar]

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'

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

• AddChar.primitiveCharFiniteField = AddChar.FiniteField.primitiveChar

The sum of all character values

theorem AddChar.sum_eq_zero_of_ne_one {R : Type u_1} [AddGroup R] [Fintype R] {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} [AddGroup R] [Fintype R] {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} [CommRing R] [Fintype R] [DecidableEq R] {R' : Type u_2} [CommRing R'] [IsDomain R'] {ψ : AddChar R R'} (b : R) (hψ : ψ.IsPrimitive) : ∑ 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.

Complex-valued additive characters

theorem AddChar.starComp_eq_inv {R : Type u_1} [CommRing R] (hR : 0 < ringChar R) {φ : AddChar R ℂ} : (↑(starRingEnd ℂ)).compAddChar φ = φ⁻¹

Post-composing an additive character to ℂ with complex conjugation gives the inverse character.

theorem AddChar.starComp_apply {R : Type u_1} [CommRing R] (hR : 0 < ringChar R) {φ : AddChar R ℂ} (a : R) : (starRingEnd ℂ) (φ a) = φ⁻¹ a

noncomputable def AddChar.FiniteField.primitiveChar_to_Complex (F : Type u_1) [Field F] [Finite F] : AddChar F ℂ

A primitive additive character on the finite field F with values in ℂ.

Equations

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

theorem AddChar.FiniteField.primitiveChar_to_Complex_isPrimitive (F : Type u_1) [Field F] [Finite F] : (AddChar.FiniteField.primitiveChar_to_Complex F).IsPrimitive