Finite-order Hecke characters

A finite-order Hecke character is locally constant: its kernel is an open subgroup of the idele class group. Every open subgroup of the idele class group contains a ray subgroup (exists_raySubgroup_le_of_isOpen), and a Hecke character trivial on raySubgroup 𝔪 is the pullback of a ray class character of 𝔪 (HeckeCharacter.mem_range_ofRayClassCharacter_iff). Together with the finiteness of the ray class groups this proves that, for a Hecke character, the following are equivalent: it has finite order, its kernel is open, and it is the pullback of a ray class character of some modulus. The finite-order Hecke characters are therefore exactly the characters of the ray class groups, which is why the ray class L-functions exhaust the Hecke L-functions of finite-order characters.

Main results

• HeckeCharacter.isOpen_ker_of_isFiniteOrder: a finite-order Hecke character has open kernel.
• HeckeCharacter.exists_ofRayClassCharacter_eq_of_isOpen_ker: a Hecke character with open kernel is the pullback of a ray class character.
• HeckeCharacter.isFiniteOrder_iff_exists_rayClassCharacter: a Hecke character has finite order exactly when it is the pullback of a ray class character of some modulus.
• HeckeCharacter.isFiniteOrder_iff_isOpen_ker: a Hecke character has finite order exactly when its kernel is open.
• HeckeCharacter.rayClassCharacterAt: the unique ray class character representing a Hecke character at a specified modulus.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §1 and Chapter VII, §6.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.isOpen_ker_of_isFiniteOrder {K : Type u_1} [Field K] [NumberField K] {χ : HeckeCharacter K} (hχ : χ.IsFiniteOrder) : IsOpen ↑(↑χ).ker

A finite-order Hecke character has open kernel, and is therefore locally constant.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.isOpen_ker_ofRayClassCharacter {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (η : RayClassCharacter 𝔪) : IsOpen ↑(↑((ofRayClassCharacter 𝔪) η)).ker

A Hecke character pulled back from a ray class character has open kernel.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.exists_ofRayClassCharacter_eq_of_isOpen_ker {K : Type u_1} [Field K] [NumberField K] {χ : HeckeCharacter K} (hχ : IsOpen ↑(↑χ).ker) : ∃ (𝔪 : Modulus K) (η : RayClassCharacter 𝔪), (ofRayClassCharacter 𝔪) η = χ

A Hecke character with open kernel is the pullback of a ray class character of some modulus 𝔪. Together with isOpen_ker_ofRayClassCharacter this identifies the Hecke characters with open kernel with the ray class characters of all moduli.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.isFiniteOrder_iff_exists_rayClassCharacter {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) : χ.IsFiniteOrder ↔ ∃ (𝔪 : Modulus K) (η : RayClassCharacter 𝔪), (ofRayClassCharacter 𝔪) η = χ

Finite-order Hecke characters are exactly the ray class characters: a Hecke character has finite order exactly when it is the pullback of a ray class character of some modulus.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.isFiniteOrder_iff_isOpen_ker {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) : χ.IsFiniteOrder ↔ IsOpen ↑(↑χ).ker

A Hecke character has finite order exactly when its kernel is open.

noncomputable def TauCeti.GlobalNumberFields.HeckeCharacter.rayClassCharacterAt {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) (𝔪 : Modulus K) (hχ : χ ∈ (ofRayClassCharacter 𝔪).range) : RayClassCharacter 𝔪

The unique ray class character of 𝔪 whose pullback is χ, given that χ comes from RayClassGroup 𝔪.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.ofRayClassCharacter_rayClassCharacterAt {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) (𝔪 : Modulus K) (hχ : χ ∈ (ofRayClassCharacter 𝔪).range) : (ofRayClassCharacter 𝔪) (χ.rayClassCharacterAt 𝔪 hχ) = χ

Pulling the representing ray class character back to the idele class group recovers the original Hecke character.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.rayClassCharacterAt_eq_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {χ : HeckeCharacter K} (hχ : χ ∈ (ofRayClassCharacter 𝔪).range) {η : RayClassCharacter 𝔪} : χ.rayClassCharacterAt 𝔪 hχ = η ↔ (ofRayClassCharacter 𝔪) η = χ

The representing ray class character is characterized by its pullback to the idele class group.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.rayClassCharacterAt_ofRayClassCharacter {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (η : RayClassCharacter 𝔪) : ((ofRayClassCharacter 𝔪) η).rayClassCharacterAt 𝔪 ⋯ = η

Extracting the representative of a Hecke character already presented by a ray class character returns that character.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.rayClassCharacterAt_of_dvd {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) (χ : HeckeCharacter K) (hχ : χ ∈ (ofRayClassCharacter 𝔪).range) : χ.rayClassCharacterAt 𝔫 ⋯ = (RayClassCharacter.induced h) (χ.rayClassCharacterAt 𝔪 hχ)

On increasing the modulus, the representative of a Hecke character is obtained by inducing its representative at the smaller modulus.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.rayClassCharacterAt_mul {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {χ ψ : HeckeCharacter K} (hχ : χ ∈ (ofRayClassCharacter 𝔪).range) (hψ : ψ ∈ (ofRayClassCharacter 𝔪).range) : (χ * ψ).rayClassCharacterAt 𝔪 ⋯ = χ.rayClassCharacterAt 𝔪 hχ * ψ.rayClassCharacterAt 𝔪 hψ

At a fixed modulus, the representative of a product is the product of the representatives.