Real signs and the infinite part of the conductor

A finite-order Hecke character χ of a number field K has vanishing modulus exponents, so its component at a real place w is x ↦ sgn(x) ^ ε_w for the real parity ε_w : ZMod 2 of its infinity type (HeckeCharacter.infinityType_eq_toContinuous_realParity). This file identifies these parities with the infinite part of the conductor of χ: the real place w divides the conductor exactly when ε_w = 1, that is, exactly when χ is nontrivial on K_wˣ.

The comparison rests on two facts about an arbitrary modulus, proved in TauCeti.NumberTheory.NumberField.Global.HeckeCharacter.InfinityType. If χ comes from a ray class character of 𝔪, it is trivial at every infinite place outside 𝔪 (HeckeCharacter.infiniteComponent_eq_one_of_mem_range_ofRayClassCharacter). Conversely, if χ comes from 𝔪 and is trivial at a real place w of 𝔪, it still comes from the modulus obtained by removing w from 𝔪 (HeckeCharacter.mem_range_ofRayClassCharacter_erase). The conductor is the least modulus from which χ comes, so it omits every real place at which χ is trivial.

Consequently the infinity type of a finite-order Hecke character is zero exactly when its conductor has no real places, and only then is it the continuous infinity type of an AlgebraicInfinityType. Every finite-order Hecke character is nevertheless algebraic (HeckeCharacter.isAlgebraic_of_isFiniteOrder): Weil's type A₀ compares infinity types only on the identity component, which does not see the real signs.

Main results

• HeckeCharacter.mem_conductor_infinitePart_iff: a real place divides the conductor of a finite-order Hecke character exactly when its real parity there is one.
• HeckeCharacter.infinityType_eq_zero_iff: the infinity type of a finite-order Hecke character vanishes exactly when its conductor has no real places.
• HeckeCharacter.infinityType_mem_range_toContinuous_iff: the same condition characterizes the finite-order characters whose infinity type comes from an AlgebraicInfinityType.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §1 and Chapter VII, §6.
• A. Weil, Basic Number Theory, Chapter VII, §3.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.realParity_infinityType_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] {χ : HeckeCharacter K} (hχ : χ.IsFiniteOrder) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : χ.infinityType.realParity w = 0 ↔ w ∉ (χ.conductor hχ).infinitePart

The real places outside the conductor. The real parity of a finite-order Hecke character at a real place w is zero exactly when w does not divide its conductor.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.mem_conductor_infinitePart_iff {K : Type u_1} [Field K] [NumberField K] {χ : HeckeCharacter K} (hχ : χ.IsFiniteOrder) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : w ∈ (χ.conductor hχ).infinitePart ↔ χ.infinityType.realParity w = 1

The infinite part of the conductor is the set of real signs. A real place w divides the conductor of a finite-order Hecke character exactly when its real parity at w is one, that is, when the character is nontrivial on the negative elements of K_w.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.infinityType_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] {χ : HeckeCharacter K} (hχ : χ.IsFiniteOrder) : χ.infinityType = 0 ↔ (χ.conductor hχ).infinitePart = ∅

The infinity type of a finite-order Hecke character vanishes exactly when its conductor has no real places.

theorem TauCeti.GlobalNumberFields.HeckeCharacter.infinityType_mem_range_toContinuous_iff {K : Type u_1} [Field K] [NumberField K] {χ : HeckeCharacter K} (hχ : χ.IsFiniteOrder) : χ.infinityType ∈ Set.range ⇑AlgebraicInfinityType.toContinuous ↔ (χ.conductor hχ).infinitePart = ∅

Finite-order Hecke characters with the infinity type of an algebraic infinity type. The infinity type of a finite-order Hecke character is AlgebraicInfinityType.toContinuous n for some n exactly when its conductor has no real places. In particular a finite-order character whose conductor contains a real place, although algebraic, does not have the infinity type of any AlgebraicInfinityType.