The ideal weight of a Galois character #
For a finite Galois extension L / K of number fields and a character χ : Gal(L/K) →* ℂˣ, this
file builds the canonical ideal weight galoisCharacterWeight χ: the completely multiplicative
function on the ideals of 𝓞 K whose value at a height-one prime 𝔭 is χ (Frob 𝔭) when 𝔭 is
unramified in L, and 0 when 𝔭 ramifies. Since Gal(L/K) is finite those unramified values
are roots of unity, so the same weight is packaged a second time as a
TauCeti.UnitaryIdealWeight K.
Nothing here assumes that L / K is cyclotomic: the construction needs only [IsGalois K L], and
the character is an arbitrary degree-one complex character of the Galois group. The Dirichlet
weight is the specialisation L / K = ℚ(ζ_m) / ℚ, where the cyclotomic character identifies
Gal(ℚ(ζ_m)/ℚ) with (ZMod m)ˣ and χ is a Dirichlet character mod m. Over a general base K
that character is still injective but need not be surjective: restriction identifies
Gal(K(ζ_m)/K) with the subgroup of (ZMod m)ˣ fixing K ∩ ℚ(ζ_m), and that subgroup is all of
(ZMod m)ˣ exactly when K ∩ ℚ(ζ_m) = ℚ. The declarations are named for the generality they
actually have.
The weight is total, and that is a design constraint rather than a convenience: a weight
specified only away from ramification leaves its values at the bad primes unconstrained, so the
Euler product and the orthogonality identities would not pin it down. Vanishing at the ramified
primes is what makes the ramified Euler factors drop out as (1 - 0)⁻¹ = 1.
Main definitions #
MonoidHom.galoisCharacterWeight: the weight ofχ, packaged as aTauCeti.MultiplicativeIdealWeight K.MonoidHom.galoisCharacterUnitaryWeight: the same weight packaged as aTauCeti.UnitaryIdealWeight K, its values having modulus1away from the ramified primes.
Main results #
MonoidHom.galoisCharacterWeight_apply_of_unramified: at an unramified height-one prime the weight isχof the Artin symbol.MonoidHom.galoisCharacterWeight_apply_eq_zero_iff: the weight vanishes at a height-one prime exactly when that prime ramifies inL.MonoidHom.badPrimes_galoisCharacterWeight: the bad primes of the weight are exactly the ramified primes.MonoidHom.galoisCharacterWeight_one: the weight of the trivial character is the indicator of the ideals prime to the ramified primes, so itsL-series is the Dedekind zeta function with the ramified Euler factors deleted.MonoidHom.galoisCharacterWeight_mul: the weight of a product of characters is the product of their weights.MonoidHom.val_galoisCharacterUnitaryWeight: the unitary packaging has the same underlying weight.MonoidHom.norm_galoisCharacterWeight_le_one: the weight of a Galois character is bounded by1.MonoidHom.summable_idealTerm_galoisCharacterWeight: the ideal series of a Galois character converges absolutely onRe s > 1.
Implementation notes #
The weight is packaged as a TauCeti.MultiplicativeIdealWeight K rather than as a bare function
Ideal (𝓞 K) → ℂ, so that the totality above is expressed in the carrier's own badPrimes API:
the bad primes of χ.galoisCharacterWeight are exactly ramifiedPrimes K L.
TauCeti.UnitaryIdealWeight K is the subtype of those multiplicative weights whose values have
modulus 1 away from the bad primes, so the unitary packaging records strictly more than the
multiplicative one and is not a replacement for it: galoisCharacterWeight remains the definition
everything else is stated about, and val_galoisCharacterUnitaryWeight is the bridge. Unitarity is
a property of the weight rather than of χ, so no hypothesis constrains χ itself to the unit
circle.
References #
Adapted from galoisCharacterOnIdeal, galoisCharacterOnIdeal_mul and
norm_galoisCharacterOnIdeal_le_one in CebotarevDensity/ZetaProduct.lean of
CBirkbeck/chebotarev-density (Apache-2.0,
Birkbeck--Brasca) at commit 8575c9df1ae0a61120ab5c964c7911414254bec7, following Sharifi,
Algebraic Number Theory, Notation 7.1.17. The factorization-product definition and the
Multiset.map_add/Multiset.prod_add multiplicativity argument are the source's; the
MultiplicativeIdealWeight packaging and the artinSymbol totalization are not the source's and
are new here. The source likewise names the construction for a general Galois character.
The ideal weight of a Galois character χ, packaged as a MultiplicativeIdealWeight. On a
height-one prime it is χ (Frob 𝔭) at the unramified primes and 0 at the ramified ones, extended
to all ideals completely multiplicatively through the prime factorization.
Instances For
Value at an unramified prime. At a height-one prime unramified in L the weight is χ of
the Artin symbol; together with the vanishing at ramified primes and complete multiplicativity this
determines the weight.
The weight vanishes at a height-one prime exactly when that prime ramifies in L. This is what
makes the weight total: the bad primes are not left unconstrained, they are pinned to 0.
The bad primes of the weight are exactly the ramified primes.
The weight of the trivial character is the indicator of the ideals prime to the ramified
primes. Its L-series is therefore the Dedekind zeta function of K with the Euler factors at the
ramified primes deleted (TauCeti.LSeries_ofBadPrimes).
The weight of a product of characters is the product of their weights. Both sides vanish
at the ramified primes and agree with χ ψ of the Artin symbol at the others. The weight of the
trivial character is not the trivial weight (galoisCharacterWeight_one), so this is
multiplicativity without a unit.
The weight of a Galois character is unitary. Its values have modulus 1 at every
unramified prime, and 0 at the ramified ones — which is exactly the UnitaryIdealWeight
contract, badPrimes being the ramified set by badPrimes_galoisCharacterWeight.
The underlying weight is galoisCharacterWeight χ itself, by
val_galoisCharacterUnitaryWeight. No hypothesis beyond multiplicativity is placed on χ; in
particular it is not assumed to take values in the unit circle.
Instances For
The unitary packaging has the same underlying weight.
The weight of a Galois character is bounded by 1.
The ideal series of a Galois character weight converges absolutely on Re s > 1.