Orthogonality relations for Dirichlet characters

Let n be a positive natural number. The main result of this file is DirichletCharacter.sum_char_inv_mul_char_eq, which says that when a : ZMod n is a unit and b : ZMod n, then the sum ∑ χ : DirichletCharacter R n, χ a⁻¹ * χ b vanishes when a ≠ b and has the value n.totient otherwise. This requires R to have enough roots of unity (e.g., R could be an algebraically closed field of characteristic zero).

noncomputable instance DirichletCharacter.fintype {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} : Fintype (DirichletCharacter R n)

Equations

• DirichletCharacter.fintype = Fintype.ofFinite (DirichletCharacter R n)

theorem DirichletCharacter.mulEquiv_units (R : Type u_1) [CommRing R] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] : Nonempty (DirichletCharacter R n ≃* (ZMod n)ˣ)

The group of Dirichlet characters mod n with values in a ring R that has enough roots of unity is (noncanonically) isomorphic to (ZMod n)ˣ.

theorem DirichletCharacter.card_eq_totient_of_hasEnoughRootsOfUnity (R : Type u_1) [CommRing R] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] : Nat.card (DirichletCharacter R n) = n.totient

There are n.totient Dirichlet characters mod n with values in a ring that has enough roots of unity.

theorem DirichletCharacter.exists_apply_ne_one_of_hasEnoughRootsOfUnity (R : Type u_1) [CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [Nontrivial R] ⦃a : ZMod n⦄ (ha : a ≠ 1) : ∃ (χ : DirichletCharacter R n), χ a ≠ 1

If R is a ring that has enough roots of unity and n ≠ 0, then for each a ≠ 1 in ZMod n, there exists a Dirichlet character χ mod n with values in R such that χ a ≠ 1.

theorem DirichletCharacter.sum_characters_eq_zero (R : Type u_1) [CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [IsDomain R] ⦃a : ZMod n⦄ (ha : a ≠ 1) : ∑ χ : DirichletCharacter R n, χ a = 0

If R is an integral domain that has enough roots of unity and n ≠ 0, then for each a ≠ 1 in ZMod n, the sum of χ a over all Dirichlet characters mod n with values in R vanishes.

theorem DirichletCharacter.sum_characters_eq (R : Type u_1) [CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [IsDomain R] (a : ZMod n) : ∑ χ : DirichletCharacter R n, χ a = if a = 1 then ↑n.totient else 0

If R is an integral domain that has enough roots of unity and n ≠ 0, then for a in ZMod n, the sum of χ a over all Dirichlet characters mod n with values in R vanishes if a ≠ 1 and has the value n.totient if a = 1.

theorem DirichletCharacter.sum_char_inv_mul_char_eq (R : Type u_1) [CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [IsDomain R] {a : ZMod n} (ha : IsUnit a) (b : ZMod n) : ∑ χ : DirichletCharacter R n, χ a⁻¹ * χ b = if a = b then ↑n.totient else 0

If R is an integral domain that has enough roots of unity and n ≠ 0, then for a and b in ZMod n with a a unit, the sum of χ a⁻¹ * χ b over all Dirichlet characters mod n with values in R vanishes if a ≠ b and has the value n.totient if a = b.