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.

Equations

• DirichletCharacter R n = MulChar (ZMod n) R

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_eq_iff {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter 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.

Equations

• DirichletCharacter.changeLevel hm = { toFun := fun (ψ : DirichletCharacter R n) => MulChar.ofUnitHom ((MulChar.toUnitHom ψ).comp (ZMod.unitsMap hm)), map_one' := ⋯, map_mul' := ⋯ }

theorem DirichletCharacter.changeLevel_def {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} (hm : n ∣ m) : (DirichletCharacter.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 ((DirichletCharacter.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 ⇑(DirichletCharacter.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] : (DirichletCharacter.changeLevel hm) χ = 1 ↔ χ = 1

@[simp]

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

theorem DirichletCharacter.changeLevel_self_toUnitHom {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : MulChar.toUnitHom ((DirichletCharacter.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) : (DirichletCharacter.changeLevel ⋯) χ = (DirichletCharacter.changeLevel hd) ((DirichletCharacter.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)ˣ) : ((DirichletCharacter.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).

Equations

• χ.FactorsThrough d = ∃ (h : d ∣ n) (χ₀ : DirichletCharacter R d), χ = (DirichletCharacter.changeLevel h) χ₀

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

Equations

• h.χ₀ = Classical.choose ⋯

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

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)

Equations

• ⋯ = ⋯

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

Equations

• DirichletCharacter.instUniqueOfNatNat = Unique.mk' (DirichletCharacter R 1)

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

Equations

• χ.conductorSet = {d : ℕ | χ.FactorsThrough 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

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

The minimum natural number level n through which χ factors.

Equations

• χ.conductor = sInf χ.conductorSet

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

Equations

• χ.isPrimitive = (χ.conductor = n)

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] : DirichletCharacter.isPrimitive 1

theorem DirichletCharacter.isPritive_one_level_zero {R : Type u_1} [CommMonoidWithZero R] : DirichletCharacter.isPrimitive 1

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

Equations

• χ.primitiveCharacter = Classical.choose ⋯

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) : DirichletCharacter.primitiveCharacter 1 = 1

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

Equations

• χ₁.mul χ₂ = (DirichletCharacter.changeLevel ⋯) χ₁ * (DirichletCharacter.changeLevel ⋯) χ₂

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

Equations

• χ₁.primitive_mul χ₂ = (χ₁.mul χ₂).primitiveCharacter

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

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

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

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

Equations

• ψ.Odd = (ψ (-1) = -1)

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

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

Equations

• ψ.Even = (ψ (-1) = 1)

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

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

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

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

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