Additive characters valued in the unit circle

This file defines additive characters, valued in the unit circle, from either

• the ring ZMod N for any non-zero natural N,
• the additive circle ℝ / T ⬝ ℤ, for any real T.

These results are separate from Analysis.SpecialFunctions.Complex.Circle in order to reduce the imports of that file.

noncomputable def AddCircle.toCircle_addChar {T : ℝ} : AddChar (AddCircle T) Circle

The canonical map from the additive to the multiplicative circle, as an AddChar.

Equations

• AddCircle.toCircle_addChar = { toFun := AddCircle.toCircle, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }

Additive characters valued in the complex circle

noncomputable def ZMod.toCircle {N : ℕ} [NeZero N] : AddChar (ZMod N) Circle

The additive character from ZMod N to the unit circle in ℂ, sending j mod N to exp (2 * π * I * j / N).

Equations

• ZMod.toCircle = AddCircle.toCircle_addChar.compAddMonoidHom ZMod.toAddCircle

theorem ZMod.toCircle_intCast {N : ℕ} [NeZero N] (j : ℤ) : ↑(toCircle ↑j) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑j / ↑N)

theorem ZMod.toCircle_natCast {N : ℕ} [NeZero N] (j : ℕ) : ↑(toCircle ↑j) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑j / ↑N)

theorem ZMod.toCircle_apply {N : ℕ} [NeZero N] (j : ZMod N) : ↑(toCircle j) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑j.val / ↑N)

Explicit formula for toCircle j. Note that this is "evil" because it uses ZMod.val. Where possible, it is recommended to lift j to ℤ and use toCircle_intCast instead.

theorem ZMod.injective_toCircle {N : ℕ} [NeZero N] : Function.Injective ⇑toCircle

noncomputable def ZMod.stdAddChar {N : ℕ} [NeZero N] : AddChar (ZMod N) ℂ

The additive character from ZMod N to ℂ, sending j mod N to exp (2 * π * I * j / N).

Equations

• ZMod.stdAddChar = Circle.coeHom.compAddChar ZMod.toCircle

theorem ZMod.stdAddChar_coe {N : ℕ} [NeZero N] (j : ℤ) : stdAddChar ↑j = Complex.exp (2 * ↑Real.pi * Complex.I * ↑j / ↑N)

theorem ZMod.stdAddChar_apply {N : ℕ} [NeZero N] (j : ZMod N) : stdAddChar j = ↑(toCircle j)

theorem ZMod.injective_stdAddChar {N : ℕ} [NeZero N] : Function.Injective ⇑stdAddChar

theorem ZMod.isPrimitive_stdAddChar (N : ℕ) [NeZero N] : stdAddChar.IsPrimitive

The standard additive character ZMod N → ℂ is primitive.