The conductor of a finite-order Hecke character

A finite-order Hecke character χ of a number field K is the pullback of a ray class character of some modulus (HeckeCharacter.isFiniteOrder_iff_exists_rayClassCharacter), and the moduli that occur are closed under taking multiples. They are also closed under greatest common divisors: χ comes from 𝔪 exactly when it is trivial on raySubgroup 𝔪, and the ray subgroup of 𝔪.gcd 𝔫 is generated by those of 𝔪 and 𝔫 (raySubgroup_gcd). Hence there is a least such modulus, the conductor of χ: χ comes from a ray class character of 𝔪 exactly when the conductor divides 𝔪.

Since the characters coming from a fixed modulus form a subgroup, the conductor is unchanged by inversion, the conductor of a power divides the conductor, and the conductor of a product divides the least common multiple of the conductors.

The conductor of a ray class character, and the primitive character inducing it, are built from this one in TauCeti.NumberTheory.NumberField.Global.RayClass.Character.Conductor.

Main definitions

• TauCeti.GlobalNumberFields.HeckeCharacter.conductor: the least modulus from which a finite-order Hecke character comes.

Main results

• TauCeti.GlobalNumberFields.HeckeCharacter.conductor_dvd_iff: a finite-order Hecke character comes from a ray class character of 𝔪 exactly when its conductor divides 𝔪.
• TauCeti.GlobalNumberFields.HeckeCharacter.conductor_inv, TauCeti.GlobalNumberFields.HeckeCharacter.conductor_zpow_dvd, and TauCeti.GlobalNumberFields.HeckeCharacter.conductor_mul_dvd_lcm_conductor: the conductor and the group operations.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §1 and Chapter VII, §6.
• The API follows Mathlib's conductor of Dirichlet characters, Mathlib.NumberTheory.DirichletCharacter.Basic (DirichletCharacter.conductor, DirichletCharacter.primitiveCharacter).

noncomputable def TauCeti.GlobalNumberFields.HeckeCharacter.conductor {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) (hχ : χ.IsFiniteOrder) : Modulus K

The conductor of a finite-order Hecke character: the least modulus 𝔣 such that the character is the pullback of a ray class character of 𝔣. It is least for divisibility: the character comes from a ray class character of 𝔪 exactly when its conductor divides 𝔪 (HeckeCharacter.conductor_dvd_iff).

theorem TauCeti.GlobalNumberFields.HeckeCharacter.mem_range_ofRayClassCharacter_conductor {K : Type u_1} [Field K] [NumberField K] {χ : HeckeCharacter K} (hχ : χ.IsFiniteOrder) : χ ∈ (ofRayClassCharacter (χ.conductor hχ)).range

A finite-order Hecke character comes from a ray class character of its conductor.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.conductor_dvd_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {χ : HeckeCharacter K} (hχ : χ.IsFiniteOrder) : χ.conductor hχ ∣ 𝔪 ↔ χ ∈ (ofRayClassCharacter 𝔪).range

The conductor is the least modulus from which a finite-order Hecke character comes: the character is the pullback of a ray class character of 𝔪 exactly when its conductor divides 𝔪.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.conductor_eq_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {χ : HeckeCharacter K} (hχ : χ.IsFiniteOrder) : χ.conductor hχ = 𝔪 ↔ χ ∈ (ofRayClassCharacter 𝔪).range ∧ ∀ (𝔫 : Modulus K), χ ∈ (ofRayClassCharacter 𝔫).range → 𝔪 ∣ 𝔫

The conductor of a finite-order Hecke character is characterized by the moduli from which the character comes.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.conductor_one {K : Type u_1} [Field K] [NumberField K] (h : IsFiniteOrder 1) : conductor 1 h = Modulus.one K

The trivial Hecke character has the trivial conductor.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.conductor_inv {K : Type u_1} [Field K] [NumberField K] {χ : HeckeCharacter K} (hχ : χ⁻¹.IsFiniteOrder) : χ⁻¹.conductor hχ = χ.conductor ⋯

Inverting a finite-order Hecke character does not change its conductor.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.conductor_zpow_dvd {K : Type u_1} [Field K] [NumberField K] {χ : HeckeCharacter K} (hχ : χ.IsFiniteOrder) (n : ℤ) : (χ ^ n).conductor ⋯ ∣ χ.conductor hχ

The conductor of an integer power of a finite-order Hecke character divides its conductor.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.conductor_pow_dvd {K : Type u_1} [Field K] [NumberField K] {χ : HeckeCharacter K} (hχ : χ.IsFiniteOrder) (n : ℕ) : (χ ^ n).conductor ⋯ ∣ χ.conductor hχ

The conductor of a power of a finite-order Hecke character divides its conductor.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.conductor_mul_dvd_lcm_conductor {K : Type u_1} [Field K] [NumberField K] {χ ψ : HeckeCharacter K} (hχ : χ.IsFiniteOrder) (hψ : ψ.IsFiniteOrder) : (χ * ψ).conductor ⋯ ∣ (χ.conductor hχ).lcm (ψ.conductor hψ)

The conductor of a product of finite-order Hecke characters divides the least common multiple of their conductors.