Ray class characters

A ray class character of a modulus 𝔪 is a multiplicative character of its finite ray class group with values in the complex units. Composing with idealClass 𝔪 evaluates it on the nonzero integral ideals prime to the finite part of 𝔪; the coprimality proof remains in the domain because idealClass 𝔪 is defined only on those ideals.

When 𝔪 ∣ 𝔫, pullback along the surjective transition classMap : Cl_𝔫 → Cl_𝔪 induces a character of the larger modulus. These pullbacks are injective, compose along chains of moduli, and agree with the inclusion of integral ideals prime to the larger modulus. This is the finite character API used in ray-class counting and in the factorization of cyclotomic Galois characters.

Main definitions

• TauCeti.GlobalNumberFields.RayClassCharacter: multiplicative complex-unit characters of a ray class group;
• TauCeti.GlobalNumberFields.RayClassCharacter.onIdeals: evaluation on integral ideals prime to the modulus;
• TauCeti.GlobalNumberFields.RayClassCharacter.induced: pullback of a character along a change of modulus.

Main results

• TauCeti.GlobalNumberFields.RayClassCharacter.ext: a ray class character is determined by its values on integral ideals;
• TauCeti.GlobalNumberFields.RayClassCharacter.induced_injective: increasing the modulus does not identify distinct characters;
• TauCeti.GlobalNumberFields.RayClassCharacter.onIdeals_induced: change of modulus commutes with evaluation on ideals;
• TauCeti.GlobalNumberFields.RayClassCharacter.exists_induced_eq_iff_of_finitePart_eq: a character is induced from a modulus with the same finite part exactly when it is trivial on the sign classes of the forgotten real places.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §1.
• S. Lang, Algebraic Number Theory, Chapter VII, §1.

@[reducible, inline]

abbrev TauCeti.GlobalNumberFields.RayClassCharacter {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Type u_1

A ray class character of 𝔪: a multiplicative character of RayClassGroup 𝔪 with values in the complex units.

noncomputable def TauCeti.GlobalNumberFields.RayClassCharacter.onIdeals {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassCharacter 𝔪) : ↥(integralIdealsPrimeTo 𝔪) →* ℂˣ

Evaluate a ray class character on nonzero integral ideals prime to its modulus.

The domain is integralIdealsPrimeTo 𝔪, rather than all integral ideals, because an ideal meeting the finite part of the modulus has no ray class and hence no character value.

@[simp]

theorem TauCeti.GlobalNumberFields.RayClassCharacter.onIdeals_apply {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassCharacter 𝔪) (I : ↥(integralIdealsPrimeTo 𝔪)) : χ.onIdeals I = χ ((idealClass 𝔪) I)

Evaluating a ray class character on an ideal is evaluation at the ideal's ray class.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.ext {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {χ ψ : RayClassCharacter 𝔪} (h : ∀ (I : ↥(integralIdealsPrimeTo 𝔪)), χ.onIdeals I = ψ.onIdeals I) : χ = ψ

A ray class character is determined by its values on integral ideals prime to the modulus.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.ext_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {χ ψ : RayClassCharacter 𝔪} : χ = ψ ↔ ∀ (I : ↥(integralIdealsPrimeTo 𝔪)), χ.onIdeals I = ψ.onIdeals I

noncomputable def TauCeti.GlobalNumberFields.RayClassCharacter.induced {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) : RayClassCharacter 𝔪 →* RayClassCharacter 𝔫

Pullback of ray class characters from a modulus 𝔪 to a multiple 𝔫 of that modulus.

@[simp]

theorem TauCeti.GlobalNumberFields.RayClassCharacter.induced_apply {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) (χ : RayClassCharacter 𝔪) (c : RayClassGroup 𝔫) : ((induced h) χ) c = χ ((classMap h) c)

A character induced to a larger modulus is evaluated through the transition map.

@[simp]

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

Pullback along the identity change of modulus fixes every character.

@[simp]

theorem TauCeti.GlobalNumberFields.RayClassCharacter.induced_trans {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 𝔬 : Modulus K} (h₁ : 𝔪 ∣ 𝔫) (h₂ : 𝔫 ∣ 𝔬) (χ : RayClassCharacter 𝔪) : (induced h₂) ((induced h₁) χ) = (induced ⋯) χ

Pullback of ray class characters composes along a chain of moduli.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.induced_injective {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) : Function.Injective ⇑(induced h)

Increasing the modulus does not identify distinct ray class characters.

@[simp]

theorem TauCeti.GlobalNumberFields.RayClassCharacter.induced_eq_one_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) (χ : RayClassCharacter 𝔪) : (induced h) χ = 1 ↔ χ = 1

A character induced to a larger modulus is trivial exactly when the original character is trivial.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.onIdeals_induced {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) (χ : RayClassCharacter 𝔪) (I : ↥(integralIdealsPrimeTo 𝔫)) : ((induced h) χ).onIdeals I = χ.onIdeals ((integralIdealsPrimeToInclusion h) I)

Change of modulus commutes with evaluation on integral ideals: the induced character at an ideal prime to 𝔫 is the original character at the same ideal viewed as prime to 𝔪.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.exists_induced_eq_iff_of_finitePart_eq {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) (hfin : 𝔪.finitePart = 𝔫.finitePart) (η : RayClassCharacter 𝔫) : (∃ (ψ : RayClassCharacter 𝔪), (induced h) ψ = η) ↔ ∀ (s : ↥𝔫.infinitePart → ℤˣ), (∀ (w : ↥𝔫.infinitePart), ↑w ∈ 𝔪.infinitePart → s w = 1) → η ((residueSignRayClass 𝔫) (1, s)) = 1

Inducing from a modulus with the same finite part is a condition on sign classes. When 𝔪 ∣ 𝔫 have the same finite part, a ray class character of 𝔫 is induced from 𝔪 exactly when it is trivial on the classes residueSignRayClass 𝔫 (1, s) of every pattern of signs s trivial at the real places of 𝔪.