Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_TwistedUnipotentTerm_SemiLocalOrbitalVocab.lean

definition module

Semi-local unipotent orbital integrals and twisted local factors

Throughout, L/K is an extension of number fields, v a nonzero prime of \mathcal O_K, and A_v = L\otimes_K K_v the semi-local algebra above v; w ranges over the type v.Extension (π“ž L) of extensions of v to \mathcal O_L, with associated completion L_w. Four elementary constructions come first: semiLocalUnipotent is the unit of \mathrm{GL}_2(A_v) with value \begin{pmatrix}1&x\\0&1\end{pmatrix} and inverse \begin{pmatrix}1&-x\\0&1\end{pmatrix}; semiLocalCentral sends \zeta \in A_v^{\times} to the scalar unit \mathrm{diag}(\zeta,\zeta), the image of \zeta under Matrix.scalar (Fin 2); semiLocalUnitComponent transports \zeta along the base-change isomorphism HeightOneSpectrum.adicCompletion.baseChangeAlgEquiv K L (π“ž L) v identifying A_v with \prod_{w} L_w and evaluates at a chosen w, yielding a unit of L_w; and semiLocalCharacter, for a homomorphism \xi_L from the full subgroup \top of (\mathbb A_L)^{\times} to \mathbb C^{\times}, is the finitely-supported product over all w \mid v of \xi_L evaluated at the determinant of NumberField.AdelicLevel.heckeGenAt (π“ž L) L w.1 applied to the w-component of \zeta (membership in \top being automatic). Next, wordIndicator, given m elements r_1,\dots,r_m and an element z of \mathrm{GL}_2(L_w) and numbers k,j, is the sum over all \iota : \mathrm{Fin}\,k \to \mathrm{Fin}\,m of the \{0,1\}-valued indicator of AutomorphicForm.semiLocalIntegralSet K L v evaluated at \iota_w(r_{\iota(0)}\cdots r_{\iota(k-1)}z^{j})^{-1}x, where the ordered word is placed at w inside \mathrm{GL}_2 of the finite adeles of L by AdelicDock.localEmbed and its semi-local component at v is read off by AutomorphicForm.semiLocalComponent. Then unipotentOrbitalFn sends x \in A_v to \int_{A_v^{\times}} \xi_v(\zeta)\big(\int_{\mathcal K} \mathbf 1_{k,j}(\kappa^{-1}\,\mathrm{diag}(\zeta,\zeta)\,n(x))\,d\kappa\big)d\zeta, the inner integral over AutomorphicForm.semiLocalIntegralSet against AutomorphicForm.semiLocalHaar and the outer one against Haar measure on A_v^{\times}.

Two further definitions sit outside the namespace. twistedLocalFactor is the function on K_v obtained by applying AutomorphicForm.AdelicTracePushforward.localTracePushforward K L v to TwistedUnipotentTerm.unipotentOrbitalFn: explicitly, r \mapsto \int \Phi\big((\,[L:K]\,)^{-1}\otimes r + \sum_i e_i \otimes w_i\big), the integral over tuples (w_i) indexed by a basis (e_i) of \ker(\mathrm{Tr}_{L/K}) against the product of the additive Haar measure on K_v normalised to give \mathcal O_v measure 1; besides the data above it takes an idele-theoretic Galois descent datum M4aHerbrand.IdeleGaloisDescent (π“ž L) K L and a K-automorphism \sigma of L as arguments, which index the definition without entering the value. Finally, IsJointFactorizableStandardOutside is the predicate on a function f on the adeles of a number field F, a finite set S of finite places, a function g on the infinite adele ring and a family h_v on the completions F_v, asserting that for every adele x, f(x) equals the value at x of the indicator of NumberField.TateGlobal.integralOutside S applied to x \mapsto g(x_\infty)\prod_{v\in S} h_v(x_v). It differs from NumberField.TateGlobal.IsFactorizableStandardOutside in treating the archimedean part as a single function on the infinite adeles rather than as a product over the infinite places.

Relation to Mathlib

Mathlib has no semi-local orbital integrals, word indicators or factorizability predicates of this kind; these are the project's own, built on Mathlib's adele rings, adic completions, general linear groups and Haar measure. IsJointFactorizableStandardOutside is a variant of the project's NumberField.TateGlobal.IsFactorizableStandardOutside.

Where it is used

