Documentation

Mathlib.NumberTheory.DirichletCharacter.Basic

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

MulChar.toUnitHom χ = MulChar.toUnitHom ψ ↔ χ = ψ

@[deprecated DirichletCharacter.toUnitHom_inj (since := "2024-12-29")]

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

MulChar.toUnitHom χ = MulChar.toUnitHom ψ ↔ χ = ψ

Alias of DirichletCharacter.toUnitHom_inj.

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

(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 : ℕ) :

χ 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) :

((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) :

χ = (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.

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)

noncomputable instance DirichletCharacter.instUniqueOfNatNat {R : Type u_1} [CommMonoidWithZero R] :

Unique (DirichletCharacter R 1)

Equations

DirichletCharacter.instUniqueOfNatNat = Unique.mk' (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) :

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

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

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] :

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

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.

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

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

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

Equations

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

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

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

Equations

ψ.Even = (ψ (-1) = 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) :

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

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.