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.

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

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.toCircle_eq_circleExp {N : ℕ} [NeZero N] (j : ZMod N) : toCircle j = Circle.exp (2 * Real.pi * (↑j.val / ↑N))

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

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.

noncomputable def ZMod.rootsOfUnityAddChar (n : ℕ) [NeZero n] : AddChar (ZMod n) ↥(rootsOfUnity n Circle)

ZMod.toCircle as an AddChar into rootsOfUnity n Circle.

@[simp]

theorem ZMod.rootsOfUnityAddChar_val (n : ℕ) [NeZero n] (x : ZMod n) : ↑↑((rootsOfUnityAddChar n) x) = toCircle x

noncomputable def rootsOfUnitytoCircle (n : ℕ) [NeZero n] : ↥(rootsOfUnity n ℂ) →* Circle

Interpret n-th roots of unity in ℂ as elements of the circle

noncomputable def rootsOfUnityCircleEquiv (n : ℕ) [NeZero n] : ↥(rootsOfUnity n Circle) ≃* ↥(rootsOfUnity n ℂ)

Equivalence of the nth roots of unity of the Circle with nth roots of unity of the complex numbers

instance instHasEnoughRootsOfUnityCircle (n : ℕ) [NeZero n] : HasEnoughRootsOfUnity Circle n

@[simp]

theorem rootsOfUnityCircleEquiv_apply (n : ℕ) [NeZero n] (w : ↥(rootsOfUnity n Circle)) : ↑↑((rootsOfUnityCircleEquiv n) w) = ↑↑↑w

theorem rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val (n : ℕ) [NeZero n] (j : ZMod n) : ↑↑((rootsOfUnityCircleEquiv n) ((ZMod.rootsOfUnityAddChar n) j)) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑j.val / ↑n)

theorem surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar (n : ℕ) [NeZero n] : Function.Surjective (⇑(rootsOfUnityCircleEquiv n) ∘ ⇑(ZMod.rootsOfUnityAddChar n))

theorem bijective_rootsOfUnityAddChar (n : ℕ) [NeZero n] : Function.Bijective ⇑(ZMod.rootsOfUnityAddChar n)