Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AutomorphicForm_FnTwist.lean

definition module

Twisting adelic GL(2) functions by determinant characters

Throughout, F is a number field with ring of integers \mathcal{O}_F, and the ambient group is AdelicGL2 (π“ž F) F, i.e. \mathrm{GL}_2 of the adele ring of F. For a monoid homomorphism \eta : \mathbb{A}_F^\times \to \mathbb{C}^\times and a function \varphi on this group, fnTwist F Ξ· Ο† is the pointwise product g \mapsto \mathrm{chiDet}\,\eta\,(g)\cdot\varphi(g), where chiDet (π“ž F) F Ξ· is the complex-valued function on \mathrm{GL}_2(\mathbb{A}_F) attached to \eta through the determinant. The elementary lemmas record that the twist of the zero function is zero, that twisting by the trivial character is the identity operation, and that twists compose: twisting by \eta_2 and then by \eta_1 equals twisting by \eta_1\eta_2. Two transformation rules for chiDet are proved: for z \in \mathbb{A}_F^\times one has \det(\mathrm{centralScalar}\,z) = z^2 (the central element being the scalar matrix of size 2), whence \mathrm{chiDet}\,\eta\,(\mathrm{centralScalar}\,z\cdot g) = \eta(z)^2\,\mathrm{chiDet}\,\eta\,(g); and if \eta satisfies the predicate IsIdeleClassChar (a condition indexed by elements of F^\times, applied here to \det\gamma to give the value 1), then chiDet is invariant under left multiplication by the image of any \gamma \in \mathrm{GL}_2(F) under globalPoints. Correspondingly, twistedCentralChar F Z ΞΎ Ξ· is the character z \mapsto \xi(z)\,\eta(z)^2 of a subgroup Z \le \mathbb{A}_F^\times, and isLsXiFunction_fnTwist states that if \varphi satisfies IsLsXiFunction for (Z,\xi) β€” left invariance under global points together with the central transformation rule by \xi β€” then fnTwist F Ξ· Ο† satisfies it for (Z, \xi\cdot(\eta|_Z)^2). Finally, in any topological group, if two functions are each fixed by an open subgroup of a subgroup H under right translation (IsSmoothVector for RightTranslationFn), so is their pointwise product; applied to the subgroup of elements with trivial archimedean component, this gives that fnTwist F Ξ· Ο† is IsKfSmooth whenever both chiDet (π“ž F) F Ξ· and \varphi are. The trivial character satisfies IsIdeleClassChar, and twistedCentralChar by it returns \xi unchanged.

Relation to Mathlib

Mathlib has no vocabulary for adelic automorphic forms; the notions twisted here (chiDet, IsLsXiFunction, IsIdeleClassChar, IsKfSmooth) are the project's own, and smoothness is formulated via the project's IsSmoothVector, meaning that the stabiliser of the vector is open. The general product lemma for smooth vectors is stated for arbitrary Mathlib topological groups acting by right translation.

Where it is used

These lemmas provide the bookkeeping for changing an automorphic function on \mathrm{GL}_2(\mathbb{A}_F) by a character of the ideles composed with the determinant: invariance under the global points is unaffected, the central character is multiplied by the square of the restricted character, and finite-level smoothness is preserved. Such twists are used when normalising central characters on the automorphic side of the modularity arguments.

References

  1. D. Bump, Automorphic Forms and Representations, Cambridge Studies in Advanced Mathematics 55, Cambridge University Press, 1997
  2. S. Gelbart, Automorphic Forms on Adele Groups, Annals of Mathematics Studies 83, Princeton University Press, 1975

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_AutomorphicForm_SmoothAutomorphicFnAt

open IsDedekindDomain NumberField MeasureTheory Matrix
open AutomorphicForm FLT.SmoothVectors

noncomputable section

namespace AutomorphicForm

variable (F : Type) [Field F] [NumberField F]

def fnTwist (Ξ· : (AdeleRing (π“ž F) F)Λ£ β†’* β„‚Λ£) (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) :
    AdelicGL2 (π“ž F) F β†’ β„‚ :=
  fun g => chiDet (π“ž F) F Ξ· g * Ο† g

@[simp] theorem fnTwist_apply (Ξ· : (AdeleRing (π“ž F) F)Λ£ β†’* β„‚Λ£)
    (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) (g : AdelicGL2 (π“ž F) F) :
    fnTwist F Ξ· Ο† g = chiDet (π“ž F) F Ξ· g * Ο† g := rfl

@[simp] theorem fnTwist_zero (Ξ· : (AdeleRing (π“ž F) F)Λ£ β†’* β„‚Λ£) :
    fnTwist F Ξ· (fun _ => (0 : β„‚)) = fun _ => (0 : β„‚) := by
  ext g; simp [fnTwist]

theorem fnTwist_one (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) :
    fnTwist F (1 : (AdeleRing (π“ž F) F)Λ£ β†’* β„‚Λ£) Ο† = Ο† := by
  ext g; simp [fnTwist, chiDet]

theorem fnTwist_fnTwist (η₁ Ξ·β‚‚ : (AdeleRing (π“ž F) F)Λ£ β†’* β„‚Λ£)
    (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) :
    fnTwist F η₁ (fnTwist F Ξ·β‚‚ Ο†) = fnTwist F (η₁ * Ξ·β‚‚) Ο† := by
  ext g; simp only [fnTwist, chiDet, MonoidHom.mul_apply, Units.val_mul]; ring

theorem det_centralScalar (z : (AdeleRing (π“ž F) F)Λ£) :
    Matrix.GeneralLinearGroup.det (centralScalar (π“ž F) F z) = z ^ 2 := by
  rw [show centralScalar (π“ž F) F = Matrix.GeneralLinearGroup.scalar (Fin 2) from rfl,
    Matrix.GeneralLinearGroup.det_scalar, Fintype.card_fin]

