Documentation

TauCeti.NumberTheory.NumberField.Global.RayClass.Character.Weight

Ideal weights of ray class characters #

A ray class character is defined on the ray class group of its modulus. Extending its induced evaluation ฯ‡.onIdeals on prime-to integral ideals by zero on the remaining ideals gives a completely multiplicative ideal weight. Its bad primes are exactly the prime divisors of the finite part of the modulus. Finiteness of the ray class group also makes the weight unitary, so its norm coefficients can be used in the Dirichlet series of arithmetic characters.

The trivial character extends to the indicator of ideals prime to the modulus, which is generally different from the everywhere-good unitary weight. Pointwise products still commute with the extension.

The zero extension here is the usual convention for the Dirichlet series of a ray class character. See Neukirch, Algebraic Number Theory, Chapter VII, ยง6.

Extend the induced evaluation ฯ‡.onIdeals on prime-to integral ideals by zero on all other ideals.

Instances For
    @[simp]

    On an ideal prime to the modulus, the extended weight equals the character value.

    @[simp]

    The extended character vanishes on ideals meeting the finite part of its modulus.

    @[simp]

    The bad primes of the ideal weight are precisely the finite primes of the modulus.

    @[simp]

    The trivial ray class character gives the indicator weight away from the modulus.

    @[simp]

    Pointwise multiplication of ray class characters agrees with multiplication of ideal weights, including at ideals meeting the modulus.

    Distinct ray class characters have distinct ideal weights: evaluation on the prime-to integral ideals already determines a ray class character.

    A ray class character gives a unitary ideal weight, extended by zero at bad primes.

    Instances For
      @[simp]

      The underlying multiplicative weight of the unitary extension.

      @[simp]

      The unitary extension respects pointwise multiplication of characters.

      theorem TauCeti.GlobalNumberFields.RayClassCharacter.toUnitaryIdealWeight_induced {K : Type u_1} [Field K] [NumberField K] {๐”ช ๐”ซ : Modulus K} (h : ๐”ช โˆฃ ๐”ซ) (ฯ‡ : RayClassCharacter ๐”ช) :
      ((induced h) ฯ‡).toUnitaryIdealWeight = ฯ‡.toUnitaryIdealWeight.restrictAway โ†‘๐”ซ.support โ‹ฏ

      Increasing the modulus restricts the induced character's ideal weight away from the finite primes of the larger modulus.

      The unitary extensions distinguish ray class characters.