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.

TODO

• add lemma unitsMap_surjective {n m : ℕ} (h : n ∣ m) (hm : m ≠ 0) : Function.Surjective (unitsMap h) and then

  lemma changeLevel_injective {d : ℕ} (h : d ∣ n) (hn : n ≠ 0) :
      Function.Injective (changeLevel (R := R) h)
  

  and

  lemma changeLevel_one_iff {d : ℕ} {χ : DirichletCharacter R n} {χ' : DirichletCharacter R d}
    (hdn : d ∣ n) (hn : n ≠ 0) (h : χ = changeLevel hdn χ') : χ = 1 ↔ χ' = 1
  

Tags

dirichlet character, multiplicative character

@[inline, reducible]

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 χ) (IsUnit.unit ha))

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)

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

noncomputable def DirichletCharacter.changeLevel {R : Type u_2} [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

• One or more equations did not get rendered due to their size.

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

theorem DirichletCharacter.changeLevel_self_toUnitHom {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : MulChar.toUnitHom ((DirichletCharacter.changeLevel (_ : n ∣ n)) χ) = 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 (_ : n ∣ d)) χ = (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 = χ (ZMod.cast ↑a)

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

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

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

The Dirichlet character at level d through which χ factors

Equations

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

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

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.instSubsingletonDirichletCharacterOfNatNatInstOfNatNat {R : Type u_1} [CommMonoidWithZero R] : Subsingleton (DirichletCharacter R 1)

Equations

• (_ : Subsingleton (DirichletCharacter R 1)) = (_ : Subsingleton (DirichletCharacter R 1))

noncomputable instance DirichletCharacter.instInhabitedDirichletCharacter {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} : Inhabited (DirichletCharacter R n)

Equations

• DirichletCharacter.instInhabitedDirichletCharacter = { default := 1 }

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

Equations

• DirichletCharacter.instUniqueDirichletCharacterOfNatNatInstOfNatNat = 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) : DirichletCharacter.FactorsThrough χ 1 ↔ χ = 1

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

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

Equations

• DirichletCharacter.conductorSet χ = {x : ℕ | DirichletCharacter.FactorsThrough χ x}

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

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

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

noncomputable def DirichletCharacter.conductor {R : Type u_1} [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ℤ.

Equations

• DirichletCharacter.conductor χ = sInf (DirichletCharacter.conductorSet χ)

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

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

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

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

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

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

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

theorem DirichletCharacter.conductor_le_conductor_mem_conductorSet {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} {d : ℕ} (hd : d ∈ DirichletCharacter.conductorSet χ) : DirichletCharacter.conductor χ ≤ DirichletCharacter.conductor (Classical.choose (_ : ∃ (χ₀ : DirichletCharacter R d), χ = (DirichletCharacter.changeLevel (_ : d ∣ n)) χ₀))

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

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

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

The primitive character associated to a Dirichlet character.

Equations

• One or more equations did not get rendered due to their size.

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

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 (Nat.lcm n m)

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

Equations

• DirichletCharacter.mul χ₁ χ₂ = (DirichletCharacter.changeLevel (_ : n ∣ Nat.lcm n m)) χ₁ * (DirichletCharacter.changeLevel (_ : m ∣ Nat.lcm n m)) χ₂

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

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

Equations

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

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

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

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

• DirichletCharacter.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

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

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

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

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

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

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