The character e^{2πi·} of ℚ/ℤ

Mathlib's AddCircle.toCircle is the character x ↦ e^{2πi x / T} of the real circle AddCircle (T : ℝ). Discriminant forms, finite quadratic modules and character modules take their values in the rational circle ℚ/ℤ = AddCircle (1 : ℚ) instead, and this file names the standard character of that group,

expCircle : ℚ/ℤ → ℂ,   r mod ℤ ↦ e^{2πi r},

as a Mathlib AddChar. It is faithful, so composing it with a ℚ/ℤ-valued character of a finite abelian group gives a complex character that is trivial exactly when the original one is; the orthogonality relation for such characters is the basic input of Gauss sums of finite quadratic modules.

Main declarations

• TauCeti.expCircle: the additive character r mod ℤ ↦ e^{2πi r} of AddCircle (1 : ℚ).
• TauCeti.expCircle_coe: its value on the class of a rational number.
• TauCeti.expCircle_eq_one_iff: it is faithful.
• TauCeti.expCircle_neg: its value at -x is the complex conjugate of its value at x.
• TauCeti.norm_expCircle: its values have norm one.
• TauCeti.expCircle_one_div_two and TauCeti.expCircle_one_div_four: e^{2πi/2} = -1 and e^{2πi/4} = i.
• TauCeti.isPrimitiveRoot_expCircle: its value at the class of 1 / n is a primitive n-th root of unity.
• CharacterModule.sum_expCircle: the orthogonality relation ∑ m, e^{2πi χ(m)} = if χ = 0 then #M else 0 for a ℚ/ℤ-valued character χ of a finite abelian group M.

noncomputable def TauCeti.expCircle : AddChar (AddCircle 1) ℂ

The standard character e^{2πi·} of ℚ/ℤ. The class of a rational number r is sent to e^{2πi r}; this is well defined because e^{2πi} is 1. It is the analogue for the rational circle AddCircle (1 : ℚ) of Mathlib's AddCircle.toCircle on a real circle.

Equations

• TauCeti.expCircle = { toFun := TauCeti.periodic_exp_two_pi_mul_I_ratCast✝.lift, map_zero_eq_one' := TauCeti.expCircle._proof_3✝, map_add_eq_mul' := TauCeti.expCircle._proof_4✝ }

@[simp]

theorem TauCeti.expCircle_coe (r : ℚ) : expCircle ↑r = Complex.exp (2 * ↑Real.pi * Complex.I * ↑r)

The value of expCircle on the class of a rational number r is e^{2πi r}.

@[simp]

theorem TauCeti.expCircle_eq_one_iff {x : AddCircle 1} : expCircle x = 1 ↔ x = 0

expCircle is faithful: its value is 1 only at 0.

@[simp]

theorem TauCeti.expCircle_neg (x : AddCircle 1) : expCircle (-x) = (starRingEnd ℂ) (expCircle x)

expCircle takes values on the unit circle: its value at -x is the complex conjugate of its value at x.

@[simp]

theorem TauCeti.norm_expCircle (x : AddCircle 1) : ‖expCircle x‖ = 1

expCircle takes values of norm one.

theorem TauCeti.expCircle_one_div_two : expCircle ↑(1 / 2) = -1

e^{2πi/2} = -1.

theorem TauCeti.expCircle_one_div_four : expCircle ↑(1 / 4) = Complex.I

e^{2πi/4} = i.

theorem TauCeti.isPrimitiveRoot_expCircle (n : ℕ) (hn : n ≠ 0) : IsPrimitiveRoot (expCircle ↑(1 / ↑n)) n

e^{2πi/n} is a primitive n-th root of unity: the value of expCircle at the class of 1 / n has multiplicative order n.

theorem CharacterModule.sum_expCircle {M : Type u_1} [AddCommGroup M] [Fintype M] (χ : CharacterModule M) [Decidable (χ = 0)] : ∑ m : M, TauCeti.expCircle (χ m) = if χ = 0 then ↑(Fintype.card M) else 0

Orthogonality for a ℚ/ℤ-valued character. Summing e^{2πi χ(m)} over a finite abelian group gives its order when the character χ is trivial and 0 otherwise.