Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LanglandsTunnell_RankinSelbergEuler.lean

definition module

Induced Euler factors and Rankin–Selberg -data

Throughout, F is a field (a number field in the final section) and K a field with a ring map \mathcal{O}_F \to \mathcal{O}_K making \mathcal{O}_K integral over \mathcal{O}_F; R is a commutative ring. For a height-one prime \mathfrak{p} of \mathcal{O}_F, primeFibre F K p is the set of height-one primes \mathfrak{P} of \mathcal{O}_K whose contraction to \mathcal{O}_F equals \mathfrak{p}, with mem_primeFibre recording membership as that equality. Given c from the height-one primes of \mathcal{O}_K to R, inducedFactor F c 𝔓 is the polynomial 1 - c(\mathfrak{P})X^{f}, where f is the inertia degree of \mathfrak{P} over its contraction, and inducedEulerPoly F c p is the product (a finprod, hence finite support) of these factors over the fibre above \mathfrak{p}. Its coefficients give inducedE1, inducedE2, inducedE3, namely -\,(coefficient of X), the coefficient of X^2, and -\,(coefficient of X^3).

rsEulerPoly a b e₁ e₂ e₃ is an explicit degree-6 polynomial over R with constant term 1 and coefficients given by universal polynomial expressions in a,b,e_1,e_2,e_3. The private identity rsEulerPoly_eq_prod states that substituting for (a,b) the first two elementary symmetric functions of \alpha_1,\alpha_2 and for (e_1,e_2,e_3) the three elementary symmetric functions of \beta_1,\beta_2,\beta_3 yields \prod_{i,j}(1-\alpha_i\beta_j X).

Finally, for a number field F, a finite set S of primes, functions a,b on the primes of F, a function c on the primes of K, and four multisets of complex shift parameters, rsDatum assembles an LDatum indexed by the primes of F outside S: the norm at \mathfrak{p} is the absolute ideal norm, the Euler polynomial is rsEulerPoly evaluated at a(\mathfrak{p}),b(\mathfrak{p}) and the induced triple of c at \mathfrak{p}, the dual Euler polynomial is the same expression at a(\mathfrak{p})/b(\mathfrak{p}), b(\mathfrak{p})^{-1} and the induced triple of \mathfrak{P}\mapsto c(\mathfrak{P})^{-1}, the four gamma multisets are the given ones, and the abscissa, centre and degree are 1, 1/2 and 6.

Relation to Mathlib

Built on Mathlib's IsDedekindDomain.HeightOneSpectrum, Ideal.inertiaDeg' and Ideal.absNorm; the target structure LDatum, a purely formal package of Euler polynomials, gamma shifts, abscissa, centre and degree, is the project's own, Mathlib having no notion of an L-datum.

Where it is used

These definitions supply the Rankin–Selberg L-function data used in the Langlands–Tunnell part of the argument: inducedEulerPoly is the shape of the unramified Euler factor over F attached to a character of a cubic extension K/F, and rsDatum packages the degree-6 Euler products of such a factor against a two-dimensional one as a formal L-datum, to which the analytic criteria (WellFormed, Converges, IsNice) of the L-datum framework are then applied.

References

  1. H. Jacquet, I. I. Piatetski-Shapiro and J. A. Shalika, Rankin–Selberg convolutions, American Journal of Mathematics 105 (1983), 367–464
  2. R. P. Langlands, Base Change for GL(2), Annals of Mathematics Studies 96, Princeton University Press, 1980
  3. J. Tunnell, Artin's conjecture for representations of octahedral type, Bulletin of the American Mathematical Society (N.S.) 5 (1981), 173–175

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_LanglandsTunnell_RankinSelbergEuler.lean

Imports

Imported by

Declarations

Source

import Mathlib.Algebra.Polynomial.Basic ↗
import Mathlib.Algebra.BigOperators.Finprod ↗
import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas ↗
import Mathlib.RingTheory.Ideal.Norm.AbsNorm ↗
import Mathlib.NumberTheory.RamificationInertia.Inertia ↗
import Mathlib.NumberTheory.NumberField.Basic ↗
import Mathlib.Tactic.Ring ↗
import Definitions.Def_LanglandsTunnell_HonestLDatum

noncomputable section

open Polynomial IsDedekindDomain NumberField

namespace LanglandsTunnell.RankinSelberg

section Induced

variable (F : Type*) [Field F] {K : Type*} [Field K] [Algebra (𝓞 F) (𝓞 K)]
  [Algebra.IsIntegral (𝓞 F) (𝓞 K)] {R : Type*} [CommRing R]

variable (K) in

def primeFibre (p : HeightOneSpectrum (𝓞 F)) : Set (HeightOneSpectrum (𝓞 K)) :=
  {𝔓 | 𝔓.under (𝓞 F) = p}

