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.
• conductor: The conductor of a Dirichlet character.
• IsPrimitive: If the level is equal to the conductor.

Tags

dirichlet character, multiplicative character

Definitions

@[reducible, inline]

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

The type of Dirichlet characters of level n.

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

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

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

Changing levels

noncomputable def DirichletCharacter.changeLevel {R : Type u_1} [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 u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} (hm : n ∣ m) : (changeLevel hm) χ = MulChar.ofUnitHom ((MulChar.toUnitHom χ).comp (ZMod.unitsMap hm))

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

theorem DirichletCharacter.changeLevel_injective {R : Type u_1} [CommMonoidWithZero R] {n m : ℕ} [NeZero m] (hm : n ∣ m) : Function.Injective ⇑(changeLevel hm)

The changeLevel map is injective (except in the degenerate case m = 0).

@[simp]

theorem DirichletCharacter.changeLevel_eq_one_iff {R : Type u_1} [CommMonoidWithZero R] {n m : ℕ} {χ : DirichletCharacter R n} (hm : n ∣ m) [NeZero m] : (changeLevel hm) χ = 1 ↔ χ = 1

@[simp]

theorem DirichletCharacter.changeLevel_self {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : (changeLevel ⋯) χ = χ

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

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

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

def DirichletCharacter.FactorsThrough {R : Type u_1} [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.changeLevel_factorsThrough {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} (hm : n ∣ m) : ((changeLevel hm) χ).FactorsThrough n

theorem DirichletCharacter.FactorsThrough.dvd {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} {d : ℕ} (h : χ.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 u_1} [CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} {d : ℕ} (h : χ.FactorsThrough d) : DirichletCharacter R d

The Dirichlet character at level d through which χ factors

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

The fact that χ factors through χ₀ of level d

theorem DirichletCharacter.FactorsThrough.existsUnique {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} {d : ℕ} [NeZero n] (h : χ.FactorsThrough d) : ∃! χ' : DirichletCharacter R d, χ = (changeLevel ⋯) χ'

The character of level d through which χ factors is uniquely determined.

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

theorem DirichletCharacter.factorsThrough_iff_ker_unitsMap {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} {d : ℕ} [NeZero n] (hd : d ∣ n) : χ.FactorsThrough d ↔ (ZMod.unitsMap hd).ker ≤ (MulChar.toUnitHom χ).ker

A Dirichlet character χ factors through d | n iff its associated unit-group hom is trivial on the kernel of ZMod.unitsMap.

theorem DirichletCharacter.factorsThrough_gcd {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} [NeZero n] (ψ : DirichletCharacter R m) (h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ) : χ.FactorsThrough (n.gcd m)

Let χ and ψ be Dirichlet characters of level n and m respectively. Assume that they agree at level n * m. Then χ factors through gcd(n, m).

Edge cases

theorem DirichletCharacter.level_one {R : Type u_1} [CommMonoidWithZero R] (χ : DirichletCharacter R 1) : χ = 1

theorem DirichletCharacter.level_one' {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) (hn : n = 1) : χ = 1

instance DirichletCharacter.instSubsingletonOfNatNat {R : Type u_1} [CommMonoidWithZero R] : Subsingleton (DirichletCharacter R 1)

@[implicit_reducible]

noncomputable instance DirichletCharacter.instUniqueOfNatNat {R : Type u_1} [CommMonoidWithZero R] : Unique (DirichletCharacter R 1)

theorem DirichletCharacter.map_zero' {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) (hn : n ≠ 1) : χ 0 = 0

A Dirichlet character of modulus ≠ 1 maps 0 to 0.

theorem DirichletCharacter.changeLevel_one {R : Type u_1} [CommMonoidWithZero R] {n d : ℕ} (h : d ∣ n) : (changeLevel h) 1 = 1

theorem DirichletCharacter.factorsThrough_one_iff {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : χ.FactorsThrough 1 ↔ χ = 1

The conductor

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

The set of natural numbers d such that χ factors through a character of level d.

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

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

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

theorem DirichletCharacter.zero_ne_mem_conductorSet {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) (hn : n ≠ 0) : 0 ∉ χ.conductorSet

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

The minimum natural number level n through which χ factors.

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

theorem DirichletCharacter.conductor_dvd_level {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : χ.conductor ∣ n

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

theorem DirichletCharacter.conductor_ne_zero {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) (hn : n ≠ 0) : χ.conductor ≠ 0

theorem DirichletCharacter.conductor_one {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (hn : n ≠ 0) : conductor 1 = 1

The conductor of the trivial character is 1.

theorem DirichletCharacter.eq_one_iff_conductor_eq_one {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} (hn : n ≠ 0) : χ = 1 ↔ χ.conductor = 1

theorem DirichletCharacter.conductor_eq_zero_iff_level_eq_zero {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} : χ.conductor = 0 ↔ n = 0

theorem DirichletCharacter.conductor_le_conductor_mem_conductorSet {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} {d : ℕ} (hd : d ∈ χ.conductorSet) : χ.conductor ≤ (Classical.choose ⋯).conductor

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

A character is primitive if its level is equal to its conductor.

theorem DirichletCharacter.isPrimitive_def {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : χ.IsPrimitive ↔ χ.conductor = n

theorem DirichletCharacter.isPrimitive_one_level_one {R : Type u_1} [CommMonoidWithZero R] : IsPrimitive 1

theorem DirichletCharacter.isPrimitive_one_level_zero {R : Type u_1} [CommMonoidWithZero R] : IsPrimitive 1

theorem DirichletCharacter.conductor_one_dvd {R : Type u_1} [CommMonoidWithZero R] (n : ℕ) : conductor 1 ∣ n

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

The primitive character associated to a Dirichlet character.

theorem DirichletCharacter.changeLevel_primitiveCharacter {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : (changeLevel ⋯) χ.primitiveCharacter = χ

theorem DirichletCharacter.primitiveCharacter_isPrimitive {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : χ.primitiveCharacter.IsPrimitive

theorem DirichletCharacter.primitiveCharacter_one {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (hn : n ≠ 0) : primitiveCharacter 1 = 1

theorem DirichletCharacter.conductor_dvd_of_mem_conductorSet {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {d : ℕ} (hn : n ≠ 0) (hd : d ∈ χ.conductorSet) : χ.conductor ∣ d

noncomputable def DirichletCharacter.mul {R : Type u_1} [CommMonoidWithZero R] {n m : ℕ} (χ₁ : DirichletCharacter R n) (χ₂ : DirichletCharacter R m) : DirichletCharacter R (n.lcm m)

Dirichlet character associated to multiplication of Dirichlet characters, after changing both levels to the same

noncomputable def DirichletCharacter.primitive_mul {R : Type u_1} [CommMonoidWithZero R] {n m : ℕ} (χ₁ : DirichletCharacter R n) (χ₂ : DirichletCharacter R m) : DirichletCharacter R (χ₁.mul χ₂).conductor

Primitive character associated to multiplication of Dirichlet characters, after changing both levels to the same

theorem DirichletCharacter.mul_def {R : Type u_1} [CommMonoidWithZero R] {n m : ℕ} {χ : DirichletCharacter R n} {ψ : DirichletCharacter R m} : χ.primitive_mul ψ = (χ.mul ψ).primitiveCharacter

theorem DirichletCharacter.primitive_mul_isPrimitive {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} (ψ : DirichletCharacter R m) : (χ.primitive_mul ψ).IsPrimitive

def DirichletCharacter.Odd {S : Type u_2} [CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) : Prop

A Dirichlet character is odd if its value at -1 is -1.

def DirichletCharacter.Even {S : Type u_2} [CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) : Prop

A Dirichlet character is even if its value at -1 is 1.

theorem DirichletCharacter.even_or_odd {S : Type u_2} [CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) [NoZeroDivisors S] : ψ.Even ∨ ψ.Odd

theorem DirichletCharacter.not_even_and_odd {S : Type u_2} [CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) [NeZero 2] : ¬(ψ.Even ∧ ψ.Odd)

theorem DirichletCharacter.Even.not_odd {S : Type u_2} [CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) [NeZero 2] (hψ : ψ.Even) : ¬ψ.Odd

theorem DirichletCharacter.Odd.not_even {S : Type u_2} [CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) [NeZero 2] (hψ : ψ.Odd) : ¬ψ.Even

theorem DirichletCharacter.Odd.toUnitHom_eval_neg_one {S : Type u_2} [CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) (hψ : ψ.Odd) : (MulChar.toUnitHom ψ) (-1) = -1

theorem DirichletCharacter.Even.toUnitHom_eval_neg_one {S : Type u_2} [CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) (hψ : ψ.Even) : (MulChar.toUnitHom ψ) (-1) = 1

theorem DirichletCharacter.Odd.eval_neg {S : Type u_2} [CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) (x : ZMod m) (hψ : ψ.Odd) : ψ (-x) = -ψ x

theorem DirichletCharacter.Even.eval_neg {S : Type u_2} [CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) (x : ZMod m) (hψ : ψ.Even) : ψ (-x) = ψ x

theorem DirichletCharacter.Even.to_fun {S : Type u_2} [CommRing S] {m : ℕ} {χ : DirichletCharacter S m} (hχ : χ.Even) : Function.Even ⇑χ

An even Dirichlet character is an even function.

theorem DirichletCharacter.Odd.to_fun {S : Type u_2} [CommRing S] {m : ℕ} {χ : DirichletCharacter S m} (hχ : χ.Odd) : Function.Odd ⇑χ

An odd Dirichlet character is an odd function.