Documentation

TauCeti.NumberTheory.NumberField.Global.HeckeCharacter.Basic

Hecke characters #

A Hecke character of a number field K is a continuous homomorphism from the idele class group C_K = 𝔸_K^Γ— / K^Γ— to β„‚Λ£. Hecke characters are the characters whose L-functions generalize Dirichlet L-functions to number fields.

Every ray class character of a modulus π”ͺ defines a Hecke character by pullback along the surjection rayClassQuotient π”ͺ : C_K β†’ Cl_π”ͺ; the pullback is continuous because the kernel of rayClassQuotient π”ͺ is the open ray subgroup. The pullback is injective, and its image consists exactly of the Hecke characters that are trivial on raySubgroup π”ͺ. Pullbacks along different moduli are compatible with the change-of-modulus map RayClassCharacter.induced, and every Hecke character coming from a ray class character has finite order.

Main definitions #

Main results #

References #

source
@[reducible, inline]
abbrev TauCeti.GlobalNumberFields.HeckeCharacter (K : Type u_1) [Field K] [NumberField K] :
Type u_1

A Hecke character of K: a continuous homomorphism from the idele class group of K to the complex units. Hecke characters form a commutative group under pointwise multiplication.

Instances For
    source
    @[reducible, inline]
    abbrev TauCeti.GlobalNumberFields.HeckeCharacter.IsFiniteOrder {K : Type u_1} [Field K] [NumberField K] (Ο‡ : HeckeCharacter K) :
    Prop

    A Hecke character has finite order when it has finite order as an element of the commutative group of continuous idele-class characters.

    Instances For
      source
      theorem TauCeti.GlobalNumberFields.HeckeCharacter.isFiniteOrder_iff {K : Type u_1} [Field K] [NumberField K] (Ο‡ : HeckeCharacter K) :
      Ο‡.IsFiniteOrder ↔ βˆƒ (n : β„•), 0 < n ∧ βˆ€ (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K), Ο‡ c ^ n = 1

      A Hecke character has finite order exactly when all of its values have a common positive exponent equal to one.

      source
      noncomputable def TauCeti.GlobalNumberFields.HeckeCharacter.ofRayClassCharacter {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
      RayClassCharacter π”ͺ β†’* HeckeCharacter K

      The Hecke character of a ray class character: the pullback of a character of the ray class group of π”ͺ along rayClassQuotient π”ͺ. It is continuous because it is trivial on the open subgroup raySubgroup π”ͺ.

      Instances For
        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.HeckeCharacter.ofRayClassCharacter_apply {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} (Ο‡ : RayClassCharacter π”ͺ) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) :
        ((ofRayClassCharacter π”ͺ) Ο‡) c = Ο‡ ((rayClassQuotient π”ͺ) c)

        The Hecke character of a ray class character is its value at the ray class.

        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.HeckeCharacter.toMonoidHom_ofRayClassCharacter {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} (Ο‡ : RayClassCharacter π”ͺ) :
        ↑((ofRayClassCharacter π”ͺ) Ο‡) = MonoidHom.comp Ο‡ (rayClassQuotient π”ͺ)

        The underlying homomorphism of the Hecke character of a ray class character is the composite with rayClassQuotient π”ͺ.

        source
        theorem TauCeti.GlobalNumberFields.HeckeCharacter.ofRayClassCharacter_injective {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
        Function.Injective ⇑(ofRayClassCharacter π”ͺ)

        Pullback of ray class characters is injective, because rayClassQuotient π”ͺ is surjective.

        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.HeckeCharacter.ofRayClassCharacter_eq_one_iff {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {Ο‡ : RayClassCharacter π”ͺ} :
        (ofRayClassCharacter π”ͺ) Ο‡ = 1 ↔ Ο‡ = 1

        The Hecke character of a ray class character is trivial exactly when the ray class character is trivial.

        source
        theorem TauCeti.GlobalNumberFields.HeckeCharacter.ofRayClassCharacter_apply_eq_one_of_mem_raySubgroup {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} (Ο‡ : RayClassCharacter π”ͺ) {c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K} (hc : c ∈ raySubgroup π”ͺ) :
        ((ofRayClassCharacter π”ͺ) Ο‡) c = 1

        The Hecke character of a ray class character of π”ͺ is trivial on the ray subgroup of π”ͺ.

        source
        theorem TauCeti.GlobalNumberFields.HeckeCharacter.mem_range_ofRayClassCharacter_iff {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {Ο‡ : HeckeCharacter K} :
        Ο‡ ∈ (ofRayClassCharacter π”ͺ).range ↔ raySubgroup π”ͺ ≀ (↑χ).ker

        The image of pullback from the ray class group of π”ͺ. A Hecke character comes from a ray class character of π”ͺ exactly when it is trivial on raySubgroup π”ͺ.

        source
        theorem TauCeti.GlobalNumberFields.HeckeCharacter.mem_range_ofRayClassCharacter_gcd {K : Type u_1} [Field K] [NumberField K] {π”ͺ 𝔫 : Modulus K} {Ο‡ : HeckeCharacter K} (hπ”ͺ : Ο‡ ∈ (ofRayClassCharacter π”ͺ).range) (h𝔫 : Ο‡ ∈ (ofRayClassCharacter 𝔫).range) :
        Ο‡ ∈ (ofRayClassCharacter (π”ͺ.gcd 𝔫)).range

        The moduli from which a Hecke character comes are closed under greatest common divisors. A Hecke character trivial on the ray subgroups of π”ͺ and of 𝔫 is trivial on the subgroup they generate, which is the ray subgroup of π”ͺ.gcd 𝔫.

        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.HeckeCharacter.ofRayClassCharacter_induced {K : Type u_1} [Field K] [NumberField K] {π”ͺ 𝔫 : Modulus K} (h : π”ͺ ∣ 𝔫) (Ο‡ : RayClassCharacter π”ͺ) :
        (ofRayClassCharacter 𝔫) ((RayClassCharacter.induced h) Ο‡) = (ofRayClassCharacter π”ͺ) Ο‡

        Pullback is compatible with change of modulus: for π”ͺ ∣ 𝔫, inducing a ray class character of π”ͺ to 𝔫 and then pulling back gives the same Hecke character as pulling back directly from π”ͺ.

        source
        theorem TauCeti.GlobalNumberFields.HeckeCharacter.range_ofRayClassCharacter_le {K : Type u_1} [Field K] [NumberField K] {π”ͺ 𝔫 : Modulus K} (h : π”ͺ ∣ 𝔫) :
        (ofRayClassCharacter π”ͺ).range ≀ (ofRayClassCharacter 𝔫).range

        The Hecke characters coming from ray class characters of π”ͺ also come from ray class characters of every multiple of π”ͺ.

        source
        theorem TauCeti.GlobalNumberFields.HeckeCharacter.isFiniteOrder_ofRayClassCharacter {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} (Ο‡ : RayClassCharacter π”ͺ) :
        ((ofRayClassCharacter π”ͺ) Ο‡).IsFiniteOrder

        Hecke characters coming from ray class characters have finite order, since the ray class group is finite.

        source
        theorem TauCeti.GlobalNumberFields.RayClassCharacter.exists_induced_eq_iff_mem_range {K : Type u_1} [Field K] [NumberField K] {π”ͺ 𝔫 : Modulus K} (h : 𝔫 ∣ π”ͺ) (Ξ· : RayClassCharacter π”ͺ) :
        (βˆƒ (ψ : RayClassCharacter 𝔫), (induced h) ψ = Ξ·) ↔ (HeckeCharacter.ofRayClassCharacter π”ͺ) Ξ· ∈ (HeckeCharacter.ofRayClassCharacter 𝔫).range

        A ray class character of π”ͺ is induced from a divisor 𝔫 of π”ͺ exactly when its Hecke character comes from a ray class character of 𝔫.