Dirichlet Characters

Let R be a commutative monoid with zero. A Dirichlet character χ of level n over R is a multiplicative character from ZMod n to R sending non-units to 0. We then obtain some properties of toUnitHom χ, the restriction of χ to a group homomorphism (ZMod n)ˣ →* Rˣ.

Main definitions:

• DirichletCharacter: The type representing a Dirichlet character.
• changeLevel: Extend the Dirichlet character χ of level n to level m, where n divides m.

TODO

• properties of the conductor

Tags

dirichlet character, multiplicative character

@[inline, reducible]

abbrev DirichletCharacter (R : Type) [CommMonoidWithZero R] (n : ℕ) : Type

The type of Dirichlet characters of level n.

theorem DirichletCharacter.toUnitHom_eq_char' {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {a : ZMod n} (ha : IsUnit a) : ↑χ a = ↑(↑(MulChar.toUnitHom χ) (IsUnit.unit ha))

theorem DirichletCharacter.toUnitHom_eq_iff {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) (ψ : DirichletCharacter R n) : MulChar.toUnitHom χ = MulChar.toUnitHom ψ ↔ χ = ψ

theorem DirichletCharacter.eval_modulus_sub {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) (x : ZMod n) : ↑χ (↑n - x) = ↑χ (-x)

theorem DirichletCharacter.periodic {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} (hm : n ∣ m) : Function.Periodic ↑χ ↑m

noncomputable def DirichletCharacter.changeLevel {R : Type} [CommMonoidWithZero R] {n : ℕ} {m : ℕ} (hm : n ∣ m) : DirichletCharacter R n →* DirichletCharacter R m

A function that modifies the level of a Dirichlet character to some multiple of its original level.

theorem DirichletCharacter.changeLevel_def {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} (hm : n ∣ m) : ↑(DirichletCharacter.changeLevel hm) χ = MulChar.ofUnitHom (MonoidHom.comp (MulChar.toUnitHom χ) (ZMod.unitsMap hm))

theorem DirichletCharacter.changeLevel_def' {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} (hm : n ∣ m) : MulChar.toUnitHom (↑(DirichletCharacter.changeLevel hm) χ) = MonoidHom.comp (MulChar.toUnitHom χ) (ZMod.unitsMap hm)

@[simp]

theorem DirichletCharacter.changeLevel_self {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : ↑(DirichletCharacter.changeLevel (_ : n ∣ n)) χ = χ

theorem DirichletCharacter.changeLevel_self_toUnitHom {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : MulChar.toUnitHom (↑(DirichletCharacter.changeLevel (_ : n ∣ n)) χ) = MulChar.toUnitHom χ

theorem DirichletCharacter.changeLevel_trans {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} {d : ℕ} (hm : n ∣ m) (hd : m ∣ d) : ↑(DirichletCharacter.changeLevel (_ : n ∣ d)) χ = ↑(DirichletCharacter.changeLevel hd) (↑(DirichletCharacter.changeLevel hm) χ)

theorem DirichletCharacter.changeLevel_eq_cast_of_dvd {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} (hm : n ∣ m) (a : (ZMod m)ˣ) : ↑(↑(DirichletCharacter.changeLevel hm) χ) ↑a = ↑χ ↑↑a

def DirichletCharacter.FactorsThrough {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) (d : ℕ) : Prop

χ of level n factors through a Dirichlet character χ₀ of level d if d ∣ n and χ₀ = χ ∘ (ZMod n → ZMod d).

theorem DirichletCharacter.FactorsThrough.dvd {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {d : ℕ} (h : DirichletCharacter.FactorsThrough χ d) : d ∣ n

The fact that d divides n when χ factors through a Dirichlet character at level d

noncomputable def DirichletCharacter.FactorsThrough.χ₀ {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {d : ℕ} (h : DirichletCharacter.FactorsThrough χ d) : DirichletCharacter R d

The Dirichlet character at level d through which χ factors

theorem DirichletCharacter.FactorsThrough.eq_changeLevel {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {d : ℕ} (h : DirichletCharacter.FactorsThrough χ d) : χ = ↑(DirichletCharacter.changeLevel (_ : d ∣ n)) (DirichletCharacter.FactorsThrough.χ₀ χ h)

The fact that χ factors through χ₀ of level d

theorem DirichletCharacter.FactorsThrough.same_level {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : DirichletCharacter.FactorsThrough χ n

def DirichletCharacter.conductorSet {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : Set ℕ

The set of natural numbers for which a Dirichlet character is periodic.

theorem DirichletCharacter.mem_conductorSet_iff {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {x : ℕ} : x ∈ DirichletCharacter.conductorSet χ ↔ DirichletCharacter.FactorsThrough χ x

theorem DirichletCharacter.level_mem_conductorSet {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : n ∈ DirichletCharacter.conductorSet χ

theorem DirichletCharacter.mem_conductorSet_dvd {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {x : ℕ} (hx : x ∈ DirichletCharacter.conductorSet χ) : x ∣ n

noncomputable def DirichletCharacter.conductor {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : ℕ

The minimum natural number n for which a Dirichlet character is periodic. The Dirichlet character χ can then alternatively be reformulated on ℤ/nℤ.