Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LanglandsTunnell_CubicInduction_ArchSmooth3.lean

definition module

Archimedean smoothness of functions on adelic over

Let \mathbb{A} denote the adele ring of \mathbb{Q}, realised as the product of the infinite adele ring and the finite adele ring, and let GL_3(\mathbb{A}) be the adelic general linear group AdelicGL 3 (π“ž β„š) β„š. Three declarations set up a real parametrisation of the archimedean directions in this group. First, for an array e \colon \mathrm{Fin}\,3 \to \mathrm{Fin}\,3 \to \mathbb{R} of real numbers, archRealMat3 e is the 3 \times 3 matrix over \mathbb{A} whose archimedean part is the matrix with entries the infinite adeles StandardKernel.ofReal (e i j) (the infinite adele whose coordinate at each infinite place of \mathbb{Q} is e\,i\,j) and whose finite part is the identity matrix; this is the image of that archimedean matrix under the multiplicative inclusion archMatrixInclN. Secondly, archRealLift3 e is the element of GL_3(\mathbb{A}) with underlying matrix archRealMat3 e whenever that matrix is a unit in the matrix ring, and the identity element of GL_3(\mathbb{A}) otherwise; the second branch is a default value, the case of interest being arrays of non-zero determinant, for which the adelic matrix is invertible because its archimedean component is invertible and its finite component is the identity. Thirdly, IsArchSmooth3 is a predicate on functions \varphi \colon GL_3(\mathbb{A}) \to \mathbb{C}: it holds when for every g \in GL_3(\mathbb{A}) the function of nine real variables e \longmapsto \varphi\bigl(g \cdot \mathrm{archRealLift3}(e)\bigr) is of class C^\infty over \mathbb{R}, in the sense of ContDiffOn with smoothness order \top, on the set \{e \mid \det(e) \neq 0\} of real arrays with non-vanishing determinant. Thus archimedean smoothness is expressed as smoothness of all right translates along this explicit real chart, rather than through a manifold structure on the adelic group.

Relation to Mathlib

Mathlib supplies the adele ring, the general linear group of matrices and the predicate ContDiffOn used here; the archimedean-smoothness condition for functions on an adelic group, and the real parametrisation through which it is phrased, are the project's own.

Where it is used

These definitions belong to the GL_3 vocabulary used in the cubic-induction (Langlands–Tunnell) part of the argument, where automorphic forms on GL_3 over \mathbb{Q} are required to be smooth in the archimedean variables; that input is what makes the odd irreducible two-dimensional mod 3 representations modular, the starting point of the modularity-lifting argument.

References

  1. R. P. Langlands, Base Change for GL(2), Annals of Mathematics Studies 96, Princeton University Press, 1980
  2. 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_ArchSmooth3.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_LanglandsTunnell_CubicInduction_Carrier
import Definitions.Def_AutomorphicForm_SmoothingKernel
import Mathlib.Analysis.Calculus.ContDiff.Defs β†—

set_option autoImplicit false

noncomputable section

open IsDedekindDomain NumberField LanglandsTunnell.CubicInduction

namespace WhittakerBlock

def archRealMat3 (e : Fin 3 β†’ Fin 3 β†’ ℝ) : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š) :=
  AutomorphicForm.archMatrixInclN (Fin 3) β„š (Matrix.of fun i j => AutomorphicForm.StandardKernel.ofReal (e i j))

open scoped Classical in

def archRealLift3 (e : Fin 3 β†’ Fin 3 β†’ ℝ) : AdelicGL 3 (π“ž β„š) β„š :=
  if h : IsUnit (archRealMat3 e) then h.unit else 1

def IsArchSmooth3 (Ο† : AdelicGL 3 (π“ž β„š) β„š β†’ β„‚) : Prop :=
  βˆ€ g : AdelicGL 3 (π“ž β„š) β„š,
    ContDiffOn ℝ (⊀ : β„•βˆž) (fun e : Fin 3 β†’ Fin 3 β†’ ℝ => Ο† (g * archRealLift3 e)) {e | (Matrix.of e).det β‰  0}

end WhittakerBlock

end

Statements phrased using this module (10)