@[simp] theorem mem_primeFibre (p : HeightOneSpectrum (𝓞 F)) (𝔓 : HeightOneSpectrum (𝓞 K)) :
    𝔓 ∈ primeFibre F K p ↔ 𝔓.under (𝓞 F) = p :=
  Iff.rfl

def inducedFactor (c : HeightOneSpectrum (𝓞 K) → R) (𝔓 : HeightOneSpectrum (𝓞 K)) : R[X] :=
  C 1 - C (c 𝔓) * X ^ ((𝔓.under (𝓞 F)).asIdeal.inertiaDeg' 𝔓.asIdeal)

def inducedEulerPoly (c : HeightOneSpectrum (𝓞 K) → R) (p : HeightOneSpectrum (𝓞 F)) : R[X] :=
  ∏ᶠ 𝔓 ∈ primeFibre F K p, inducedFactor F c 𝔓

def inducedE1 (c : HeightOneSpectrum (𝓞 K) → R) (p : HeightOneSpectrum (𝓞 F)) : R :=
  -(inducedEulerPoly F c p).coeff 1

def inducedE2 (c : HeightOneSpectrum (𝓞 K) → R) (p : HeightOneSpectrum (𝓞 F)) : R :=
  (inducedEulerPoly F c p).coeff 2

def inducedE3 (c : HeightOneSpectrum (𝓞 K) → R) (p : HeightOneSpectrum (𝓞 F)) : R :=
  -(inducedEulerPoly F c p).coeff 3

end Induced

section RankinSelberg

variable {R : Type*} [CommRing R]

def rsEulerPoly (a b e₁ e₂ e₃ : R) : R[X] :=
  C 1
    + C (-(a * e₁)) * X
    + C (a ^ 2 * e₂ + b * e₁ ^ 2 - 2 * b * e₂) * X ^ 2
    + C (-(a ^ 3 * e₃) - a * b * e₁ * e₂ + 3 * a * b * e₃) * X ^ 3
    + C (a ^ 2 * b * e₁ * e₃ - 2 * b ^ 2 * e₁ * e₃ + b ^ 2 * e₂ ^ 2) * X ^ 4
    + C (-(a * b ^ 2 * e₂ * e₃)) * X ^ 5
    + C (b ^ 3 * e₃ ^ 2) * X ^ 6

private theorem rsEulerPoly_eq_prod (α₁ α₂ β₁ β₂ β₃ : R) :
    rsEulerPoly (α₁ + α₂) (α₁ * α₂) (β₁ + β₂ + β₃) (β₁ * β₂ + β₁ * β₃ + β₂ * β₃)
        (β₁ * β₂ * β₃) =
      (C 1 - C (α₁ * β₁) * X) * (C 1 - C (α₁ * β₂) * X) * (C 1 - C (α₁ * β₃) * X) *
        ((C 1 - C (α₂ * β₁) * X) * (C 1 - C (α₂ * β₂) * X) * (C 1 - C (α₂ * β₃) * X)) := by
  simp only [rsEulerPoly, map_add, map_sub, map_neg, map_mul, map_pow, map_ofNat, map_one]
  ring

end RankinSelberg

section Datum

variable (F : Type*) [Field F] [NumberField F] {K : Type*} [Field K] [Algebra (𝓞 F) (𝓞 K)]
  [Algebra.IsIntegral (𝓞 F) (𝓞 K)]

def rsDatum (S : Finset (HeightOneSpectrum (𝓞 F))) (a b : HeightOneSpectrum (𝓞 F) → ℂ)
    (c : HeightOneSpectrum (𝓞 K) → ℂ) (gammaR gammaC gammaRDual gammaCDual : Multiset ℂ) :
    LDatum {p : HeightOneSpectrum (𝓞 F) // p ∉ S} where
  norm := fun p => Ideal.absNorm p.1.asIdeal
  euler := fun p =>
    rsEulerPoly (a p.1) (b p.1) (inducedE1 F c p.1) (inducedE2 F c p.1) (inducedE3 F c p.1)
  dual := fun p =>
    rsEulerPoly (a p.1 / b p.1) (b p.1)⁻¹ (inducedE1 F (fun 𝔓 => (c 𝔓)⁻¹) p.1)
      (inducedE2 F (fun 𝔓 => (c 𝔓)⁻¹) p.1) (inducedE3 F (fun 𝔓 => (c 𝔓)⁻¹) p.1)
  gammaR := gammaR
  gammaC := gammaC
  gammaRDual := gammaRDual
  gammaCDual := gammaCDual
  abscissa := 1
  center := 1 / 2
  degree := 6

end Datum

end LanglandsTunnell.RankinSelberg

end

Statements phrased using this module (280)

… and 130 more statements (search for the module name to find them).