Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LanglandsTunnell_CubicInduction_WhittakerBlock.lean

definition module

Adelic unipotent subgroup, quotient measure, Whittaker blocks

The setting is G = \mathrm{GL}_3 over the adeles of \mathbb{Q}, with the Borel \sigma-algebras of \mathbb{A} and of AdelicGL 3 used locally inside each definition. unipotentSubgroup3 is the subgroup of AdelicGL 3 (π“ž β„š) β„š generated by the matrices upperUnipotent3 x y z for adelic x,y,z; two private computations record that these matrices multiply by the Heisenberg rule (x,y,z)\cdot(x',y',z') = (x+x', y+y', z+z'+xy') and invert as (-x,-y,xy-z), whence mem_unipotentSubgroup3_iff: membership in this subgroup is exactly being of the form upperUnipotent3 x y z. coe_unipotentSubgroup3_eq identifies the underlying set by the six entry conditions (the three diagonal entries equal 1, the three entries below the diagonal equal 0), and isClosed_unipotentSubgroup3 deduces that the subgroup is closed. unipotentHaar3 is the pushforward of the threefold product of the adelic additive Haar measure along (x,y,z)\mapsto \mathtt{upperUnipotent3}\,x\,y\,z, a measure on the subgroup for the induced Borel structure. quotientMeasure is the measure on the orbit space of the subgroup acting on AdelicGL 3 (π“ž β„š) β„š produced from the adelic Haar measure of \mathrm{GL}_3 and unipotentHaar3 by the general construction HaarQuotient.measure (a compact-exhaustion weight, normalised by its integral over the subgroup, pushed forward to the orbit space); the instance sigmaCompactSpace_adelicGL3 supplies the \sigma-compactness of AdelicGL 3 (π“ž β„š) β„š on which that construction depends. For a finite set S of finite places, zerothShell S is the set of orbits whose chosen representative has, at each finite place p \notin S, its p-component equal to a product upperUnipotent3 x y z * k with k in the local maximal compact subgroup. Finally block pins ψ f Ξ¦ Οƒ S is the [0,\infty]-valued lower integral over zerothShell S, against quotientMeasure, of \lVert \mathtt{whittaker3}\,\mathtt{pins}\,\psi\,f\rVert^2 times \lVert\Phi\rVert evaluated on the bottom row of the representative matrix, times the \sigma-th power of the idele norm of the determinant; here whittaker3 is the triple integral of f against \psi(-(x+y)) over the unipotent directions. The integrand is evaluated at the chosen orbit representative q.out, so these are definitions attached to a choice of representatives rather than functions shown to descend to the quotient.

Relation to Mathlib

Mathlib has no adelic \mathrm{GL}_3 Whittaker theory; the unipotent subgroup, its measure, the shell sets and the blocks are the project's own, and the quotient measure is built from the project's HaarQuotient.measure on the orbit space rather than from Mathlib's quotient-group Haar measures. The \sigma-compactness instance is obtained from Mathlib's closed-embedding results applied to the embedding of the unit group into matrices and their opposite.

Where it is used

These objects belong to the cubic-induction package for Langlands–Tunnell: they provide the measure-theoretic framework (Whittaker functions on \mathrm{GL}_3(\mathbb{A}), integration over the unipotent orbit space, and finiteness blocks for the resulting integrals) used to handle the automorphic form induced from cubic data. That package supplies the modularity of the residual mod-3 representation which begins the modularity-lifting argument.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, Β§1
  2. H. Jacquet, I. I. Piatetski-Shapiro and J. A. Shalika, Rankin–Selberg convolutions, American Journal of Mathematics 105 (1983), 367–464
  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_CubicInduction_WhittakerBlock.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_HaarQuotient
import Definitions.Def_LanglandsTunnell_CubicInduction_Structure
import Definitions.Def_NumberField_TateGlobalZeta
import Definitions.Def_M4aHerbrand_AdeleTopologyFacts

set_option autoImplicit false

noncomputable section

open MeasureTheory IsDedekindDomain NumberField NumberField.AdelicHaar LanglandsTunnell.CubicInduction Topology
open scoped ENNReal NNReal

namespace WhittakerBlock

def unipotentSubgroup3 : Subgroup (AdelicGL 3 (π“ž β„š) β„š) :=
  Subgroup.closure (Set.range fun t : AdeleRing (π“ž β„š) β„š Γ— AdeleRing (π“ž β„š) β„š Γ— AdeleRing (π“ž β„š) β„š =>
    upperUnipotent3 t.1 t.2.1 t.2.2)

def unipotentHaar3 :
    @Measure β†₯unipotentSubgroup3 (@Subtype.instMeasurableSpace _ _ (glBorel (Fin 3) (π“ž β„š) β„š)) :=
  letI : MeasurableSpace (AdeleRing (π“ž β„š) β„š) := adeleBorel (π“ž β„š) β„š
  letI : MeasurableSpace (AdelicGL 3 (π“ž β„š) β„š) := glBorel (Fin 3) (π“ž β„š) β„š
  Measure.map
    (fun t : AdeleRing (π“ž β„š) β„š Γ— AdeleRing (π“ž β„š) β„š Γ— AdeleRing (π“ž β„š) β„š =>
      (⟨upperUnipotent3 t.1 t.2.1 t.2.2, Subgroup.subset_closure ⟨t, rfl⟩⟩ : unipotentSubgroup3))
    ((adelicAddHaar (π“ž β„š) β„š).prod ((adelicAddHaar (π“ž β„š) β„š).prod (adelicAddHaar (π“ž β„š) β„š)))

def quotientMeasure :
    @Measure (MulAction.orbitRel.Quotient (unipotentSubgroup3) (AdelicGL 3 (π“ž β„š) β„š))
      (@Quotient.instMeasurableSpace _ _ (glBorel (Fin 3) (π“ž β„š) β„š)) :=
  letI : MeasurableSpace (AdelicGL 3 (π“ž β„š) β„š) := glBorel (Fin 3) (π“ž β„š) β„š
  HaarQuotient.measure (adelicGLHaar (Fin 3) (π“ž β„š) β„š) unipotentSubgroup3 unipotentHaar3

def zerothShell (S : Finset (HeightOneSpectrum (π“ž β„š))) :
    Set (MulAction.orbitRel.Quotient (unipotentSubgroup3) (AdelicGL 3 (π“ž β„š) β„š)) :=
  {q | βˆ€ p : HeightOneSpectrum (π“ž β„š), p βˆ‰ S β†’
    βˆƒ (x y z : p.adicCompletion β„š) (k : GL (Fin 3) (p.adicCompletion β„š)),
      k ∈ localMaximalCompact3 (π“ž β„š) β„š p ∧ componentAt3 (π“ž β„š) β„š p q.out = upperUnipotent3 x y z * k}

def block (pins : AutomorphicForm.CarrierPins β„š) (ψ : AddChar (AdeleRing (π“ž β„š) β„š) β„‚)
    (f : AdelicGL 3 (π“ž β„š) β„š β†’ β„‚) (Ξ¦ : (Fin 3 β†’ AdeleRing (π“ž β„š) β„š) β†’ β„‚) (Οƒ : ℝ)
    (S : Finset (HeightOneSpectrum (π“ž β„š))) : ℝβ‰₯0∞ :=
  letI : MeasurableSpace (AdelicGL 3 (π“ž β„š) β„š) := glBorel (Fin 3) (π“ž β„š) β„š
  ∫⁻ q in zerothShell S,
    ((β€–whittaker3 pins ψ f q.outβ€–β‚Š : ℝβ‰₯0∞) ^ 2 *
      (β€–Ξ¦ fun j : Fin 3 => (q.out : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 2 jβ€–β‚Š : ℝβ‰₯0∞) *
      ENNReal.ofReal (NumberField.TateGlobal.ideleNorm β„š (Matrix.GeneralLinearGroup.det q.out) ^ Οƒ))
    βˆ‚quotientMeasure

instance sigmaCompactSpace_adelicGL3 : SigmaCompactSpace (AdelicGL 3 (π“ž β„š) β„š) := by
  haveI : SigmaCompactSpace (Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) :=
    inferInstanceAs (SigmaCompactSpace (Fin 3 β†’ Fin 3 β†’ AdeleRing (π“ž β„š) β„š))
  haveI : SigmaCompactSpace (Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š))ᡐᡒᡖ :=
    MulOpposite.opHomeomorph.symm.isClosedEmbedding.sigmaCompactSpace
  exact Units.isClosedEmbedding_embedProduct.sigmaCompactSpace

section Heisenberg

variable {A : Type*} [CommRing A]

private theorem upperUnipotent3_mul (x y z x' y' z' : A) :
    upperUnipotent3 x y z * upperUnipotent3 x' y' z' = upperUnipotent3 (x + x') (y + y') (z + z' + x * y') := by
  ext i j
  fin_cases i <;> fin_cases j <;> simp [upperUnipotent3, Units.val_mul, Matrix.mul_apply, Fin.sum_univ_three]
  all_goals ring

private theorem upperUnipotent3_inv (x y z : A) :
    (upperUnipotent3 x y z)⁻¹ = upperUnipotent3 (-x) (-y) (x * y - z) := by
  rw [inv_eq_iff_mul_eq_one, upperUnipotent3_mul, show x + -x = 0 by ring, show y + -y = 0 by ring,
    show z + (x * y - z) + x * -y = 0 by ring, upperUnipotent3_zero]

end Heisenberg

theorem mem_unipotentSubgroup3_iff (g : AdelicGL 3 (π“ž β„š) β„š) :
    g ∈ unipotentSubgroup3 ↔ βˆƒ x y z : AdeleRing (π“ž β„š) β„š, g = upperUnipotent3 x y z := by
  refine ⟨fun hg => ?_, fun ⟨x, y, z, h⟩ => h β–Έ Subgroup.subset_closure ⟨(x, y, z), rfl⟩⟩
  unfold unipotentSubgroup3 at hg
  induction hg using Subgroup.closure_induction with
  | mem _ h => obtain ⟨t, rfl⟩ := h; exact ⟨t.1, t.2.1, t.2.2, rfl⟩
  | one => exact ⟨0, 0, 0, upperUnipotent3_zero.symm⟩
  | mul _ _ _ _ h h' =>
    obtain ⟨x, y, z, rfl⟩ := h
    obtain ⟨x', y', z', rfl⟩ := h'
    exact ⟨_, _, _, upperUnipotent3_mul x y z x' y' z'⟩
  | inv _ _ h =>
    obtain ⟨x, y, z, rfl⟩ := h
    exact ⟨_, _, _, upperUnipotent3_inv x y z⟩

theorem coe_unipotentSubgroup3_eq :
    ((unipotentSubgroup3 : Subgroup (AdelicGL 3 (π“ž β„š) β„š)) : Set (AdelicGL 3 (π“ž β„š) β„š)) =
      {g : AdelicGL 3 (π“ž β„š) β„š |
        (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 0 0 = 1 ∧
        (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 1 1 = 1 ∧
        (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 2 2 = 1 ∧
        (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 1 0 = 0 ∧
        (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 2 0 = 0 ∧
        (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 2 1 = 0} := by
  ext g
  simp only [SetLike.mem_coe, Set.mem_setOf_eq, mem_unipotentSubgroup3_iff]
  constructor
  · rintro ⟨x, y, z, rfl⟩
    simp
  · rintro ⟨h00, h11, h22, h10, h20, h21⟩
    refine ⟨(g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 0 1, (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 1 2,
      (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 0 2, ?_⟩
    refine Matrix.GeneralLinearGroup.ext fun i j => ?_
    rw [upperUnipotent3_coe]
    fin_cases i <;> fin_cases j <;> simp [h00, h11, h22, h10, h20, h21]

theorem isClosed_unipotentSubgroup3 :
    IsClosed ((unipotentSubgroup3 : Subgroup (AdelicGL 3 (π“ž β„š) β„š)) : Set (AdelicGL 3 (π“ž β„š) β„š)) := by
  rw [coe_unipotentSubgroup3_eq]
  have hc : βˆ€ i j : Fin 3,
      Continuous fun g : AdelicGL 3 (π“ž β„š) β„š => (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) i j :=
    fun i j => Units.continuous_val.matrix_elem i j
  have hz : βˆ€ (i j : Fin 3) (c : AdeleRing (π“ž β„š) β„š),
      IsClosed {g : AdelicGL 3 (π“ž β„š) β„š | (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) i j = c} :=
    fun i j c => isClosed_singleton.preimage (hc i j)
  simp only [Set.setOf_and]
  exact (hz 0 0 1).inter ((hz 1 1 1).inter ((hz 2 2 1).inter ((hz 1 0 0).inter ((hz 2 0 0).inter (hz 2 1 0)))))

end WhittakerBlock

end

Statements phrased using this module (16)