Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AutomorphicForm_RationalCentreUnipotentQuotient.lean

definition module

Rational centre 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; all measures are taken for the Borel \sigma-algebras coming from the topologies on \mathbb{A}_K and on \mathrm{GL}_2(\mathbb{A}_K). Four objects are introduced. First, rationalCentre K is the subgroup of \mathrm{GL}_2(\mathbb{A}_K) obtained as the range of the homomorphism K^\times \to \mathrm{GL}_2(\mathbb{A}_K) sending a to the scalar matrix a\cdot 1 in \mathrm{GL}_2(K) and then applying globalPoints, the entrywise map induced by K \to \mathbb{A}_K; so it consists of the adelic scalar matrices with rational entry. Second, rationalCentreUnipotent K is the join H = Z(K) \sqcup N(\mathbb{A}_K) of this subgroup with adelicUnipotent K, the range of x \mapsto \begin{pmatrix}1&x\\0&1\end{pmatrix} on \mathbb{A}_K. Third, RationalCentreUnipotentQuotient K is the quotient of \mathrm{GL}_2(\mathbb{A}_K) by the orbit relation of the left translation action of H, i.e. the space of right cosets H\backslash\mathrm{GL}_2(\mathbb{A}_K).

Fourth, the measures. rationalCentreUnipotentHaar K is the measure on H given by the sum, over all a \in K^\times, of the pushforward of unipotentHaar K along n \mapsto (a\cdot 1)\,n, the latter element being recorded as a member of H via membership in the join; here unipotentHaar K is the image under x \mapsto \begin{pmatrix}1&x\\0&1\end{pmatrix} of the additive Haar measure of \mathbb{A}_K rescaled so that the adelic box has mass one. Finally, rationalCentreUnipotentQuotientMeasure K is HaarQuotient.measure applied to the Haar measure adelicGLHaar (Fin 2) (𝓞 K) K of \mathrm{GL}_2(\mathbb{A}_K), the subgroup H and the measure just defined: the pushforward along the coset projection of the Haar measure weighted by the density function attached to H and to that measure.

Relation to Mathlib

The quotient type is Mathlib's MulAction.orbitRel.Quotient and the measures are assembled with Mathlib's Measure.sum and Measure.map; the adelic groups, their Haar measures and the weighted-density quotient measure HaarQuotient.measure are the project's own constructions.

Where it is used

These definitions provide the homogeneous space and normalised measures for the subgroup generated by the rational central scalars and the adelic unipotent radical, the setting in which constant terms and Rankin–Selberg type integrals on \mathrm{GL}_2(\mathbb{A}_K) are formulated in the automorphic-forms part of the development; they refine the purely unipotent quotient and measure on which they are built.

References

  1. H. Jacquet, Automorphic Forms on GL(2), Part II, Lecture Notes in Mathematics 278, Springer, 1972
  2. D. Bump, Automorphic Forms and Representations, Cambridge Studies in Advanced Mathematics 55, Cambridge University Press, 1997, §3.8
  3. 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_RationalCentreUnipotentQuotient.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_AutomorphicForm_UnipotentQuotient

open MeasureTheory NumberField NumberField.AdelicHaar NumberField.AdelicBox

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 rationalCentre : Subgroup (AdelicGL2 (𝓞 K) K) :=
  ((globalPoints (𝓞 K) K).comp
    (Units.map (Matrix.scalar (Fin 2) : K →+* Matrix (Fin 2) (Fin 2) K).toMonoidHom)).range

abbrev rationalCentreUnipotent : Subgroup (AdelicGL2 (𝓞 K) K) :=
  rationalCentre K ⊔ adelicUnipotent K

abbrev RationalCentreUnipotentQuotient : Type _ :=
  MulAction.orbitRel.Quotient (rationalCentreUnipotent K) (AdelicGL2 (𝓞 K) K)

def rationalCentreUnipotentHaar : Measure (rationalCentreUnipotent K) :=
  Measure.sum fun a : Kˣ =>
    Measure.map
      (fun n : adelicUnipotent K =>
        (⟨globalPoints (𝓞 K) K (Units.map (Matrix.scalar (Fin 2) : K →+* Matrix (Fin 2) (Fin 2) K).toMonoidHom a)
            * (n : AdelicGL2 (𝓞 K) K),
          Subgroup.mul_mem_sup ⟨a, rfl⟩ n.2⟩ : rationalCentreUnipotent K))
      (unipotentHaar K)

def rationalCentreUnipotentQuotientMeasure : Measure (RationalCentreUnipotentQuotient K) :=
  HaarQuotient.measure (adelicGLHaar (Fin 2) (𝓞 K) K) (rationalCentreUnipotent K)
    (rationalCentreUnipotentHaar K)

end AutomorphicForm

end

Statements phrased using this module (12)