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 levelnto levelm, wherendividesm.conductor: The conductor of a Dirichlet character.IsPrimitive: If the level is equal to the conductor.
Tags #
dirichlet character, multiplicative character
Definitions #
@[reducible, inline]
The type of Dirichlet characters of level n.
Instances For
theorem
DirichletCharacter.toUnitHom_eq_char'
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
{a : ZMod n}
(ha : IsUnit a)
:
theorem
DirichletCharacter.toUnitHom_inj
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ ψ : DirichletCharacter R n)
:
@[deprecated DirichletCharacter.toUnitHom_inj (since := "2024-12-29")]
theorem
DirichletCharacter.toUnitHom_eq_iff
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ ψ : DirichletCharacter R n)
:
Alias of DirichletCharacter.toUnitHom_inj.
theorem
DirichletCharacter.eval_modulus_sub
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
(x : ZMod n)
:
Changing levels #
noncomputable def
DirichletCharacter.changeLevel
{R : Type u_1}
[CommMonoidWithZero R]
{n m : ℕ}
(hm : n ∣ 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' := ⋯ }
Instances For
theorem
DirichletCharacter.changeLevel_def
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
{m : ℕ}
(hm : n ∣ m)
:
theorem
DirichletCharacter.changeLevel_injective
{R : Type u_1}
[CommMonoidWithZero R]
{n m : ℕ}
[NeZero 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}
[CommMonoidWithZero R]
{n m : ℕ}
{χ : DirichletCharacter R n}
(hm : n ∣ m)
[NeZero m]
:
@[simp]
theorem
DirichletCharacter.changeLevel_self
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
:
theorem
DirichletCharacter.changeLevel_trans
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
{m d : ℕ}
(hm : n ∣ m)
(hd : m ∣ d)
:
theorem
DirichletCharacter.changeLevel_eq_cast_of_dvd
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
{m : ℕ}
(hm : n ∣ m)
(a : (ZMod m)ˣ)
:
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) χ₀
Instances For
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)
:
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)
:
The Dirichlet character at level d through which χ factors
Equations
Instances For
theorem
DirichletCharacter.FactorsThrough.eq_changeLevel
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
{χ : DirichletCharacter R n}
{d : ℕ}
(h : χ.FactorsThrough d)
:
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)
:
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)
:
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)
:
theorem
DirichletCharacter.level_one'
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
(hn : n = 1)
:
noncomputable instance
DirichletCharacter.instUniqueOfNatNat
{R : Type u_1}
[CommMonoidWithZero R]
:
Unique (DirichletCharacter R 1)
Equations
theorem
DirichletCharacter.map_zero'
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
(hn : n ≠ 1)
:
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)
:
theorem
DirichletCharacter.factorsThrough_one_iff
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
:
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.
Instances For
theorem
DirichletCharacter.mem_conductorSet_iff
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
{x : ℕ}
:
theorem
DirichletCharacter.level_mem_conductorSet
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
:
theorem
DirichletCharacter.mem_conductorSet_dvd
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
{x : ℕ}
(hx : x ∈ χ.conductorSet)
:
noncomputable def
DirichletCharacter.conductor
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
:
The minimum natural number level n through which χ factors.
Instances For
theorem
DirichletCharacter.conductor_mem_conductorSet
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
:
theorem
DirichletCharacter.conductor_dvd_level
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
:
theorem
DirichletCharacter.factorsThrough_conductor
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
:
theorem
DirichletCharacter.conductor_ne_zero
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
(hn : n ≠ 0)
:
theorem
DirichletCharacter.conductor_one
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(hn : n ≠ 0)
:
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)
:
theorem
DirichletCharacter.conductor_eq_zero_iff_level_eq_zero
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
{χ : DirichletCharacter R n}
:
theorem
DirichletCharacter.conductor_le_conductor_mem_conductorSet
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
{χ : DirichletCharacter R n}
{d : ℕ}
(hd : d ∈ χ.conductorSet)
:
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.
Instances For
noncomputable def
DirichletCharacter.primitiveCharacter
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
:
The primitive character associated to a Dirichlet character.
Instances For
theorem
DirichletCharacter.primitiveCharacter_isPrimitive
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
:
theorem
DirichletCharacter.primitiveCharacter_one
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(hn : n ≠ 0)
:
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
Instances For
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
Instances For
theorem
DirichletCharacter.mul_def
{R : Type u_1}
[CommMonoidWithZero R]
{n m : ℕ}
{χ : DirichletCharacter R n}
{ψ : DirichletCharacter R m}
:
theorem
DirichletCharacter.primitive_mul_isPrimitive
{R : Type u_1}
[CommMonoidWithZero R]
{n : ℕ}
(χ : DirichletCharacter R n)
{m : ℕ}
(ψ : DirichletCharacter R m)
:
(χ.primitive_mul ψ).IsPrimitive
theorem
DirichletCharacter.even_or_odd
{S : Type u_2}
[CommRing S]
{m : ℕ}
(ψ : DirichletCharacter S m)
[NoZeroDivisors S]
:
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)
:
theorem
DirichletCharacter.Even.toUnitHom_eval_neg_one
{S : Type u_2}
[CommRing S]
{m : ℕ}
(ψ : DirichletCharacter S m)
(hψ : ψ.Even)
:
theorem
DirichletCharacter.Even.to_fun
{S : Type u_2}
[CommRing S]
{m : ℕ}
{χ : DirichletCharacter S m}
(hχ : χ.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.