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

additive character

Definitions related to and results on additive characters

def AddChar (R : Type u) [AddMonoid R] (R' : Type v) [CommMonoid R'] : 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').

Equations

• AddChar R R' = (Multiplicative R →* R')

instance AddChar.instCommMonoidAddChar (R : Type u) [AddMonoid R] (R' : Type v) [CommMonoid R'] : CommMonoid (AddChar R R')

Equations

• AddChar.instCommMonoidAddChar R R' = inferInstanceAs (CommMonoid (Multiplicative R →* R'))

instance AddChar.instInhabitedAddChar (R : Type u) [AddMonoid R] (R' : Type v) [CommMonoid R'] : Inhabited (AddChar R R')

Equations

• AddChar.instInhabitedAddChar R R' = inferInstanceAs (Inhabited (Multiplicative R →* R'))

def AddChar.toMonoidHom {R : Type u} [AddMonoid R] {R' : Type v} [CommMonoid R'] : AddChar R R' → Multiplicative R →* R'

Interpret an additive character as a monoid homomorphism.

Equations

• AddChar.toMonoidHom = id

def AddChar.toFun {R : Type u} [AddMonoid R] {R' : Type v} [CommMonoid R'] (ψ : AddChar R R') (x : R) : R'

Equations

• ↑ψ x = ↑(AddChar.toMonoidHom ψ) (↑Multiplicative.ofAdd x)

instance AddChar.hasCoeToFun {R : Type u} [AddMonoid R] {R' : Type v} [CommMonoid R'] : CoeFun (AddChar R R') fun x => 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 ofAdd a when we want to apply an additive character.

Equations

• AddChar.hasCoeToFun = { coe := AddChar.toFun }

theorem AddChar.coe_to_fun_apply {R : Type u} [AddMonoid R] {R' : Type v} [CommMonoid R'] (ψ : AddChar R R') (a : R) : ↑ψ a = ↑(AddChar.toMonoidHom ψ) (↑Multiplicative.ofAdd a)

theorem AddChar.mul_apply {R : Type u} [AddMonoid R] {R' : Type v} [CommMonoid R'] (ψ : AddChar R R') (φ : AddChar R R') (a : R) : ↑(ψ * φ) a = ↑ψ a * ↑φ a

@[simp]

theorem AddChar.one_apply {R : Type u} [AddMonoid R] {R' : Type v} [CommMonoid R'] (a : R) : ↑1 a = 1

instance AddChar.monoidHomClass {R : Type u} [AddMonoid R] {R' : Type v} [CommMonoid R'] : MonoidHomClass (AddChar R R') (Multiplicative R) R'

Equations

• AddChar.monoidHomClass = MonoidHom.monoidHomClass

theorem AddChar.ext {R : Type u} [AddMonoid R] {R' : Type v} [CommMonoid R'] (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} [AddMonoid R] {R' : Type v} [CommMonoid R'] (ψ : AddChar R R') : ↑ψ 0 = 1

An additive character maps 0 to 1.

@[simp]

theorem AddChar.map_add_mul {R : Type u} [AddMonoid R] {R' : Type v} [CommMonoid R'] (ψ : 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} [AddMonoid R] {R' : Type v} [CommMonoid R'] (ψ : 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} [AddCommGroup R] {R' : Type v} [CommMonoid R'] : Inv (AddChar R R')

An additive character on a commutative additive group has an inverse.

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

Equations

• AddChar.hasInv = { inv := fun ψ => MonoidHom.comp ψ invMonoidHom }

theorem AddChar.inv_apply {R : Type u} [AddCommGroup R] {R' : Type v} [CommMonoid R'] (ψ : AddChar R R') (x : R) : ↑ψ⁻¹ x = ↑ψ (-x)

@[simp]

theorem AddChar.map_zsmul_zpow {R : Type u} [AddCommGroup R] {R' : Type v} [CommGroup R'] (ψ : 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} [AddCommGroup R] {R' : Type v} [CommMonoid R'] : CommGroup (AddChar R R')

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

Equations

• AddChar.commGroup = let src := MonoidHom.commMonoid; CommGroup.mk (_ : ∀ (a b : Multiplicative R →* R'), a * b = b * a)

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

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

Equations

• AddChar.IsNontrivial ψ = ∃ a, ↑ψ a ≠ 1

theorem AddChar.isNontrivial_iff_ne_trivial {R : Type u} [CommRing R] {R' : Type v} [CommRing R'] (ψ : AddChar R R') : AddChar.IsNontrivial ψ ↔ ψ ≠ 1

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

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

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

Equations

• AddChar.mulShift ψ a = MonoidHom.comp ψ (↑AddMonoidHom.toMultiplicative (AddMonoidHom.mulLeft a))

@[simp]

theorem AddChar.mulShift_apply {R : Type u} [CommRing R] {R' : Type v} [CommRing R'] {ψ : AddChar R R'} {a : R} {x : R} : ↑(AddChar.mulShift ψ a) x = ↑ψ (a * x)

theorem AddChar.inv_mulShift {R : Type u} [CommRing R] {R' : Type v} [CommRing R'] (ψ : AddChar R R') : ψ⁻¹ = AddChar.mulShift ψ (-1)

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

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

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

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

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

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

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

@[simp]

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

mulShift ψ 0 is the trivial character.

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

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

Equations

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

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

When R is a field F, then a nontrivial additive character is 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')) ×' AddChar.IsPrimitive char)

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

• AddChar.PrimitiveAddChar.n χ = χ.fst

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

The second projection from PrimitiveAddChar, giving the character.

Equations

• AddChar.PrimitiveAddChar.char χ = χ.snd.fst

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

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

Additive characters on ZMod n

def AddChar.zmodChar {C : Type v} [CommRing 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

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

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

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

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

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

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

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

Existence of a primitive additive character on a finite field

noncomputable def AddChar.primitiveCharFiniteField (F : Type u_1) (F' : Type u_2) [Field F] [Fintype 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} [CommRing R] {R' : Type v} [CommRing R'] [Fintype R] [IsDomain R'] {ψ : AddChar R R'} (hψ : AddChar.IsNontrivial ψ) : (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} [CommRing R] {R' : Type v} [CommRing R'] [Fintype R] {ψ : AddChar R R'} (hψ : ¬AddChar.IsNontrivial ψ) : (Finset.sum Finset.univ fun a => ↑ψ 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} [CommRing R] {R' : Type v} [CommRing R'] [Fintype R] [DecidableEq R] [IsDomain R'] {ψ : AddChar R R'} (b : R) (hψ : AddChar.IsPrimitive ψ) : (Finset.sum Finset.univ fun x => ↑ψ (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.