`Definitions/Def_NumberField_RayCharacterData.lean`

definition module

Hecke character data: signs, parity, primitivity, Gauss sums

Throughout, K is a number field, \mathfrak f an ideal of \mathcal O_K, and \chi a monoid homomorphism from the narrow ray class group \mathrm{NarrowRayClassGroup}\,K\,\mathfrak f to \mathbb C; that group is the quotient of the subgroup coprimeToModulus of invertible fractional ideals whose multiplicity vanishes at every height-one prime dividing \mathfrak f by the subgroup generated by the ideals (\alpha) with \alpha\neq 0, \alpha\equiv 1 \pmod{\mathfrak f} and \tau(\alpha)>0 for every ring homomorphism \tau : K\to\mathbb R. For a finite set S of real infinite places, signAt sends x\in K to the product over v\in S of the signs of the real embeddings attached to v, viewed in \mathbb C. chiIdeal extends \chi to all fractional ideals: the value at I is \chi of the class of I when I\neq0 and I, as a unit, lies in coprimeToModulus, and 0 otherwise. IsParity K 𝔣 χ S asserts that \chi of the principal ideal (\alpha) equals \mathrm{signAt}\,S\,\alpha for every \alpha\neq0 with \alpha-1\in\mathfrak f (no positivity being imposed on \alpha), and chiFin is the sign-corrected value \chi((\alpha))\cdot \mathrm{signAt}\,S\,\alpha. IsPrimitiveMod K 𝔣 χ is the witness form of primitivity: for every ideal \mathfrak f' with \mathfrak f\subseteq\mathfrak f' and \mathfrak f'\neq\mathfrak f there is a totally positive \alpha\neq0 with \alpha-1\in\mathfrak f' whose value \chi((\alpha)) is neither 0 nor 1. addChar is x\mapsto \exp(2\pi i\,\mathrm{Tr}_{K/\mathbb Q}(x)). Given \mathfrak f\neq 0, which makes \mathcal O_K/\mathfrak f finite, gaussSumAt at y\in K is \mathrm{signAt}\,S\,y times \chi of (y)\,\mathfrak f\,\mathfrak d, \mathfrak d=\mathrm{differentIdeal}\ \mathbb Z\ \mathcal O_K, times \sum_{r\in\mathcal O_K/\mathfrak f}\mathrm{chiFin}(r)\,\mathrm{addChar}(r y), the sum being taken over chosen representatives of the residues. Finally IsGaussDatum K 𝔣 χ y requires y\neq0, \mathrm{Tr}_{K/\mathbb Q}(\alpha y)\in\mathbb Z for all \alpha\in\mathfrak f, and \chi((y)\,\mathfrak f\,\mathfrak d)\neq0. Two degenerate cases are recorded: the trivial character with S=\varnothing satisfies IsParity, and every character modulo \mathfrak f=\top satisfies IsPrimitiveMod, there being no ideal strictly containing \top.

Relation to Mathlib

The narrow ray class group used here is the project's own construction; the ingredients taken from Mathlib are fractional ideals and their multiplicities, infinite places together with the real embedding attached to a real place, the trace form, and the different ideal differentIdeal. The Gauss sums defined here are sums attached to a Hecke character of a number field, not instances of Mathlib's gaussSum for characters of finite fields.

Where it is used

This module fixes the vocabulary — extension of a narrow ray class character to fractional ideals, its sign pattern at real places, parity, primitivity and the associated Gauss sums — shared by the statements about Hecke characters of number fields in this part of the development.

References

J. Neukirch, Algebraic Number Theory, Grundlehren der mathematischen Wissenschaften 322, Springer, 1999, Ch. VI–VII
W. Narkiewicz, Elementary and Analytic Theory of Algebraic Numbers, 3rd ed., Springer Monographs in Mathematics, Springer, 2004

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

86 lines
10 declarations
used in the statements of 5 theorems and imported by 8 proofs
imports 1 definition modules

Source file: Definitions/Def_NumberField_RayCharacterData.lean

Imports

Def_NarrowRayClassGroup

Imported by

Def_NumberField_NormResidueCharacter

Source

import Definitions.Def_NarrowRayClassGroup
import Mathlib.RingTheory.DedekindDomain.Different ↗

set_option autoImplicit false

noncomputable section

namespace M4aP2

open Real NumberField NumberField.InfinitePlace Deep.NTSupply
open scoped nonZeroDivisors Classical

variable (K : Type) [Field K] [NumberField K]

