The shift and the unitary part of a Hecke character

For a Hecke character χ of a number field K, the absolute value |χ| is a continuous homomorphism from the idele class group C_K to ℝ>0. It is trivial on the compact norm-one subgroup C_K¹, so it factors through the idele class norm ‖·‖ : C_K → ℝ>0, and a continuous endomorphism of ℝ>0 is a real power. Hence there is a unique real number σ, the shift of χ, with |χ(c)| = ‖c‖ ^ σ for every idele class c. The shift is real by construction: a complex exponent s would only be determined up to the imaginary part, since ‖·‖ ^ (i t) is unitary for every real t.

Twisting χ by ‖·‖ ^ (-σ) gives the unitary part of χ, a Hecke character with values of absolute value 1, and χ is its unitary part times ‖·‖ ^ σ. Characters of finite order, in particular those coming from ray class characters, have shift 0.

Main definitions

• TauCeti.GlobalNumberFields.HeckeCharacter.normPow: the Hecke character c ↦ ‖c‖ ^ s for a complex exponent s.
• TauCeti.GlobalNumberFields.HeckeCharacter.shift: the real exponent σ with |χ| = ‖·‖ ^ σ.
• TauCeti.GlobalNumberFields.HeckeCharacter.unitaryPart: the unitary Hecke character χ · ‖·‖ ^ (-σ).

Main results

• TauCeti.GlobalNumberFields.HeckeCharacter.norm_apply_eq_rpow_shift: |χ(c)| = ‖c‖ ^ σ.
• TauCeti.GlobalNumberFields.HeckeCharacter.shift_eq_of_norm_apply_eq_rpow: the shift is the only real exponent with this property.
• TauCeti.GlobalNumberFields.HeckeCharacter.shift_eq_zero_iff: the shift vanishes exactly for unitary characters.
• TauCeti.GlobalNumberFields.HeckeCharacter.norm_unitaryPart: the unitary part takes values of absolute value 1.
• TauCeti.GlobalNumberFields.HeckeCharacter.unitaryPart_mul_normPow_shift: a Hecke character is its unitary part times ‖·‖ ^ σ, and unitaryPart_mul_normPow shows this decomposition is unique.
• TauCeti.GlobalNumberFields.HeckeCharacter.shift_ofRayClassCharacter: characters coming from ray class characters have shift 0.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII, §6.
• J. Tate, Fourier analysis in number fields and Hecke's zeta-functions, in J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, §3.

The norm characters ‖·‖ ^ s

