Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AutomorphicForm_ArchLowestWeight.lean

definition module

Archimedean lowest-weight predicate at a real place

Throughout, F is a number field, w an infinite place of F together with a witness hw that w is real, and \varphi a complex-valued function on \mathrm{GL}_2 of the adele ring of F (the group AdelicGL2 (π“ž F) F). For z in the upper half-plane, iwasawaSectionGL z is the element of \mathrm{GL}_2(\mathbb{R}) with matrix \begin{pmatrix}\operatorname{Im} z&\operatorname{Re} z\\0&1\end{pmatrix}; it is transported entrywise into \mathrm{GL}_2 of the completion F_w along the inverse of the isomorphism F_w\cong\mathbb{R} attached to a real place, and then placed into the adelic group by adelicArchGLInclAt F w, which puts the given matrix in the component at w and the identity at all other places (archimedean and finite). Write D_g(z) for the resulting value \varphi\bigl(g\cdot\iota_w(\ldots)\bigr), the descent of \varphi at w through g.

The predicate AutomorphicForm.IsArchLowestWeightAt w hw Ο† asserts that there exists a complex number \sigma such that for every adelic g the function z\mapsto (\operatorname{Im} z)^{\sigma}\,D_g(z) is differentiable on the upper half-plane in the sense of MDifferentiable for the trivial complex model \mathcal{I}(\mathbb{C}) on source and target, the power being the complex power of the positive real number \operatorname{Im} z. Note the quantifier order: a single exponent \sigma must work uniformly in g. The accompanying lemmas record an unfolding statement; that the zero function satisfies the predicate (with \sigma=0); stability under multiplication of \varphi by a fixed complex constant; a variant in which a real exponent \sigma is given and the normalising factor is the real power (\operatorname{Im} z)^{\sigma} coerced to \mathbb{C}; and that the predicate IsArchHolomorphicAt w hw Ο†, which demands holomorphy of the (\operatorname{Im} z)^{-1}-normalised descents, implies it, being the case \sigma=-1.

Relation to Mathlib

Mathlib supplies the complex-manifold structure on the upper half-plane and the notion MDifferentiable, and the adele ring, completions at infinite places and the isomorphism F_w\cong\mathbb{R} at a real place; the predicate on adelic functions itself is the project's own.

Where it is used

The stronger predicate IsArchHolomorphicAt is one of the archimedean conditions imposed in the project's cuspidality notion viaCompactCuspNotion, alongside the weight-one character condition at each real place; IsArchLowestWeightAt is the corresponding weakened condition, allowing an arbitrary uniform exponent in place of the normalisation by (\operatorname{Im} z)^{-1}.

References

  1. S. Gelbart, Automorphic Forms on Adele Groups, Annals of Mathematics Studies 83, Princeton University Press, 1975
  2. 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_AutomorphicForm_ArchLowestWeight.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_AutomorphicForm_ViaCompactCuspNotion

set_option autoImplicit false

open NumberField NumberField.InfinitePlace NumberField.InfinitePlace.Completion
open scoped Manifold

noncomputable section

namespace AutomorphicForm

def IsArchLowestWeightAt {F : Type} [Field F] [NumberField F] (w : InfinitePlace F)
    (hw : w.IsReal) (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) : Prop :=
  βˆƒ Οƒ : β„‚, βˆ€ g : AdelicGL2 (π“ž F) F, MDifferentiable π“˜(β„‚) π“˜(β„‚) fun z : UpperHalfPlane =>
    (((z.im : ℝ) : β„‚) ^ Οƒ) * Ο† (g * adelicArchGLInclAt F w
      (Matrix.GeneralLinearGroup.map
        ((InfinitePlace.Completion.ringEquivRealOfIsReal hw).symm.toRingHom)
        (iwasawaSectionGL z)))

variable {F : Type} [Field F] [NumberField F]

theorem isArchLowestWeightAt_iff (w : InfinitePlace F) (hw : w.IsReal)
    (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) :
    IsArchLowestWeightAt w hw Ο† ↔
      βˆƒ Οƒ : β„‚, βˆ€ g : AdelicGL2 (π“ž F) F, MDifferentiable π“˜(β„‚) π“˜(β„‚) fun z : UpperHalfPlane =>
        (((z.im : ℝ) : β„‚) ^ Οƒ) * Ο† (g * adelicArchGLInclAt F w
          (Matrix.GeneralLinearGroup.map
            ((InfinitePlace.Completion.ringEquivRealOfIsReal hw).symm.toRingHom)
            (iwasawaSectionGL z))) :=
  Iff.rfl

