Cancellation for the ideal weight of a cyclotomic Galois character

Let F = K(μ_m) be an m-th cyclotomic extension of a number field K and χ a character of Gal(F/K) whose ray class character χ ∘ cyclotomicArtin K F m of cyclotomicModulus K m is nontrivial. This file provides cancellation for the ideal weight galoisCharacterUnitaryWeight χ with its Euler factors at the primes dividing m deleted: its ideal partial sums are O(x ^ (1 - 1 / [K : ℚ])). At such a prime the weight can be a root of unity rather than 0 (the prime may be unramified in F), so the restricted weight is the one that agrees with the ray class character.

Main results

• MonoidHom.hasCancellation_restrictAway_galoisCharacterUnitaryWeight: the weight restricted away from the primes dividing m has cancellation.

theorem MonoidHom.hasCancellation_restrictAway_galoisCharacterUnitaryWeight {K : Type u_1} [Field K] [NumberField K] {F : Type u_2} [Field F] [NumberField F] [Algebra K F] {m : ℕ} [NeZero m] [IsCyclotomicExtension {m} K F] [IsGalois K F] (χ : Gal(F/K) →* ℂˣ) (hχ : χ.comp (NumberField.Chebotarev.cyclotomicArtin K F m) ≠ 1) : TauCeti.HasCancellation (χ.galoisCharacterUnitaryWeight.restrictAway ↑(NumberField.Chebotarev.cyclotomicModulus K m).support ⋯)

Cancellation for a cyclotomic Galois character, away from the level. For F = K(μ_m) and a character χ of Gal(F/K) whose ray class character χ ∘ cyclotomicArtin K F m is nontrivial, the ideal weight of χ with the Euler factors at the primes dividing m deleted has cancellation.