The conductor of a ray class character

For a ray class character η of 𝔪, the conductor of its Hecke character (HeckeCharacter.conductor) is the least modulus from which η is induced. It divides 𝔪, it does not change when η is induced to a larger modulus, and η is primitive exactly when its conductor is 𝔪. Every ray class character is induced from a primitive character of its conductor, RayClassCharacter.primitiveCharacter, and every finite-order Hecke character is the pullback of a primitive ray class character of its conductor. Primitive characters are the normalization in which ray class L-functions are studied.

Main definitions

• TauCeti.GlobalNumberFields.RayClassCharacter.conductor: the least modulus from which a ray class character is induced.
• TauCeti.GlobalNumberFields.RayClassCharacter.primitiveCharacter: the primitive character of the conductor inducing a ray class character.

Main results

• TauCeti.GlobalNumberFields.RayClassCharacter.conductor_dvd_iff: a ray class character is induced from a divisor 𝔫 of its modulus exactly when its conductor divides 𝔫.
• TauCeti.GlobalNumberFields.RayClassCharacter.conductor_induced: inducing a character to a larger modulus does not change its conductor.
• TauCeti.GlobalNumberFields.RayClassCharacter.conductor_eq_of_induced_eq: two characters that induce the same character of a common multiple of their moduli have the same conductor.
• TauCeti.GlobalNumberFields.RayClassCharacter.isPrimitive_iff_conductor_eq: a ray class character is primitive exactly when its conductor is its modulus.
• TauCeti.GlobalNumberFields.RayClassCharacter.induced_primitiveCharacter and TauCeti.GlobalNumberFields.RayClassCharacter.isPrimitive_primitiveCharacter: every ray class character is induced from a primitive character of its conductor.
• TauCeti.GlobalNumberFields.RayClassCharacter.conductor_inv, TauCeti.GlobalNumberFields.RayClassCharacter.conductor_zpow_dvd, and TauCeti.GlobalNumberFields.RayClassCharacter.conductor_mul_dvd_lcm_conductor: the conductor and the group operations.
• TauCeti.GlobalNumberFields.HeckeCharacter.isPrimitive_rayClassCharacterAt_conductor: a finite-order Hecke character is the pullback of a primitive ray class character of its conductor, namely its representative there.

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, DirichletCharacter.conductor_changeLevel).

noncomputable def TauCeti.GlobalNumberFields.RayClassCharacter.conductor {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (η : RayClassCharacter 𝔪) : Modulus K

The conductor of a ray class character: the conductor of its Hecke character, that is, the least modulus from which the character is induced (RayClassCharacter.conductor_dvd_iff).

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.conductor_ofRayClassCharacter {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (η : RayClassCharacter 𝔪) (hη : ((ofRayClassCharacter 𝔪) η).IsFiniteOrder) : ((ofRayClassCharacter 𝔪) η).conductor hη = η.conductor

The conductor of the Hecke character of a ray class character is the conductor of the ray class character.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.conductor_dvd_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔫 ∣ 𝔪) {η : RayClassCharacter 𝔪} : η.conductor ∣ 𝔫 ↔ ∃ (ψ : RayClassCharacter 𝔫), (induced h) ψ = η

The conductor is the least modulus from which a ray class character is induced: a ray class character of 𝔪 is induced from a divisor 𝔫 of 𝔪 exactly when its conductor divides 𝔫.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.conductor_dvd {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (η : RayClassCharacter 𝔪) : η.conductor ∣ 𝔪

The conductor of a ray class character divides its modulus.

noncomputable def TauCeti.GlobalNumberFields.RayClassCharacter.primitiveCharacter {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (η : RayClassCharacter 𝔪) : RayClassCharacter η.conductor

The primitive character inducing a ray class character: the character of the conductor from which the ray class character is induced (RayClassCharacter.induced_primitiveCharacter). It is primitive (RayClassCharacter.isPrimitive_primitiveCharacter).

@[simp]

theorem TauCeti.GlobalNumberFields.RayClassCharacter.induced_primitiveCharacter {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (η : RayClassCharacter 𝔪) : (induced ⋯) η.primitiveCharacter = η

A ray class character is induced from its primitive character.

@[simp]

theorem TauCeti.GlobalNumberFields.RayClassCharacter.conductor_induced {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) (η : RayClassCharacter 𝔪) : ((induced h) η).conductor = η.conductor

Inducing a ray class character to a larger modulus does not change its conductor.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.conductor_eq_of_induced_eq {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 𝔐 : Modulus K} (h : 𝔪 ∣ 𝔐) (h' : 𝔫 ∣ 𝔐) {η : RayClassCharacter 𝔪} {η' : RayClassCharacter 𝔫} (hη : (induced h) η = (induced h') η') : η.conductor = η'.conductor

Two ray class characters, possibly of different moduli, that induce the same character of a common multiple of their moduli have the same conductor.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.isPrimitive_iff_conductor_eq {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (η : RayClassCharacter 𝔪) : η.IsPrimitive ↔ η.conductor = 𝔪

A ray class character is primitive exactly when its conductor is its modulus.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.isPrimitive_primitiveCharacter {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (η : RayClassCharacter 𝔪) : η.primitiveCharacter.IsPrimitive

The primitive character of a ray class character is primitive.

@[simp]

theorem TauCeti.GlobalNumberFields.RayClassCharacter.conductor_one {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} : conductor 1 = Modulus.one K

The trivial character of any modulus has the trivial conductor.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.conductor_eq_one_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {η : RayClassCharacter 𝔪} : η.conductor = Modulus.one K ↔ ∃ (ψ : RayClassCharacter (Modulus.one K)), (induced ⋯) ψ = η

A ray class character has the trivial conductor exactly when it is induced from a character of the trivial modulus, that is, of the ideal class group.

@[simp]

theorem TauCeti.GlobalNumberFields.RayClassCharacter.primitiveCharacter_one {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} : primitiveCharacter 1 = 1

The primitive character of the trivial character is trivial.

@[simp]

theorem TauCeti.GlobalNumberFields.RayClassCharacter.conductor_inv {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (η : RayClassCharacter 𝔪) : η⁻¹.conductor = η.conductor

Inverting a ray class character does not change its conductor.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.conductor_zpow_dvd {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (η : RayClassCharacter 𝔪) (n : ℤ) : (η ^ n).conductor ∣ η.conductor

The conductor of an integer power of a ray class character divides its conductor.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.conductor_pow_dvd {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (η : RayClassCharacter 𝔪) (n : ℕ) : (η ^ n).conductor ∣ η.conductor

The conductor of a power of a ray class character divides its conductor.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.conductor_mul_dvd_lcm_conductor {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (η ψ : RayClassCharacter 𝔪) : (η * ψ).conductor ∣ η.conductor.lcm ψ.conductor

The conductor of a product of ray class characters divides the least common multiple of their conductors.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.isPrimitive_rayClassCharacterAt_conductor {K : Type u_1} [Field K] [NumberField K] {χ : HeckeCharacter K} (hχ : χ.IsFiniteOrder) : (χ.rayClassCharacterAt (χ.conductor hχ) ⋯).IsPrimitive

The representative of a finite-order Hecke character at its conductor is primitive. Since its pullback is the character itself (ofRayClassCharacter_rayClassCharacterAt), a finite-order Hecke character is the pullback of a primitive ray class character of its conductor.