Global number fields, ray classes, adeles, and Hecke characters

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe ray class ideal count#

For every modulus 𝔪 there is a power saving δ > 0 such that, in each ray class c of 𝔪, the number of nonzero integral ideals prime to 𝔪 of norm at most x is rayClassIdealMainTerm 𝔪 * x + O(x ^ (1 - δ)). One can take δ = 1 / [K : ℚ]; for that explicit exponent, use isBigO_rayClassIdealCountingFunction_sub instead.

TauCeti.GlobalNumberFields.rayClassIdealCount.{u_1} {K : Type u_1} [Field K] [NumberField K]
  (𝔪 : TauCeti.GlobalNumberFields.Modulus K) :
  ∃ δ,
    0 < δ ∧
      ∀ (c : TauCeti.GlobalNumberFields.RayClassGroup 𝔪),
        (fun x =>
            ↑(TauCeti.GlobalNumberFields.rayClassIdealCountingFunction 𝔪 c x) -
              TauCeti.GlobalNumberFields.rayClassIdealMainTerm 𝔪 * x) =O[Filter.atTop]
          fun x => x ^ (1 - δ)
Lean

Formalized in Tau Ceti as TauCeti.GlobalNumberFields.rayClassIdealCount.

Sources
LeanTauCeti.GlobalNumberFields.rayClassIdealCount

TheoremFinite-order Hecke characters are exactly the ray class characters#

a Hecke character has finite order exactly when it is the pullback of a ray class character of some modulus.

TauCeti.GlobalNumberFields.HeckeCharacter.isFiniteOrder_iff_exists_rayClassCharacter.{u_1}
  {K : Type u_1} [Field K] [NumberField K] (χ : TauCeti.GlobalNumberFields.HeckeCharacter K) :
  χ.IsFiniteOrder ↔ ∃ 𝔪 η, (TauCeti.GlobalNumberFields.HeckeCharacter.ofRayClassCharacter 𝔪) η = χ
Lean

Formalized in Tau Ceti as TauCeti.GlobalNumberFields.HeckeCharacter.isFiniteOrder_iff_exists_rayClassCharacter.

Sources
LeanTauCeti.GlobalNumberFields.HeckeCharacter.isFiniteOrder_iff_exists_rayClassCharacter
Uses 1 · Used by 1
Proof usesIsDedekindDomain.FiniteAdeleRing.sIntegralAdeles
Used byThe infinite part of the conductor is the set of real signs

TheoremThe infinite part of the conductor is the set of real signs#

A real place w divides the conductor of a finite-order Hecke character exactly when its real parity at w is one, that is, when the character is nontrivial on the negative elements of K_w.

