Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AutomorphicForm_RationalTorusUnipotentQuotient.lean

definition module

Rational diagonal torus times adelic unipotent: subgroup, quotient, measures

Throughout, K is a number field, \mathbb{A}_K its adele ring and \mathrm{GL}_2(\mathbb{A}_K) is AdelicGL2 (𝓞 K) K, equipped with the Borel \sigma-algebras attached to it and to \mathbb{A}_K in the project's adelic Haar module. Four group-theoretic objects are introduced. rationalDiagOne is the image in \mathrm{GL}_2(\mathbb{A}_K) of the homomorphism a \mapsto \mathrm{diag}(a,1) on K^\times followed by the map \mathrm{GL}_2(K) \to \mathrm{GL}_2(\mathbb{A}_K) induced by K \to \mathbb{A}_K. rationalTorus is the join of rationalCentre (the image of z \mapsto z\cdot 1_2 on K^\times, again pushed into \mathrm{GL}_2(\mathbb{A}_K)) with rationalDiagOne, i.e. the subgroup of diagonal matrices with entries in K^\times. rationalTorusUnipotent is the join of rationalTorus with adelicUnipotent, the image of x \mapsto \begin{pmatrix}1&x\\0&1\end{pmatrix} on \mathbb{A}_K. RationalTorusUnipotentQuotient is the orbit space of the left multiplication action of this subgroup on \mathrm{GL}_2(\mathbb{A}_K), taken as Mathlib's orbit-relation quotient rather than as a coset space.

Two measures are then defined. rationalTorusUnipotentHaar is the sum, over pairs (z,a) \in K^\times \times K^\times — a parametrisation of the diagonal matrices \mathrm{diag}(za,z) with entries in K^\times — of the pushforwards of unipotentHaar K under left translation n \mapsto (z\cdot 1_2)\,\mathrm{diag}(a,1)\,n inside the subgroup; here unipotentHaar K is the image under x \mapsto \begin{pmatrix}1&x\\0&1\end{pmatrix} of the additive adelic Haar measure rescaled by the inverse of the measure of adelicBox K. Thus the measure is discrete (counting) in the rational-torus direction and normalised Haar in the unipotent direction. rationalTorusUnipotentQuotientMeasure is the resulting measure on the orbit space, obtained by applying HaarQuotient.measure to the Haar measure adelicGLHaar (Fin 2) (𝓞 K) K on \mathrm{GL}_2(\mathbb{A}_K), the subgroup, and rationalTorusUnipotentHaar: the pushforward along the quotient map of the ambient Haar measure weighted by the density built from a compact exhaustion in HaarQuotient.density.

Relation to Mathlib

Mathlib supplies the adele ring, Haar measure on locally compact groups and the orbit-relation quotient used here, but none of these adelic subgroups of \mathrm{GL}_2(\mathbb{A}_K) nor the quotient measure; the latter is built from the project's own HaarQuotient.measure. The module is a sibling of the constructions for Z(K)N_2(\mathbb{A}_K) and for N_2(\mathbb{A}_K) alone, with the same conventions.

Where it is used

These are the intermediate objects of the Rankin–Selberg unfolding in the automorphic part of the argument: after unfolding to the rational Borel quotient and integrating over the unipotent radical one lands on T(K)N_2(\mathbb{A}_K)\backslash\mathrm{GL}_2(\mathbb{A}_K), from which the rank-one torus is unfolded down to Z(K)N_2(\mathbb{A}_K)\backslash\mathrm{GL}_2(\mathbb{A}_K).

References

  1. D. Bump, Automorphic Forms and Representations, Cambridge Studies in Advanced Mathematics 55, Cambridge University Press, 1997
  2. A. Weil, Basic Number Theory, Grundlehren der mathematischen Wissenschaften 144, Springer, 1967

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_AutomorphicForm_RationalCentreUnipotentQuotient
import Definitions.Def_NumberField_AdelicLevel

set_option autoImplicit false

open MeasureTheory NumberField NumberField.AdelicHaar NumberField.AdelicBox NumberField.AdelicLevel

noncomputable section

namespace AutomorphicForm

attribute [local instance] NumberField.AdelicHaar.glBorel NumberField.AdelicHaar.borelSpace_glBorel
  NumberField.AdelicHaar.adeleBorel NumberField.AdelicHaar.borelSpace_adeleBorel

variable (K : Type*) [Field K] [NumberField K]

abbrev rationalDiagOne : Subgroup (AdelicGL2 (𝓞 K) K) :=
  ((globalPoints (𝓞 K) K).comp (diagOne (A := K))).range

abbrev rationalTorus : Subgroup (AdelicGL2 (𝓞 K) K) :=
  rationalCentre K ⊔ rationalDiagOne K

abbrev rationalTorusUnipotent : Subgroup (AdelicGL2 (𝓞 K) K) :=
  rationalTorus K ⊔ adelicUnipotent K

abbrev RationalTorusUnipotentQuotient : Type _ :=
  MulAction.orbitRel.Quotient (rationalTorusUnipotent K) (AdelicGL2 (𝓞 K) K)

def rationalTorusUnipotentHaar : Measure (rationalTorusUnipotent K) :=
  Measure.sum fun za : Kˣ × Kˣ =>
    Measure.map
      (fun n : adelicUnipotent K =>
        (⟨globalPoints (𝓞 K) K (Units.map (Matrix.scalar (Fin 2) : K →+* Matrix (Fin 2) (Fin 2) K).toMonoidHom za.1)
            * globalPoints (𝓞 K) K (diagOne za.2) * (n : AdelicGL2 (𝓞 K) K),
          Subgroup.mul_mem_sup
            (Subgroup.mul_mem_sup ⟨za.1, rfl⟩ ⟨za.2, rfl⟩) n.2⟩ : rationalTorusUnipotent K))
      (unipotentHaar K)

def rationalTorusUnipotentQuotientMeasure : Measure (RationalTorusUnipotentQuotient K) :=
  HaarQuotient.measure (adelicGLHaar (Fin 2) (𝓞 K) K) (rationalTorusUnipotent K)
    (rationalTorusUnipotentHaar K)

end AutomorphicForm

end

Statements phrased using this module (37)