# 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) (n : ) :
Type u_1

The type of Dirichlet characters of level n.

Equations
Instances For
theorem DirichletCharacter.toUnitHom_eq_char' {R : Type u_1} {n : } (χ : ) {a : ZMod n} (ha : ) :
χ a = ( ha.unit)
theorem DirichletCharacter.toUnitHom_eq_iff {R : Type u_1} {n : } (χ : ) (ψ : ) :
χ = ψ
theorem DirichletCharacter.eval_modulus_sub {R : Type u_1} {n : } (χ : ) (x : ZMod n) :
χ (n - x) = χ (-x)

### Changing levels #

noncomputable def DirichletCharacter.changeLevel {R : Type u_1} {n : } {m : } (hm : n m) :

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

Equations
• = { toFun := fun (ψ : ) => MulChar.ofUnitHom (.comp ()), map_one' := , map_mul' := }
Instances For
theorem DirichletCharacter.changeLevel_def {R : Type u_1} {n : } (χ : ) {m : } (hm : n m) :
= MulChar.ofUnitHom (.comp ())
theorem DirichletCharacter.changeLevel_toUnitHom {R : Type u_1} {n : } (χ : ) {m : } (hm : n m) :
= .comp ()
theorem DirichletCharacter.changeLevel_injective {R : Type u_1} {n : } {m : } [] (hm : n m) :

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

@[simp]
theorem DirichletCharacter.changeLevel_eq_one_iff {R : Type u_1} {n : } {m : } {χ : } (hm : n m) [] :
= 1 χ = 1
@[simp]
theorem DirichletCharacter.changeLevel_self {R : Type u_1} {n : } (χ : ) :
theorem DirichletCharacter.changeLevel_trans {R : Type u_1} {n : } (χ : ) {m : } {d : } (hm : n m) (hd : m d) :
theorem DirichletCharacter.changeLevel_eq_cast_of_dvd {R : Type u_1} {n : } (χ : ) {m : } (hm : n m) (a : (ZMod m)ˣ) :
() a = χ (a).cast
def DirichletCharacter.FactorsThrough {R : Type u_1} {n : } (χ : ) (d : ) :

χ 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) (χ₀ : ), χ =
Instances For
theorem DirichletCharacter.changeLevel_factorsThrough {R : Type u_1} {n : } (χ : ) {m : } (hm : n m) :
().FactorsThrough n
theorem DirichletCharacter.FactorsThrough.dvd {R : Type u_1} {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} {n : } {χ : } {d : } (h : χ.FactorsThrough d) :

The Dirichlet character at level d through which χ factors

Equations
• h.χ₀ =
Instances For
theorem DirichletCharacter.FactorsThrough.eq_changeLevel {R : Type u_1} {n : } {χ : } {d : } (h : χ.FactorsThrough d) :
χ = h.χ₀

The fact that χ factors through χ₀ of level d

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

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

theorem DirichletCharacter.FactorsThrough.same_level {R : Type u_1} {n : } (χ : ) :
χ.FactorsThrough n
theorem DirichletCharacter.factorsThrough_iff_ker_unitsMap {R : Type u_1} {n : } {χ : } {d : } [] (hd : d n) :
χ.FactorsThrough d ().ker .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} (χ : ) :
χ = 1
theorem DirichletCharacter.level_one' {R : Type u_1} {n : } (χ : ) (hn : n = 1) :
χ = 1
Equations
• =
noncomputable instance DirichletCharacter.instUniqueOfNatNat {R : Type u_1} :
Equations
• DirichletCharacter.instUniqueOfNatNat =
theorem DirichletCharacter.changeLevel_one {R : Type u_1} {n : } {d : } (h : d n) :
theorem DirichletCharacter.factorsThrough_one_iff {R : Type u_1} {n : } (χ : ) :
χ.FactorsThrough 1 χ = 1

### The conductor #

def DirichletCharacter.conductorSet {R : Type u_1} {n : } (χ : ) :

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

Equations
• χ.conductorSet = {d : | χ.FactorsThrough d}
Instances For
theorem DirichletCharacter.mem_conductorSet_iff {R : Type u_1} {n : } (χ : ) {x : } :
x χ.conductorSet χ.FactorsThrough x
theorem DirichletCharacter.level_mem_conductorSet {R : Type u_1} {n : } (χ : ) :
n χ.conductorSet
theorem DirichletCharacter.mem_conductorSet_dvd {R : Type u_1} {n : } (χ : ) {x : } (hx : x χ.conductorSet) :
x n
noncomputable def DirichletCharacter.conductor {R : Type u_1} {n : } (χ : ) :

