Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LanglandsTunnell_CubicInduction_ArchSmoothSpace3.lean

definition module

Archimedean-smooth functions on adelic and their derivations

The ambient object is the space of complex-valued functions on AdelicGL 3 (π“ž β„š) β„š, the general linear group of degree 3 over the adele ring of \mathbb{Q}. A real entry array e \colon Fin 3 β†’ Fin 3 β†’ ℝ is placed into this group by archRealMat3, which sends e entrywise into the infinite adeles (through the inverses of the real-completion isomorphisms at the infinite places) and takes the identity matrix at the finite part; archRealLift3 e is the corresponding unit of the adelic matrix ring when that matrix is invertible, and 1 otherwise. The predicate IsArchSmooth3 Ο† says that for every g the map e \mapsto Ο†(g \cdot archRealLift3 e) is C^\infty on the locus \{e : \det e \neq 0\}, and archDeriv i j Ο† g is the derivative at s = 0 of s \mapsto Ο†(g \cdot archRealLift3(1 + s E_{ij})).

Two objects are defined. smoothFunctions3 is the \mathbb{C}-submodule of functions satisfying IsArchSmooth3, membership in which is by definition the predicate (mem_smoothFunctions3); closure under zero, sums and scalar multiples comes from the corresponding properties of ContDiffOn. archDerivβ‚— i j is the \mathbb{C}-linear endomorphism of this submodule given by Ο† \mapsto archDeriv i j Ο†, with coe_archDerivβ‚—_apply identifying its underlying function.