theorem chiDet_centralScalar_mul (Ξ· : (AdeleRing (π“ž F) F)Λ£ β†’* β„‚Λ£)
    (z : (AdeleRing (π“ž F) F)Λ£) (g : AdelicGL2 (π“ž F) F) :
    chiDet (π“ž F) F Ξ· (centralScalar (π“ž F) F z * g) =
      ((Ξ· z : β„‚Λ£) : β„‚) ^ 2 * chiDet (π“ž F) F Ξ· g := by
  simp only [chiDet, map_mul, det_centralScalar F, map_pow, Units.val_mul, Units.val_pow_eq_pow_val]

def twistedCentralChar (Z : Subgroup (AdeleRing (π“ž F) F)Λ£) (ΞΎ : Z β†’* β„‚Λ£)
    (Ξ· : (AdeleRing (π“ž F) F)Λ£ β†’* β„‚Λ£) : Z β†’* β„‚Λ£ :=
  ΞΎ * (Ξ·.comp Z.subtype) ^ 2

theorem chiDet_globalPoints_mul (Ξ· : (AdeleRing (π“ž F) F)Λ£ β†’* β„‚Λ£)
    (hΞ·F : IsIdeleClassChar (π“ž F) F Ξ·) (Ξ³ : GL (Fin 2) F) (g : AdelicGL2 (π“ž F) F) :
    chiDet (π“ž F) F Ξ· (globalPoints (π“ž F) F Ξ³ * g) = chiDet (π“ž F) F Ξ· g := by
  unfold chiDet
  congr 1
  rw [map_mul, globalPoints, Matrix.GeneralLinearGroup.map_det, map_mul,
    hΞ·F (Matrix.GeneralLinearGroup.det Ξ³), one_mul]

theorem isLsXiFunction_fnTwist {Z : Subgroup (AdeleRing (π“ž F) F)Λ£} {ΞΎ : Z β†’* β„‚Λ£}
    (Ξ· : (AdeleRing (π“ž F) F)Λ£ β†’* β„‚Λ£) (hΞ·F : IsIdeleClassChar (π“ž F) F Ξ·)
    {Ο† : AdelicGL2 (π“ž F) F β†’ β„‚} (hΟ† : IsLsXiFunction (π“ž F) F Z ΞΎ Ο†) :
    IsLsXiFunction (π“ž F) F Z (twistedCentralChar F Z ΞΎ Ξ·) (fnTwist F Ξ· Ο†) := by
  refine ⟨fun γ g => ?_, fun z g => ?_⟩
  · simp only [fnTwist_apply, chiDet_globalPoints_mul F η hηF, hφ.left_invariant γ g]
  · simp only [fnTwist_apply, chiDet_centralScalar_mul F, hφ.central_transform z g,
      twistedCentralChar, MonoidHom.mul_apply, MonoidHom.comp_apply, Subgroup.coe_subtype,
      MonoidHom.pow_apply, Units.val_mul, Units.val_pow_eq_pow_val]
    ring

theorem isSmoothVector_rightTranslationFn_mul {G : Type*} [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] {M : Type*} [Mul M] {H : Subgroup G} {Ο† ψ : G β†’ M}
    (hφ : IsSmoothVector H (RightTranslationFn.mk (G := G) φ))
    (hψ : IsSmoothVector H (RightTranslationFn.mk (G := G) ψ)) :
    IsSmoothVector H (RightTranslationFn.mk (G := G) (fun g => Ο† g * ψ g)) := by
  rw [isSmoothVector_iff_isOpen_stabilizer]
  refine Subgroup.isOpen_mono ?_ (isOpen_coe_inf_stabilizer hΟ† hψ)
  intro k hk
  rw [Subgroup.mem_inf, MulAction.mem_stabilizer_iff, MulAction.mem_stabilizer_iff,
    Subgroup.smul_def, Subgroup.smul_def] at hk
  rw [MulAction.mem_stabilizer_iff, Subgroup.smul_def]
  refine RightTranslationFn.ext fun g => ?_
  have hΟ†k : Ο† (g * ↑k) = Ο† g := by
    have := congrFun (congrArg RightTranslationFn.toFun hk.1) g
    simp only [RightTranslationFn.toFun_smul] at this
    exact this
  have hψk : ψ (g * ↑k) = ψ g := by
    have := congrFun (congrArg RightTranslationFn.toFun hk.2) g
    simp only [RightTranslationFn.toFun_smul] at this
    exact this
  simp only [RightTranslationFn.toFun_smul]
  exact congrArgβ‚‚ (Β· * Β·) hΟ†k hψk

theorem isKfSmooth_fnTwist (Ξ· : (AdeleRing (π“ž F) F)Λ£ β†’* β„‚Λ£)
    (hΞ·Kf : IsKfSmooth F (chiDet (π“ž F) F Ξ·)) {Ο† : AdelicGL2 (π“ž F) F β†’ β„‚}
    (hφ : IsKfSmooth F φ) : IsKfSmooth F (fnTwist F η φ) :=
  isSmoothVector_rightTranslationFn_mul hηKf hφ

theorem twistedCentralChar_one (Z : Subgroup (AdeleRing (π“ž F) F)Λ£) (ΞΎ : Z β†’* β„‚Λ£) :
    twistedCentralChar F Z ΞΎ 1 = ΞΎ := by
  ext z; simp [twistedCentralChar]

theorem isIdeleClassChar_one : IsIdeleClassChar (π“ž F) F (1 : (AdeleRing (π“ž F) F)Λ£ β†’* β„‚Λ£) :=
  fun _ => rfl

end AutomorphicForm

end

Statements phrased using this module (34)