TauCeti.GlobalNumberFields.HeckeCharacter.mem_conductor_infinitePart_iff.{u_1} {K : Type u_1}
  [Field K] [NumberField K] {χ : TauCeti.GlobalNumberFields.HeckeCharacter K} (hχ : χ.IsFiniteOrder)
  (w : { w // w.IsReal }) : w ∈ (χ.conductor hχ).infinitePart ↔ χ.infinityType.realParity w = 1
Lean

Formalized in Tau Ceti as TauCeti.GlobalNumberFields.HeckeCharacter.mem_conductor_infinitePart_iff.

Sources
LeanTauCeti.GlobalNumberFields.HeckeCharacter.mem_conductor_infinitePart_iff
Uses 2
Proof usesFinite-order Hecke characters are exactly the ray class characters · IsDedekindDomain.FiniteAdeleRing.sIntegralAdeles

DefinitionThe ray class group of ℚ modulo (n)·∞ is the Galois group of ℚ(ζ_n)#

The composite of ratModulusEquivZMod with the inverse of Mathlib's galEquivZMod: a ray class with residue a ∈ (ZMod n)ˣ goes to the automorphism acting on the n-th roots of unity by ζ ↦ ζ ^ a. It sends the ray class of a prime p ∤ n to the arithmetic Frobenius at p (isArithFrobAt_iff_eq_ratModulusEquivGal_idealClass).

TauCeti.GlobalNumberFields.ratModulusEquivGal.{u_1} (n : ℕ) [NeZero n] (F : Type u_1) [Field F]
  [NumberField F] [IsCyclotomicExtension {n} ℚ F] :
  TauCeti.GlobalNumberFields.RayClassGroup (TauCeti.GlobalNumberFields.ratModulus n ⋯) ≃* Gal(F/ℚ)
Lean

Formalized in Tau Ceti as TauCeti.GlobalNumberFields.ratModulusEquivGal.

Sources
LeanTauCeti.GlobalNumberFields.ratModulusEquivGal
Used by 1
Used byThe Kronecker–Weber theorem

TheoremThe congruence description of the Picard group#

A ray class of the conductor maps to the trivial Picard class exactly when it is the ray class of an ideal of 𝓞 K generated by an element of the order.

TauCeti.GlobalNumberFields.NumberFieldOrder.mem_ker_rayClassToPic.{u_1} {K : Type u_1} [Field K]
  [NumberField K] (O : TauCeti.GlobalNumberFields.NumberFieldOrder K)
  {c : TauCeti.GlobalNumberFields.RayClassGroup O.conductorModulus} :
  c ∈ O.rayClassToPic.ker ↔
    ∃ J,
      (TauCeti.GlobalNumberFields.idealClass O.conductorModulus) J = c ∧
        ∃ β ∈ O.toRingOfIntegers, ↑J = Ideal.span {β}
Lean

Formalized in Tau Ceti as TauCeti.GlobalNumberFields.NumberFieldOrder.mem_ker_rayClassToPic.

Sources
LeanTauCeti.GlobalNumberFields.NumberFieldOrder.mem_ker_rayClassToPic

TheoremThe congruence description of the narrow Picard group#

A ray class of the narrow conductor modulus maps to the trivial narrow Picard class exactly when it is the ray class of an ideal of 𝓞 K generated by a totally positive element of the order.

TauCeti.GlobalNumberFields.NumberFieldOrder.mem_ker_rayClassToNarrowPic.{u_1} {K : Type u_1}
  [Field K] [NumberField K] (O : TauCeti.GlobalNumberFields.NumberFieldOrder K)
  {c : TauCeti.GlobalNumberFields.RayClassGroup O.narrowConductorModulus} :
  c ∈ O.rayClassToNarrowPic.ker ↔
    ∃ J,
      (TauCeti.GlobalNumberFields.idealClass O.narrowConductorModulus) J = c ∧
        ∃ β ∈ O.toRingOfIntegers, NumberField.IsTotallyPositive ↑β ∧ ↑J = Ideal.span {β}
Lean

Formalized in Tau Ceti as TauCeti.GlobalNumberFields.NumberFieldOrder.mem_ker_rayClassToNarrowPic.

Sources
LeanTauCeti.GlobalNumberFields.NumberFieldOrder.mem_ker_rayClassToNarrowPic

TheoremAn order is Gorenstein exactly when all of its proper fractional ideals are invertible# 

TauCeti.GlobalNumberFields.NumberFieldOrder.isGorenstein_iff_forall_isUnit.{u} {K : Type u}
  [Field K] [NumberField K] (O : TauCeti.GlobalNumberFields.NumberFieldOrder K) :
  O.IsGorenstein ↔
    ∀ (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K),
      O.IsProperFractionalIdeal I → IsUnit I
Lean

Formalized in Tau Ceti as TauCeti.GlobalNumberFields.NumberFieldOrder.isGorenstein_iff_forall_isUnit.

Sources
LeanTauCeti.GlobalNumberFields.NumberFieldOrder.isGorenstein_iff_forall_isUnit

DefinitionIsDedekindDomain.FiniteAdeleRing.sIntegralAdeles#

The S-integral finite adeles ∏_{v ∈ S} K_v × ∏_{v ∉ S} 𝒪_v: the finite adeles that are integral at every finite place outside S, as an R-subalgebra of the finite adele ring. For S = ∅ these are the integral finite adeles, and every finite adele is S-integral for some finite S.

IsDedekindDomain.FiniteAdeleRing.sIntegralAdeles.{u_1, u_2} (R : Type u_1) [CommRing R]
  [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K]
  (S : Set (IsDedekindDomain.HeightOneSpectrum R)) :
  Subalgebra R (IsDedekindDomain.FiniteAdeleRing R K)
Lean

Formalized in Tau Ceti as IsDedekindDomain.FiniteAdeleRing.sIntegralAdeles.

Sources
LeanIsDedekindDomain.FiniteAdeleRing.sIntegralAdeles
Used by 4
Used byFinite-order Hecke characters are exactly the ray class characters · The idele class group splits as C_K¹ × ℝ>0 · The infinite part of the conductor is the set of real signs · The Kronecker–Weber theorem

DefinitionThe idele class group splits as C_K¹ × ℝ>0#

The infinite place w determines the isomorphism of topological groups sending an idele class c to its norm-one part c · s(‖c‖)⁻¹ and its norm ‖c‖, where s = ideleClassNormSection K w.

TauCeti.GlobalNumberFields.normOneProdEquiv.{u_1} {K : Type u_1} [Field K] [NumberField K]
  (w : NumberField.InfinitePlace K) :
  NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K ≃ₜ*
    ↥(TauCeti.GlobalNumberFields.IdeleClassGroup.normOne K) × NNRealˣ
Lean

Formalized in Tau Ceti as TauCeti.GlobalNumberFields.normOneProdEquiv.

Sources
LeanTauCeti.GlobalNumberFields.normOneProdEquiv
Uses 1
Proof usesIsDedekindDomain.FiniteAdeleRing.sIntegralAdeles

TheoremBase change of adeles in a tower K ⊆ L ⊆ M#

the comparison for M/K factors through the comparison for L/K, followed by the comparison for M/L.

TauCeti.GlobalNumberFields.adeleBaseChangeEquiv_tower.{u_1, u_2, u_3} (K : Type u_1) (L : Type u_2)
  [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L]
  [TopologicalSpace (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)]
  [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)
      (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)]
  (M : Type u_3) [Field M] [NumberField M] [Algebra K M] [Algebra L M] [IsScalarTower K L M]
  [TopologicalSpace (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) M)]
  [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)
      (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) M)]
  [TopologicalSpace (TensorProduct L (NumberField.AdeleRing (NumberField.RingOfIntegers L) L) M)]
  [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)
      (TensorProduct L (NumberField.AdeleRing (NumberField.RingOfIntegers L) L) M)]
  (a : NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (z : M) :
  (TauCeti.GlobalNumberFields.adeleBaseChangeEquiv K M) (a ⊗ₜ[K] z) =
    (TauCeti.GlobalNumberFields.adeleBaseChangeEquiv L M)
      ((TauCeti.GlobalNumberFields.adeleBaseChangeEquiv K L) (a ⊗ₜ[K] 1) ⊗ₜ[L] z)
Lean

Formalized in Tau Ceti as TauCeti.GlobalNumberFields.adeleBaseChangeEquiv_tower.

Sources
LeanTauCeti.GlobalNumberFields.adeleBaseChangeEquiv_tower
Uses 1
Proof usesThe semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w

TheoremEuler's formula#

the trace dual of a monogenic order ℤ[x] is generated by the inverse of the derivative of the minimal polynomial of x, evaluated at x.

TauCeti.GlobalNumberFields.NumberFieldOrder.traceDual_eq_spanSingleton_of_toSubalgebra_eq_adjoin.{u}
  {K : Type u} [Field K] [NumberField K] {O : TauCeti.GlobalNumberFields.NumberFieldOrder K} {x : K}
  (hx : O.toSubalgebra = ℤ[x]) :
  O.traceDual =
    (FractionalIdeal.spanSingleton (nonZeroDivisors ↥O.toSubalgebra))
      ((Polynomial.aeval x) (Polynomial.derivative (minpoly ℚ x)))⁻¹
Lean

Formalized in Tau Ceti as TauCeti.GlobalNumberFields.NumberFieldOrder.traceDual_eq_spanSingleton_of_toSubalgebra_eq_adjoin.

Sources
LeanTauCeti.GlobalNumberFields.NumberFieldOrder.traceDual_eq_spanSingleton_of_toSubalgebra_eq_adjoin

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.