theorem isArchLowestWeightAt_zero (w : InfinitePlace F) (hw : w.IsReal) :
    IsArchLowestWeightAt w hw (fun _ => 0) :=
  ⟨0, fun _ => by simpa using mdifferentiable_const⟩

theorem IsArchLowestWeightAt.const_mul {w : InfinitePlace F} {hw : w.IsReal}
    {Ο† : AdelicGL2 (π“ž F) F β†’ β„‚} (h : IsArchLowestWeightAt w hw Ο†) (a : β„‚) :
    IsArchLowestWeightAt w hw (fun g => a * Ο† g) := by
  obtain βŸ¨Οƒ, hΟƒβŸ© := h
  refine βŸ¨Οƒ, fun g => ?_⟩
  have := (hσ g).const_smul a
  simpa [Pi.smul_def, smul_eq_mul, mul_left_comm] using this

theorem isArchLowestWeightAt_of_rpow {w : InfinitePlace F} {hw : w.IsReal}
    {Ο† : AdelicGL2 (π“ž F) F β†’ β„‚} (Οƒ : ℝ)
    (h : βˆ€ g : AdelicGL2 (π“ž F) F, MDifferentiable π“˜(β„‚) π“˜(β„‚) fun z : UpperHalfPlane =>
      (((z.im : ℝ) ^ Οƒ : ℝ) : β„‚) * Ο† (g * adelicArchGLInclAt F w
        (Matrix.GeneralLinearGroup.map
          ((InfinitePlace.Completion.ringEquivRealOfIsReal hw).symm.toRingHom)
          (iwasawaSectionGL z)))) :
    IsArchLowestWeightAt w hw Ο† := by
  refine ⟨(Οƒ : β„‚), fun g => ?_⟩
  have hfun : (fun z : UpperHalfPlane =>
      (((z.im : ℝ) : β„‚) ^ (Οƒ : β„‚)) * Ο† (g * adelicArchGLInclAt F w
        (Matrix.GeneralLinearGroup.map
          ((InfinitePlace.Completion.ringEquivRealOfIsReal hw).symm.toRingHom)
          (iwasawaSectionGL z)))) =
      (fun z : UpperHalfPlane =>
      (((z.im : ℝ) ^ Οƒ : ℝ) : β„‚) * Ο† (g * adelicArchGLInclAt F w
        (Matrix.GeneralLinearGroup.map
          ((InfinitePlace.Completion.ringEquivRealOfIsReal hw).symm.toRingHom)
          (iwasawaSectionGL z)))) := by
    funext z
    rw [Complex.ofReal_cpow (le_of_lt z.im_pos)]
  rw [hfun]
  exact h g

theorem IsArchHolomorphicAt.isArchLowestWeightAt {w : InfinitePlace F} {hw : w.IsReal}
    {Ο† : AdelicGL2 (π“ž F) F β†’ β„‚} (h : IsArchHolomorphicAt w hw Ο†) :
    IsArchLowestWeightAt w hw Ο† := by
  refine ⟨-1, fun g => ?_⟩
  have hfun : (fun z : UpperHalfPlane =>
      (((z.im : ℝ) : β„‚) ^ (-1 : β„‚)) * Ο† (g * adelicArchGLInclAt F w
        (Matrix.GeneralLinearGroup.map
          ((InfinitePlace.Completion.ringEquivRealOfIsReal hw).symm.toRingHom)
          (iwasawaSectionGL z)))) =
      (fun z : UpperHalfPlane =>
      ((z.im : ℝ) : β„‚)⁻¹ * Ο† (g * adelicArchGLInclAt F w
        (Matrix.GeneralLinearGroup.map
          ((InfinitePlace.Completion.ringEquivRealOfIsReal hw).symm.toRingHom)
          (iwasawaSectionGL z)))) := by
    funext z
    rw [Complex.cpow_neg_one]
  rw [hfun]
  exact h g

end AutomorphicForm

end

section Battery
open AutomorphicForm
#check @IsArchLowestWeightAt
#print axioms AutomorphicForm.isArchLowestWeightAt_zero
#print axioms AutomorphicForm.IsArchLowestWeightAt.const_mul
#print axioms AutomorphicForm.isArchLowestWeightAt_of_rpow
#print axioms AutomorphicForm.IsArchHolomorphicAt.isArchLowestWeightAt
end Battery

Statements phrased using this module (9)