Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_FrobeniusDensity_ClassGroupLSeries.lean

definition module

Partial Dedekind zeta functions and class-group -series

Throughout, K is a number field with ring of integers \mathcal{O}_K. For an ideal class C \in ClassGroup (π“ž K) and n : \mathbb{N}, classZetaCoeff K C n is the Nat.card of the subtype of elements I of the non-zero-divisor submonoid (\mathrm{Ideal}\,\mathcal{O}_K)^{0} of the multiplicative monoid of ideals (i.e. of nonzero integral ideals) satisfying absNorm I = n together with ClassGroup.mk0 I = C; so it counts the integral ideals of absolute norm n lying in the class C. The partial zeta function classZeta K C is Mathlib's LSeries applied to these coefficients, cast to \mathbb{C}, i.e. \sum_{n\ge 1} a_C(n) n^{-s} (the LSeries convention discards the index 0 term).

classResidue K is the real number \frac{2^{r_1}(2\pi)^{r_2} R_K}{w_K\sqrt{|d_K|}}, with r_1 = nrRealPlaces K, r_2 = nrComplexPlaces K, R_K = regulator K, w_K = torsionOrder K the order of the torsion subgroup of the units, and d_K = discr K; this is the analytic class number formula constant with the class number removed.

Characters are taken to be monoid homomorphisms \chi : ClassGroup (π“ž K) β†’* β„‚, so \chi(1) = 1 and the values are roots of unity. For such a \chi, classGroupLSeries K Ο‡ s is the finite sum \sum_{C} \chi(C)\,classZeta K C s over the class group.

Finally, LSeriesInheritsPole K Ο‡ is the predicate asserting the existence of a real c > 0 such that, eventually in the filter \mathcal{N}[>]1 of real numbers approaching 1 from above, c \le \|(s-1)\,classGroupLSeries K Ο‡ s\| (with s coerced to \mathbb{C}): the L-series retains a pole, rather than being regular, at s = 1.

Relation to Mathlib

Built on Mathlib's LSeries, ClassGroup/ClassGroup.mk0, absNorm, regulator, torsionOrder, discr and the counts of real and complex infinite places; the decomposition of the Dedekind zeta function into partial zeta functions of individual ideal classes, the associated class-group L-series and the pole predicate are the project's own.

Where it is used

These are the analytic objects used in the argument that the classes of the degree-one primes generate the ideal class group (the statement that an ideal class character trivial on degree-one primes is trivial), which feeds the class-group input of the Stickelberger–Herbrand branch.

References

  1. S. Lang, Algebraic Number Theory, 2nd edition, Graduate Texts in Mathematics 110, Springer, 1994, Chapter VIII
  2. J. Neukirch, Algebraic Number Theory, Grundlehren der mathematischen Wissenschaften 322, Springer, 1999, Chapter VII

References are suggested automatically and have not been individually verified.

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

Source file: Definitions/Def_FrobeniusDensity_ClassGroupLSeries.lean

Declarations

Source

import Mathlib

set_option autoImplicit false

open Filter Ideal NumberField NumberField.InfinitePlace NumberField.Units Topology
  nonZeroDivisors

open scoped Real

namespace FrobeniusDensity

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

noncomputable section

def classZetaCoeff (C : ClassGroup (π“ž K)) (n : β„•) : β„• :=
  Nat.card {I : (Ideal (π“ž K))⁰ // absNorm (I : Ideal (π“ž K)) = n ∧ ClassGroup.mk0 I = C}

def classZeta (C : ClassGroup (π“ž K)) (s : β„‚) : β„‚ :=
  LSeries (fun n ↦ classZetaCoeff K C n) s

def classResidue : ℝ :=
  (2 ^ nrRealPlaces K * (2 * Ο€) ^ nrComplexPlaces K * regulator K) /
    (torsionOrder K * Real.sqrt |discr K|)

def classGroupLSeries (Ο‡ : ClassGroup (π“ž K) β†’* β„‚) (s : β„‚) : β„‚ :=
  βˆ‘ C : ClassGroup (π“ž K), Ο‡ C * classZeta K C s

def LSeriesInheritsPole (Ο‡ : ClassGroup (π“ž K) β†’* β„‚) : Prop :=
  βˆƒ c : ℝ, 0 < c ∧
    βˆ€αΆ  s : ℝ in 𝓝[>] 1, c ≀ β€–(fun s : ℝ ↦ (s - 1) * classGroupLSeries K Ο‡ s) sβ€–

end

end FrobeniusDensity

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).