Documentation

Mathlib.NumberTheory.DirichletCharacter.Orthogonality

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

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

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

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.

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.

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.

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.