The minimum natural number level n through which χ factors.

Equations
• χ.conductor = sInf χ.conductorSet
Instances For
theorem DirichletCharacter.conductor_mem_conductorSet {R : Type u_1} {n : } (χ : ) :
χ.conductor χ.conductorSet
theorem DirichletCharacter.conductor_dvd_level {R : Type u_1} {n : } (χ : ) :
χ.conductor n
theorem DirichletCharacter.factorsThrough_conductor {R : Type u_1} {n : } (χ : ) :
χ.FactorsThrough χ.conductor
theorem DirichletCharacter.conductor_ne_zero {R : Type u_1} {n : } (χ : ) (hn : n 0) :
χ.conductor 0
theorem DirichletCharacter.conductor_one {R : Type u_1} {n : } (hn : n 0) :

The conductor of the trivial character is 1.

theorem DirichletCharacter.eq_one_iff_conductor_eq_one {R : Type u_1} {n : } {χ : } (hn : n 0) :
χ = 1 χ.conductor = 1
theorem DirichletCharacter.conductor_eq_zero_iff_level_eq_zero {R : Type u_1} {n : } {χ : } :
χ.conductor = 0 n = 0
theorem DirichletCharacter.conductor_le_conductor_mem_conductorSet {R : Type u_1} {n : } {χ : } {d : } (hd : d χ.conductorSet) :
χ.conductor ().conductor
def DirichletCharacter.isPrimitive {R : Type u_1} {n : } (χ : ) :

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

Equations
• χ.isPrimitive = (χ.conductor = n)
Instances For
theorem DirichletCharacter.isPrimitive_def {R : Type u_1} {n : } (χ : ) :
χ.isPrimitive χ.conductor = n
noncomputable def DirichletCharacter.primitiveCharacter {R : Type u_1} {n : } (χ : ) :
DirichletCharacter R χ.conductor

The primitive character associated to a Dirichlet character.

Equations
• χ.primitiveCharacter =
Instances For
theorem DirichletCharacter.primitiveCharacter_isPrimitive {R : Type u_1} {n : } (χ : ) :
χ.primitiveCharacter.isPrimitive
theorem DirichletCharacter.primitiveCharacter_one {R : Type u_1} {n : } (hn : n 0) :
noncomputable def DirichletCharacter.mul {R : Type u_1} {n : } {m : } (χ₁ : ) (χ₂ : ) :
DirichletCharacter R (n.lcm m)

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

Equations
• χ₁.mul χ₂ =
Instances For
noncomputable def DirichletCharacter.primitive_mul {R : Type u_1} {n : } {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
Instances For
theorem DirichletCharacter.mul_def {R : Type u_1} {n : } {m : } {χ : } {ψ : } :
χ.primitive_mul ψ = (χ.mul ψ).primitiveCharacter
theorem DirichletCharacter.isPrimitive.primitive_mul {R : Type u_1} {n : } (χ : ) {m : } (ψ : ) :
(χ.primitive_mul ψ).isPrimitive
def DirichletCharacter.Odd {S : Type} [] {m : } (ψ : ) :

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

Equations
• ψ.Odd = (ψ (-1) = -1)
Instances For
def DirichletCharacter.Even {S : Type} [] {m : } (ψ : ) :

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

Equations
• ψ.Even = (ψ (-1) = 1)
Instances For
theorem DirichletCharacter.even_or_odd {S : Type} [] {m : } (ψ : ) [] :
ψ.Even ψ.Odd
theorem DirichletCharacter.Odd.toUnitHom_eval_neg_one {S : Type} [] {m : } (ψ : ) (hψ : ψ.Odd) :
(-1) = -1
theorem DirichletCharacter.Even.toUnitHom_eval_neg_one {S : Type} [] {m : } (ψ : ) (hψ : ψ.Even) :
(-1) = 1
theorem DirichletCharacter.Odd.eval_neg {S : Type} [] {m : } (ψ : ) (x : ZMod m) (hψ : ψ.Odd) :
ψ (-x) = -ψ x
theorem DirichletCharacter.Even.eval_neg {S : Type} [] {m : } (ψ : ) (x : ZMod m) (hψ : ψ.Even) :
ψ (-x) = ψ x