These are the local ingredients of the unipotent contributions to a twisted trace formula for \mathrm{GL}_2 over an extension L/K with a central character of the ideles of L: the orbital function at v, its push-forward along the trace map to a function on K_v, and the shape condition under which a global test function is a product of such local factors and standard outside a finite set of places.

References

  1. H. Jacquet and R. P. Langlands, Automorphic Forms on GL(2), Lecture Notes in Mathematics 114, Springer, 1970
  2. R. P. Langlands, Base Change for GL(2), Annals of Mathematics Studies 96, Princeton University Press, 1980
  3. J. T. Tate, Fourier analysis in number fields and Hecke's zeta-functions, in: Algebraic Number Theory (J. W. S. Cassels and A. FrΓΆhlich, eds.), Academic Press, 1967, 305–347

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_AdelicDock_LocalEmbedding
import Definitions.Def_AutomorphicForm_AdelicTracePushforward
import Definitions.Def_NumberField_TateGlobalZeta

set_option autoImplicit false

open MeasureTheory NumberField IsDedekindDomain
open scoped TensorProduct

noncomputable section

namespace TwistedUnipotentTerm

section Definitions

noncomputable def semiLocalUnipotent
    (K L : Type) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L]
    (v : IsDedekindDomain.HeightOneSpectrum (π“ž K)) (x : L βŠ—[K] v.adicCompletion K) :
    GL (Fin 2) (L βŠ—[K] v.adicCompletion K) :=
  ⟨!![1, x; 0, 1], !![1, -x; 0, 1], by
    ext i j
    fin_cases i <;> fin_cases j <;> simp [Matrix.mul_apply, Fin.sum_univ_two], by
    ext i j
    fin_cases i <;> fin_cases j <;> simp [Matrix.mul_apply, Fin.sum_univ_two]⟩

noncomputable def semiLocalCentral
    (K L : Type) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L]
    (v : IsDedekindDomain.HeightOneSpectrum (π“ž K)) (ΞΆ : (L βŠ—[K] v.adicCompletion K)Λ£) :
    GL (Fin 2) (L βŠ—[K] v.adicCompletion K) :=
  Units.map (Matrix.scalar (Fin 2) : L βŠ—[K] v.adicCompletion K β†’+* Matrix (Fin 2) (Fin 2) _).toMonoidHom ΞΆ

noncomputable def semiLocalUnitComponent (K L : Type) [Field K] [NumberField K] [Field L] [NumberField L]
    [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (π“ž K)) (w : v.Extension (π“ž L))
    (ΞΆ : (L βŠ—[K] v.adicCompletion K)Λ£) : (w.1.adicCompletion L)Λ£ :=
  Units.map (Pi.evalMonoidHom (fun w' : v.Extension (π“ž L) => w'.1.adicCompletion L) w)
    (Units.mapEquiv (HeightOneSpectrum.adicCompletion.baseChangeAlgEquiv K L (π“ž L) v).toRingEquiv.toMulEquiv ΞΆ)

noncomputable def semiLocalCharacter (K L : Type) [Field K] [NumberField K] [Field L] [NumberField L]
    [Algebra K L] (ΞΎL : (⊀ : Subgroup (AdeleRing (π“ž L) L)Λ£) β†’* β„‚Λ£) (v : IsDedekindDomain.HeightOneSpectrum (π“ž K))
    (ΞΆ : (L βŠ—[K] v.adicCompletion K)Λ£) : β„‚ :=
  ∏ᢠ w : v.Extension (π“ž L),
    ((ξL ⟨Matrix.GeneralLinearGroup.det
        (NumberField.AdelicLevel.heckeGenAt (π“ž L) L w.1 (semiLocalUnitComponent K L v w ΞΆ)),
      Subgroup.mem_top _⟩ : β„‚Λ£) : β„‚)

noncomputable def wordIndicator (K L : Type) [Field K] [NumberField K] [Field L] [NumberField L]
    [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (π“ž K)) (w : v.Extension (π“ž L)) (m : β„•)
    (rT : Fin m β†’ GL (Fin 2) (w.1.adicCompletion L)) (z : GL (Fin 2) (w.1.adicCompletion L)) (k j : β„•)
    (x : GL (Fin 2) (L βŠ—[K] v.adicCompletion K)) : β„‚ :=
  βˆ‘ ΞΉ : Fin k β†’ Fin m,
    (AutomorphicForm.semiLocalIntegralSet K L v).indicator (fun _ => (1 : β„‚))
      ((AutomorphicForm.semiLocalComponent K L v (AdelicDock.localEmbed (π“ž L) L w.1
        ((List.ofFn fun i => rT (ι i)).prod * z ^ j)))⁻¹ * x)