def signAt (S : Finset {w : InfinitePlace K // IsReal w}) (x : K) : ℂ :=
  ∏ v ∈ S, ((SignType.sign (embedding_of_isReal v.2 x) : ℤ) : ℂ)

variable (𝔣 : Ideal (𝓞 K)) (χ : NarrowRayClassGroup K 𝔣 →* ℂ)

def chiIdeal (I : FractionalIdeal (𝓞 K)⁰ K) : ℂ :=
  if h : I ≠ 0 then
    (if hc : Units.mk0 I h ∈ coprimeToModulus K 𝔣
      then χ (NarrowRayClassGroup.mk K 𝔣 ⟨Units.mk0 I h, hc⟩) else 0)
  else 0

def IsParity (S : Finset {w : InfinitePlace K // IsReal w}) : Prop :=
  ∀ α : 𝓞 K, α ≠ 0 → α - 1 ∈ 𝔣 →
    chiIdeal K 𝔣 χ ((Ideal.span {α} : Ideal (𝓞 K)) : FractionalIdeal (𝓞 K)⁰ K) = signAt K S (α : K)

def chiFin (S : Finset {w : InfinitePlace K // IsReal w}) (α : 𝓞 K) : ℂ :=
  chiIdeal K 𝔣 χ ((Ideal.span {α} : Ideal (𝓞 K)) : FractionalIdeal (𝓞 K)⁰ K) * signAt K S (α : K)

def IsPrimitiveMod : Prop :=
  ∀ 𝔣' : Ideal (𝓞 K), 𝔣 ≤ 𝔣' → 𝔣' ≠ 𝔣 →
    ∃ α : 𝓞 K, α ≠ 0 ∧ α - 1 ∈ 𝔣' ∧ (∀ τ : K →+* ℝ, 0 < τ (α : K)) ∧
      chiIdeal K 𝔣 χ ((Ideal.span {α} : Ideal (𝓞 K)) : FractionalIdeal (𝓞 K)⁰ K) ≠ 0 ∧
      chiIdeal K 𝔣 χ ((Ideal.span {α} : Ideal (𝓞 K)) : FractionalIdeal (𝓞 K)⁰ K) ≠ 1

def addChar (x : K) : ℂ :=
  Complex.exp (2 * π * Complex.I * (Algebra.trace ℚ K x : ℂ))

def gaussSumAt (h𝔣 : 𝔣 ≠ ⊥) (S : Finset {w : InfinitePlace K // IsReal w}) (y : K) : ℂ :=
  haveI := Ideal.finiteQuotientOfFreeOfNeBot 𝔣 h𝔣
  haveI : Fintype (𝓞 K ⧸ 𝔣) := Fintype.ofFinite _
  signAt K S y
    * chiIdeal K 𝔣 χ (FractionalIdeal.spanSingleton (𝓞 K)⁰ y * (𝔣 : FractionalIdeal (𝓞 K)⁰ K)
        * ((differentIdeal ℤ (𝓞 K) : Ideal (𝓞 K)) : FractionalIdeal (𝓞 K)⁰ K))
    * ∑ r : 𝓞 K ⧸ 𝔣, chiFin K 𝔣 χ S (Quotient.out r) * addChar K ((Quotient.out r : 𝓞 K) * y)

def IsGaussDatum (y : K) : Prop :=
  y ≠ 0 ∧ (∀ α : 𝓞 K, α ∈ 𝔣 → (Algebra.trace ℚ K ((α : K) * y) : ℚ) ∈ (algebraMap ℤ ℚ).range) ∧
    chiIdeal K 𝔣 χ (FractionalIdeal.spanSingleton (𝓞 K)⁰ y * (𝔣 : FractionalIdeal (𝓞 K)⁰ K)
        * ((differentIdeal ℤ (𝓞 K) : Ideal (𝓞 K)) : FractionalIdeal (𝓞 K)⁰ K)) ≠ 0

theorem isParity_one_empty : IsParity K 𝔣 (1 : NarrowRayClassGroup K 𝔣 →* ℂ) ∅ := by
  intro α hα h1
  have hne : ((Ideal.span {α} : Ideal (𝓞 K)) : FractionalIdeal (𝓞 K)⁰ K) ≠ 0 := by
    rw [Ne, FractionalIdeal.coeIdeal_eq_zero, Ideal.span_singleton_eq_bot]
    exact hα
  have hcop : Units.mk0 _ hne ∈ coprimeToModulus K 𝔣 := by
    have h := principalUnit_mem_coprimeToModulus K hα h1
    rw [mem_coprimeToModulus_iff] at h ⊢
    intro v hv
    have := h v hv
    rwa [principalUnit_val] at this
  rw [chiIdeal, dif_pos hne, dif_pos hcop, MonoidHom.one_apply, signAt, Finset.prod_empty]

theorem isPrimitiveMod_top (χ' : NarrowRayClassGroup K ⊤ →* ℂ) : IsPrimitiveMod K ⊤ χ' := by
  intro 𝔣' hle hne
  exact absurd (top_le_iff.mp hle) hne

end M4aP2

end

#print axioms M4aP2.signAt
#print axioms M4aP2.chiIdeal
#print axioms M4aP2.IsParity
#print axioms M4aP2.chiFin
#print axioms M4aP2.IsPrimitiveMod
#print axioms M4aP2.addChar
#print axioms M4aP2.gaussSumAt
#print axioms M4aP2.IsGaussDatum
#print axioms M4aP2.isParity_one_empty
#print axioms M4aP2.isPrimitiveMod_top

Statements phrased using this module (5)

Functional equation of completed narrow ray class L-functions M4aTorus.completedRayL_fe 0 below · depth 14
Hecke's functional equation for narrow class characters NumberField.exists_completedRayL_functionalEquation_of_modulus_top 0 below · depth 14
Existence of a Gauss datum for a narrow ray class character NumberField.exists_isGaussDatum 0 below · depth 14
Logarithm of a narrow ray class L-series as a prime sum NumberField.exists_continuousOn_exp_eq_rayClassLSeries 0 below · depth 16
Entireness of non-trivial narrow ray class L-series (Hecke) NumberField.exists_differentiable_eq_rayClassLSeries_of_ne_one 1 below · depth 16