The accompanying results are: archRealLift3_mul, stating that for arrays e, e' of nonzero determinant the lifts multiply, \mathrm{lift}(e)\,\mathrm{lift}(e') = \mathrm{lift}(ee'); archDeriv_eq_fderiv, which for arch-smooth Ο† and \det e \neq 0 identifies archDeriv i j Ο† (g Β· archRealLift3 e) with the FrΓ©chet derivative at e of e' \mapsto Ο†(g \cdot \mathrm{lift}(e')) in the direction whose (a,b) entry is e_{ai} for b = j and 0 otherwise, that is the array of e E_{ij}; and isArchSmooth3_archDeriv, the resulting stability of arch-smoothness under archDeriv i j. Private auxiliaries record that the nonvanishing-determinant locus is open, that 1 + sE_{ij} lies in it for small s and equals 1 + s\,E_{ij} as a sum, that e \mapsto eE_{ij} is smooth, the differentiability of the one-parameter lines s \mapsto F(e + sv), and a ring homomorphism realAdeleHom from \mathbb{R} to the infinite adeles of \mathbb{Q} through which the placement of real matrices is multiplicative.

Relation to Mathlib

Mathlib has no notion of smooth vectors or of a Lie-algebra action on functions on an adelic group; the placement archRealLift3, the smoothness predicate IsArchSmooth3 and the operators archDeriv are the project's own, expressed through Mathlib's ContDiffOn, deriv and fderiv on the finite-dimensional real space Fin 3 β†’ Fin 3 β†’ ℝ, and the space of smooth functions is a plain Submodule β„‚ of the function space.

Where it is used

The operators archDeriv are the archimedean differentiations out of which the three Casimir-type operators casimir1, casimir2, casimir3 and the centre-finiteness condition IsCentreFinite on functions on adelic GL_3 are built; the submodule and the linear operators defined here make that action available on a fixed space of arch-smooth functions. This vocabulary belongs to the cubic-induction treatment of the Langlands–Tunnell theorem, which supplies the modularity of the residual mod 3 representation used in the Wiles 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
  3. D. Bump, Automorphic Forms and Representations, Cambridge Studies in Advanced Mathematics 55, Cambridge University Press, 1997

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

Imports

Imported by

Declarations

Source

import Definitions.Def_LanglandsTunnell_CubicInduction_ArchCentre3

set_option autoImplicit false

noncomputable section

open IsDedekindDomain NumberField AutomorphicForm

namespace LanglandsTunnell.CubicInduction.WhittakerBlock

private def invertibleEntries : Set (Fin 3 β†’ Fin 3 β†’ ℝ) := {e | (Matrix.of e).det β‰  0}

private theorem isOpen_invertibleEntries : IsOpen invertibleEntries :=
  isOpen_ne.preimage (Continuous.matrix_det (continuous_matrix fun a b =>
    (continuous_apply b).comp (continuous_apply a)))

private def unipotentEntries (i j : Fin 3) (s : ℝ) : Fin 3 β†’ Fin 3 β†’ ℝ :=
  fun a b => (if a = b then (1 : ℝ) else 0) + if a = i ∧ b = j then s else 0

private def oneEntries : Fin 3 β†’ Fin 3 β†’ ℝ := fun a b => if a = b then (1 : ℝ) else 0

private def elementaryEntries (i j : Fin 3) : Fin 3 β†’ Fin 3 β†’ ℝ := fun a b => if a = i ∧ b = j then (1 : ℝ) else 0

private theorem archDeriv_eq_deriv (i j : Fin 3) (Ο† : AdelicGL 3 (π“ž β„š) β„š β†’ β„‚) (g : AdelicGL 3 (π“ž β„š) β„š) :
    archDeriv i j Ο† g = deriv (fun s : ℝ => Ο† (g * WhittakerBlock.archRealLift3 (unipotentEntries i j s))) 0 :=
  rfl

private theorem unipotentEntries_eq (i j : Fin 3) (s : ℝ) :
    unipotentEntries i j s = oneEntries + s β€’ elementaryEntries i j := by
  funext a b
  simp only [unipotentEntries, oneEntries, elementaryEntries, Pi.add_apply, Pi.smul_apply, smul_eq_mul, mul_ite,
    mul_one, mul_zero]

private theorem of_oneEntries : Matrix.of oneEntries = 1 := by
  ext a b
  simp only [oneEntries, Matrix.of_apply, Matrix.one_apply]

private theorem oneEntries_mem : oneEntries ∈ invertibleEntries := by
  show (Matrix.of oneEntries).det β‰  0
  rw [of_oneEntries, Matrix.det_one]
  exact one_ne_zero

private theorem eventually_unipotentEntries_mem (i j : Fin 3) :
    βˆ€αΆ  s : ℝ in nhds 0, unipotentEntries i j s ∈ invertibleEntries := by
  have hc : Continuous fun s : ℝ => unipotentEntries i j s := by
    refine continuous_pi fun a => continuous_pi fun b => ?_
    show Continuous fun s : ℝ => (if a = b then (1 : ℝ) else 0) + if a = i ∧ b = j then s else 0
    refine continuous_const.add ?_
    by_cases h : a = i ∧ b = j
    Β· simp only [h]
      exact continuous_id
    Β· simp only [h, if_false]
      exact continuous_const
  have h0 : unipotentEntries i j 0 ∈ invertibleEntries := by
    rw [unipotentEntries_eq, zero_smul, add_zero]
    exact oneEntries_mem
  exact hc.continuousAt.eventually_mem (isOpen_invertibleEntries.mem_nhds h0)

private theorem mul_unipotentEntries_eq (i j : Fin 3) (e : Fin 3 β†’ Fin 3 β†’ ℝ) (s : ℝ) :
    (fun a b => (Matrix.of e * Matrix.of (unipotentEntries i j s)) a b) =
      e + s β€’ fun a b => if b = j then e a i else 0 := by
  funext a b
  by_cases hb : b = j
  Β· subst hb
    simp [Matrix.mul_apply, unipotentEntries, mul_add, Finset.sum_add_distrib, mul_comm]
  Β· simp [Matrix.mul_apply, unipotentEntries, hb]

private theorem contDiff_direction (i j : Fin 3) :
    ContDiff ℝ (⊀ : β„•βˆž) fun e : Fin 3 β†’ Fin 3 β†’ ℝ => (fun a b => if b = j then e a i else 0 : Fin 3 β†’ Fin 3 β†’ ℝ) := by
  refine contDiff_pi.2 fun a => contDiff_pi.2 fun b => ?_
  by_cases hb : b = j
  Β· simp only [hb, if_true]
    exact contDiff_pi.1 (contDiff_pi.1 contDiff_id a) i
  Β· simp only [hb, if_false]
    exact contDiff_const

private theorem hasDerivAt_line {F : (Fin 3 β†’ Fin 3 β†’ ℝ) β†’ β„‚} (hF : ContDiffOn ℝ (⊀ : β„•βˆž) F invertibleEntries)
    {e : Fin 3 β†’ Fin 3 β†’ ℝ} (he : e ∈ invertibleEntries) (v : Fin 3 β†’ Fin 3 β†’ ℝ) :
    HasDerivAt (fun s : ℝ => F (e + s β€’ v)) (fderiv ℝ F e v) 0 := by
  have hd : DifferentiableAt ℝ F e :=
    ((contDiffOn_infty_iff_fderiv_of_isOpen isOpen_invertibleEntries).1 hF).1.differentiableAt
      (isOpen_invertibleEntries.mem_nhds he)
  have hl : HasDerivAt (fun s : ℝ => e + s β€’ v) ((1 : ℝ) β€’ v) 0 :=
    ((hasDerivAt_id (0 : ℝ)).smul_const v).const_add e
  rw [one_smul] at hl
  exact hd.hasFDerivAt.comp_hasDerivAt_of_eq (0 : ℝ) hl (by simp)

private theorem differentiableAt_unipotent {Ο† : AdelicGL 3 (π“ž β„š) β„š β†’ β„‚} (hΟ† : WhittakerBlock.IsArchSmooth3 Ο†)
    (i j : Fin 3) (g : AdelicGL 3 (π“ž β„š) β„š) :
    DifferentiableAt ℝ (fun s : ℝ => Ο† (g * WhittakerBlock.archRealLift3 (unipotentEntries i j s))) 0 := by
  simp only [unipotentEntries_eq]
  exact (hasDerivAt_line (hφ g) oneEntries_mem (elementaryEntries i j)).differentiableAt

private def realAdeleHom : ℝ β†’+* InfiniteAdeleRing β„š :=
  RingHom.pi fun v => (InfinitePlace.Completion.ringEquivRealOfIsReal (IsTotallyReal.isReal v)).symm.toRingHom

private theorem archRealMat3_eq (e : Fin 3 β†’ Fin 3 β†’ ℝ) :
    WhittakerBlock.archRealMat3 e = archMatrixInclN (Fin 3) β„š ((Matrix.of e).map realAdeleHom) :=
  rfl

private theorem archRealMat3_mul (e e' : Fin 3 β†’ Fin 3 β†’ ℝ) :
    WhittakerBlock.archRealMat3 (fun a b => (Matrix.of e * Matrix.of e') a b) =
      WhittakerBlock.archRealMat3 e * WhittakerBlock.archRealMat3 e' := by
  rw [archRealMat3_eq, archRealMat3_eq, archRealMat3_eq, ← archMatrixInclN_mul, ← Matrix.map_mul]
  rfl

private theorem isUnit_archRealMat3 {e : Fin 3 β†’ Fin 3 β†’ ℝ} (he : e ∈ invertibleEntries) :
    IsUnit (WhittakerBlock.archRealMat3 e) := by
  have hdet : IsUnit ((Matrix.of e).map realAdeleHom) := by
    rw [Matrix.isUnit_iff_isUnit_det, ← RingHom.mapMatrix_apply, ← RingHom.map_det]
    exact (isUnit_iff_ne_zero.2 he).map realAdeleHom
  rw [archRealMat3_eq]
  exact hdet.map (archMatrixInclHomN (Fin 3) β„š)

private theorem coe_archRealLift3 {e : Fin 3 β†’ Fin 3 β†’ ℝ} (he : e ∈ invertibleEntries) :
    (WhittakerBlock.archRealLift3 e : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) = WhittakerBlock.archRealMat3 e := by
  unfold WhittakerBlock.archRealLift3
  rw [dif_pos (isUnit_archRealMat3 he)]
  exact (isUnit_archRealMat3 he).unit_spec

private theorem mul_mem_invertibleEntries {e e' : Fin 3 β†’ Fin 3 β†’ ℝ} (he : e ∈ invertibleEntries)
    (he' : e' ∈ invertibleEntries) : (fun a b => (Matrix.of e * Matrix.of e') a b) ∈ invertibleEntries := by
  show (Matrix.of e * Matrix.of e').det β‰  0
  rw [Matrix.det_mul]
  exact mul_ne_zero he he'

theorem archRealLift3_mul {e e' : Fin 3 β†’ Fin 3 β†’ ℝ} (he : (Matrix.of e).det β‰  0) (he' : (Matrix.of e').det β‰  0) :
    WhittakerBlock.archRealLift3 e * WhittakerBlock.archRealLift3 e' =
      WhittakerBlock.archRealLift3 (fun a b => (Matrix.of e * Matrix.of e') a b) := by
  have hm : e ∈ invertibleEntries := he
  have hm' : e' ∈ invertibleEntries := he'
  apply Units.ext
  rw [Units.val_mul, coe_archRealLift3 hm, coe_archRealLift3 hm', coe_archRealLift3 (mul_mem_invertibleEntries hm hm')]
  exact (archRealMat3_mul e e').symm

theorem archDeriv_eq_fderiv {Ο† : AdelicGL 3 (π“ž β„š) β„š β†’ β„‚} (hΟ† : WhittakerBlock.IsArchSmooth3 Ο†) (i j : Fin 3)
    (g : AdelicGL 3 (π“ž β„š) β„š) {e : Fin 3 β†’ Fin 3 β†’ ℝ} (he : (Matrix.of e).det β‰  0) :
    archDeriv i j Ο† (g * WhittakerBlock.archRealLift3 e) =
      fderiv ℝ (fun e' => Ο† (g * WhittakerBlock.archRealLift3 e')) e (fun a b => if b = j then e a i else 0) := by
  have he' : e ∈ invertibleEntries := he
  have hev : (fun s : ℝ =>
        Ο† (g * WhittakerBlock.archRealLift3 e * WhittakerBlock.archRealLift3 (unipotentEntries i j s))) =αΆ [nhds 0]
      fun s : ℝ => Ο† (g * WhittakerBlock.archRealLift3 (e + s β€’ fun a b => if b = j then e a i else 0)) := by
    filter_upwards [eventually_unipotentEntries_mem i j] with s hs
    rw [mul_assoc, archRealLift3_mul he hs, mul_unipotentEntries_eq]
  rw [archDeriv_eq_deriv, hev.deriv_eq]
  exact (hasDerivAt_line (hφ g) he' _).deriv

theorem isArchSmooth3_archDeriv {Ο† : AdelicGL 3 (π“ž β„š) β„š β†’ β„‚} (hΟ† : WhittakerBlock.IsArchSmooth3 Ο†) (i j : Fin 3) :
    WhittakerBlock.IsArchSmooth3 (archDeriv i j Ο†) := by
  intro g
  have hF := (contDiffOn_infty_iff_fderiv_of_isOpen isOpen_invertibleEntries).1 (hφ g)
  refine (hF.2.clm_apply (contDiff_direction i j).contDiffOn).congr fun e he => ?_
  exact archDeriv_eq_fderiv hφ i j g he

def smoothFunctions3 : Submodule β„‚ (AdelicGL 3 (π“ž β„š) β„š β†’ β„‚) where
  carrier := {Ο† | WhittakerBlock.IsArchSmooth3 Ο†}
  zero_mem' := by
    intro g
    exact contDiffOn_const
  add_mem' := by
    intro Ο† ψ hΟ† hψ g
    exact (hΟ† g).add (hψ g)
  smul_mem' := by
    intro c φ hφ g
    exact (hφ g).const_smul c

theorem mem_smoothFunctions3 {Ο† : AdelicGL 3 (π“ž β„š) β„š β†’ β„‚} :
    Ο† ∈ smoothFunctions3 ↔ WhittakerBlock.IsArchSmooth3 Ο† :=
  Iff.rfl

def archDerivβ‚— (i j : Fin 3) : smoothFunctions3 β†’β‚—[β„‚] smoothFunctions3 where
  toFun Ο† := ⟨archDeriv i j Ο†, isArchSmooth3_archDeriv Ο†.2 i j⟩
  map_add' Ο† ψ := Subtype.ext <| funext fun g =>
    ((differentiableAt_unipotent Ο†.2 i j g).hasDerivAt.add (differentiableAt_unipotent ψ.2 i j g).hasDerivAt).deriv
  map_smul' c Ο† := Subtype.ext <| funext fun g =>
    ((differentiableAt_unipotent Ο†.2 i j g).hasDerivAt.const_smul c).deriv

@[simp]
theorem coe_archDerivβ‚—_apply (i j : Fin 3) (Ο† : smoothFunctions3) :
    ((archDerivβ‚— i j Ο† : smoothFunctions3) : AdelicGL 3 (π“ž β„š) β„š β†’ β„‚) = archDeriv i j Ο† :=
  rfl

end LanglandsTunnell.CubicInduction.WhittakerBlock

Statements phrased using this module (0)

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