open scoped TensorProduct.RightActions in

noncomputable def unipotentOrbitalFn (K L : Type) [Field K] [NumberField K] [Field L] [NumberField L]
    [Algebra K L] (ΞΎL : (⊀ : Subgroup (AdeleRing (π“ž L) L)Λ£) β†’* β„‚Λ£) (v : IsDedekindDomain.HeightOneSpectrum (π“ž K))
    (w : v.Extension (π“ž L)) (m : β„•) (rT : Fin m β†’ GL (Fin 2) (w.1.adicCompletion L))
    (z : GL (Fin 2) (w.1.adicCompletion L)) (k j : β„•) (x : L βŠ—[K] v.adicCompletion K) : β„‚ :=
  letI : MeasurableSpace (GL (Fin 2) (L βŠ—[K] v.adicCompletion K)) :=
    AutomorphicForm.glBorelOf (L βŠ—[K] v.adicCompletion K)
  haveI := AutomorphicForm.isTopologicalRing_tensor K L (v.adicCompletion K)
  haveI := AutomorphicForm.t2Space_tensor K L (v.adicCompletion K)
  haveI := AutomorphicForm.locallyCompactSpace_tensor K L (v.adicCompletion K)
  haveI : LocallyCompactSpace (L βŠ—[K] v.adicCompletion K)Λ£ :=
    Units.isClosedEmbedding_embedProduct.locallyCompactSpace
  letI : MeasurableSpace (L βŠ—[K] v.adicCompletion K)Λ£ := borel _
  haveI : BorelSpace (L βŠ—[K] v.adicCompletion K)Λ£ := ⟨rfl⟩
  ∫ ΞΆ : (L βŠ—[K] v.adicCompletion K)Λ£,
    semiLocalCharacter K L ΞΎL v ΞΆ *
      ∫ κ in AutomorphicForm.semiLocalIntegralSet K L v,
        wordIndicator K L v w m rT z k j (κ⁻¹ * semiLocalCentral K L v ΢ * semiLocalUnipotent K L v x)
          βˆ‚(AutomorphicForm.semiLocalHaar K L v)
    βˆ‚(Measure.haar : Measure (L βŠ—[K] v.adicCompletion K)Λ£)

end Definitions

end TwistedUnipotentTerm

section RootDefinitions

open AutomorphicForm in

noncomputable def twistedLocalFactor
    (K L : Type) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L]
    (D : M4aHerbrand.IdeleGaloisDescent (π“ž L) K L) (Οƒ : L ≃ₐ[K] L)
    (ΞΎL : (⊀ : Subgroup (AdeleRing (π“ž L) L)Λ£) β†’* β„‚Λ£) (v : HeightOneSpectrum (π“ž K)) (w : v.Extension (π“ž L))
    (m : β„•) (rT : Fin m β†’ GL (Fin 2) (w.1.adicCompletion L)) (z : GL (Fin 2) (w.1.adicCompletion L)) (k j : β„•) :
    v.adicCompletion K β†’ β„‚ :=
  have _ := D
  have _ := Οƒ
  letI : MeasurableSpace (v.adicCompletion K) := borel _
  haveI : BorelSpace (v.adicCompletion K) := ⟨rfl⟩
  AdelicTracePushforward.localTracePushforward K L v (TwistedUnipotentTerm.unipotentOrbitalFn K L ΞΎL v w m rT z k j)

def IsJointFactorizableStandardOutside {F : Type} [Field F] [NumberField F] (f : AdeleRing (π“ž F) F β†’ β„‚)
    (S : Finset (HeightOneSpectrum (π“ž F))) (g : InfiniteAdeleRing F β†’ β„‚)
    (h : (v : HeightOneSpectrum (π“ž F)) β†’ v.adicCompletion F β†’ β„‚) : Prop :=
  βˆ€ x, f x = (NumberField.TateGlobal.integralOutside S).indicator
    (fun x => g x.1 * ∏ v ∈ S, h v ((x.2 : FiniteAdeleRing (π“ž F) F) v)) x

end RootDefinitions

end

Statements phrased using this module (42)