noncomputable def TauCeti.GlobalNumberFields.HeckeCharacter.normPow (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : HeckeCharacter K

The norm character c ↦ ‖c‖ ^ s of the idele class group, for a complex exponent s. It is unitary exactly when s is purely imaginary.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.normPow_apply {K : Type u_1} [Field K] [NumberField K] (s : ℂ) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : ↑((normPow K s) c) = ↑↑↑(ideleClassNorm c) ^ s

The value of the norm character ‖·‖ ^ s at an idele class c is ‖c‖ ^ s.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.norm_normPow_apply {K : Type u_1} [Field K] [NumberField K] (s : ℂ) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : ‖↑((normPow K s) c)‖ = ↑↑(ideleClassNorm c) ^ s.re

The absolute value of ‖c‖ ^ s is ‖c‖ ^ Re s.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.normPow_zero {K : Type u_1} [Field K] [NumberField K] : normPow K 0 = 1

The zeroth power of the idele class norm is the trivial character.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.normPow_add {K : Type u_1} [Field K] [NumberField K] (s t : ℂ) : normPow K (s + t) = normPow K s * normPow K t

Norm characters multiply by adding exponents.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.normPow_neg {K : Type u_1} [Field K] [NumberField K] (s : ℂ) : normPow K (-s) = (normPow K s)⁻¹

The norm character with the negated exponent is the inverse character.

The shift

noncomputable def TauCeti.GlobalNumberFields.HeckeCharacter.shift {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) : ℝ

The shift of a Hecke character: the unique real number σ with |χ(c)| = ‖c‖ ^ σ for every idele class c.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.norm_apply_eq_rpow_shift {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : ‖↑(χ c)‖ = ↑↑(ideleClassNorm c) ^ χ.shift

The absolute value of a Hecke character is the shift-th power of the idele class norm.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.shift_eq_of_norm_apply_eq_rpow {K : Type u_1} [Field K] [NumberField K] {χ : HeckeCharacter K} {σ : ℝ} (h : ∀ (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K), ‖↑(χ c)‖ = ↑↑(ideleClassNorm c) ^ σ) : χ.shift = σ

Uniqueness of the shift: if |χ| = ‖·‖ ^ σ for a real number σ, then σ is the shift of χ.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.shift_normPow {K : Type u_1} [Field K] [NumberField K] (s : ℂ) : (normPow K s).shift = s.re

The shift of the norm character ‖·‖ ^ s is the real part of s.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.shift_one {K : Type u_1} [Field K] [NumberField K] : shift 1 = 0

The trivial character has shift 0.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.shift_mul {K : Type u_1} [Field K] [NumberField K] (χ ψ : HeckeCharacter K) : (χ * ψ).shift = χ.shift + ψ.shift

Shifts add under multiplication of Hecke characters.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.shift_inv {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) : χ⁻¹.shift = -χ.shift

The inverse of a Hecke character has the negated shift.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.shift_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) : χ.shift = 0 ↔ ∀ (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K), ‖↑(χ c)‖ = 1

The shift vanishes exactly for unitary Hecke characters.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.shift_eq_zero_of_isOfFinOrder {K : Type u_1} [Field K] [NumberField K] {χ : HeckeCharacter K} (hχ : IsOfFinOrder χ) : χ.shift = 0

A Hecke character of finite order has shift 0: its values are roots of unity.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.shift_ofRayClassCharacter {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (η : RayClassCharacter 𝔪) : ((ofRayClassCharacter 𝔪) η).shift = 0

Hecke characters coming from ray class characters have shift 0.

The unitary part

noncomputable def TauCeti.GlobalNumberFields.HeckeCharacter.unitaryPart {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) : HeckeCharacter K

The unitary part of a Hecke character χ: the twist χ · ‖·‖ ^ (-σ) by the inverse power of the idele class norm, where σ is the shift of χ. It takes values of absolute value 1.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.unitaryPart_def {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) : χ.unitaryPart = χ * normPow K (-↑χ.shift)

The unitary part of χ is χ times the norm character with exponent -σ.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.unitaryPart_apply {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : ↑(χ.unitaryPart c) = ↑(χ c) * ↑↑↑(ideleClassNorm c) ^ (-↑χ.shift)

The value of the unitary part of χ at c is χ(c) · ‖c‖ ^ (-σ).

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.shift_unitaryPart {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) : χ.unitaryPart.shift = 0

The unitary part of a Hecke character has shift 0.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.norm_unitaryPart {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : ‖↑(χ.unitaryPart c)‖ = 1

The unitary part of a Hecke character takes values of absolute value 1.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.unitaryPart_mul_normPow_shift {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) : χ.unitaryPart * normPow K ↑χ.shift = χ

The unitary decomposition: a Hecke character is its unitary part times the shift-th power of the idele class norm.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.unitaryPart_mul {K : Type u_1} [Field K] [NumberField K] (χ ψ : HeckeCharacter K) : (χ * ψ).unitaryPart = χ.unitaryPart * ψ.unitaryPart

The unitary part of a product is the product of the unitary parts.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.unitaryPart_one {K : Type u_1} [Field K] [NumberField K] : unitaryPart 1 = 1

The unitary part of the trivial character is trivial.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.unitaryPart_inv {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) : χ⁻¹.unitaryPart = χ.unitaryPart⁻¹

The unitary part of an inverse is the inverse of the unitary part.

@[simp]

theorem TauCeti.GlobalNumberFields.HeckeCharacter.unitaryPart_unitaryPart {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) : χ.unitaryPart.unitaryPart = χ.unitaryPart

Taking the unitary part twice has the same result as taking it once.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.unitaryPart_mul_normPow {K : Type u_1} [Field K] [NumberField K] {ψ : HeckeCharacter K} (hψ : ψ.shift = 0) (σ : ℝ) : (ψ * normPow K ↑σ).unitaryPart = ψ

Uniqueness of the unitary decomposition: the unitary part of ψ · ‖·‖ ^ σ, for a unitary Hecke character ψ and a real number σ, is ψ.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.unitaryPart_eq_self_iff {K : Type u_1} [Field K] [NumberField K] (χ : HeckeCharacter K) : χ.unitaryPart = χ ↔ χ.shift = 0

A Hecke character is its own unitary part exactly when its shift vanishes.