1. FormalConjecturesForMathlib
  2. NumberTheory
  3. AutomorphicForm
  4. BorelJacquet
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet.CenterAction public import FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet.LieDeriv public import FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet.Subgroups public import Mathlib.Analysis.SpecialFunctions.Pow.Real public import Mathlib.LinearAlgebra.FiniteDimensional.Defs public import Mathlib.RingTheory.Ideal.Quotient.Operations public import Mathlib.Topology.Algebra.OpenSubgroup public import Mathlib.Topology.LocallyConstant.Basic@[expose] public section

Automorphic forms in the sense of Borel-Jacquet

Borel-Jacquet means the definition of an automorphic form given by Armand Borel and Hervé Jacquet in their article in the Corvallis proceedings (the first reference below) — the standard adelic definition. It is formalised here for G = GL n / ℚ with maximal compact subgroup K = O n ℝ, in the shape Buzzard states it for GL₂.

Writing G(𝔸) = G(𝔸_f) × G(ℝ), where G(𝔸_f) = GL n 𝔸ᶠ[ℤ, ℚ] is the points of GL n in the finite adeles of ℚ, an automorphic form is a smooth f : G(𝔸) → ℂ such that

    (a) f (γ x) = f x for all γ ∈ G(ℚ), embedded diagonally;

    (b1) f (x u) = f x for all u in some compact open subgroup of G(𝔸_f);

    (b2) the ℂ-span of the right translates x ↦ f (x k), for k ∈ K, is finite-dimensional;

    (c) f is annihilated by an ideal of finite codimension of the centre of the universal enveloping algebra of the complexified Lie algebra of G(ℝ), acting by left invariant differential operators;

    (d) for each x ∈ G(𝔸_f), the function y ↦ f (x, y) on G(ℝ) is slowly increasing.

Smooth means continuous, locally constant in the finite variable and C^∞ in the archimedean one. The further condition (e) cutting out cusp forms, that the constant term along every unipotent radical vanishes, is not formalised here: it needs Haar integration over N(ℚ) \ N(𝔸).

Main declarations

All in the namespace Matrix.GeneralLinearGroup unless qualified otherwise:

    AutomorphicForm.IsKFinite and AutomorphicForm.IsZFinite: the finiteness conditions (b2) and (c), for an abstract group and module respectively.

    gnorm and IsSlowlyIncreasing: the norm ‖y‖ = max (|y|, |y⁻¹|) on GL n ℝ and condition (d), slow increase.

    IsSmoothAdelic and IsAutomorphicForm: smoothness on G(𝔸), and the definition itself.

    isAutomorphicForm_one: the constant function 1 is an automorphic form — a sanity check exercising every condition; condition (c) holds through constantsCharacter, the character by which the centre acts on constants.

    automorphicForms and rightTranslation: the automorphic forms as a ℂ-submodule of the functions on G(𝔸), with the right translation representation of G(𝔸_f) on it.

The remaining ingredients of the definition are developed in the BorelJacquet subdirectory:

    BorelJacquet.LieDeriv: the C^∞ functions on GL n ℝ (IsSmoothOnGL, smoothGL) and the action on them of 𝔤𝔩 n ℝ and its complexification (lieDeriv, lieDerivC).

    BorelJacquet.CenterAction: the enveloping algebra universalEnveloping, its centre centerUniversalEnveloping, their action (envelopingAction, centerAction) — the action of condition (c) — and the character constantsCharacter.

    BorelJacquet.Subgroups: the subgroups ratDiagonal (condition (a)), orthogonalSubgroup (condition (b2)) and integralAdelicSubgroup (the compact open subgroup witnessing condition (b1)).

Relation to the literature

Buzzard states (b2) through a finite-dimensional representation σ of K; for compact K that formulation is equivalent to the one used here, since the span of the translates is a continuous, hence semisimple, finite-dimensional representation of K. Conditions (b1) and (b2) together are the K-finiteness of Getz-Hahn's Definition 6.5 for K = K_∞ K^∞ with K^∞ ≤ G(𝔸_f) compact open.

Condition (d) follows Buzzard in letting the constants depend on the finite variable. Getz-Hahn's Definition 6.4 instead imposes one global bound |f g| ≤ c * H g ^ r for their adelic height H; for GL n that height factors as H (x, y) = H_f x * gnorm y, so the global bound implies (d). Only these implications are asserted; no equivalence with Getz-Hahn's full definition is claimed.

Implementation notes

The action of condition (c) is constructed, not assumed; see FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet.LieDeriv and FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet.CenterAction for the construction. The action lives on smoothGL n, not on all of G(𝔸) → ℂ — a differential operator has nothing to act on at a non-differentiable function — so condition (c) asks for one ideal annihilating every slice y ↦ f (x, y) at once, the finite variable being a spectator.

References:

    A. Borel and H. Jacquet, Automorphic forms and automorphic representations, in Automorphic Forms, Representations and L-functions (Corvallis), Proc. Sympos. Pure Math. 33, Part 1, Amer. Math. Soc. (1979), 189–207; §4.

    K. Buzzard, Automorphic forms for GL2 over Q, §1. https://www.ma.imperial.ac.uk/~buzzard/maths/research/notes/automorphic_forms_for_gl2_over_Q.pdf

    J. R. Getz and H. Hahn, An Introduction to Automorphic Representations, GTM 300, Springer (2024), §6.2 and §6.3; in the numbering of that text, Definitions 6.1 (moderate growth), 6.2 (Z(𝔤)-finiteness), 6.4 (adelic moderate growth) and 6.5 (adelic automorphic form). https://sites.duke.edu/jgetz/files/2022/04/Graduate_Text.pdf

namespace AutomorphicForm

The finiteness conditions (b2) and (c), abstractly

section KFinitevariable {G : Type*} [Group G] (K : Subgroup G) (k : Type*) [Field k] (f : G → k)

The k-span of the right translates of f by the subgroup K.

def rightTranslateSpan : Submodule k (G → k) := Submodule.span k (Set.range fun u : K => fun x => f (x * (u : G)))lemma self_mem_rightTranslateSpan : f ∈ rightTranslateSpan K k f := Submodule.subset_span ⟨1, funext fun x => G:Type u_1inst✝¹:Group GK:Subgroup Gk:Type u_2inst✝:Field kf:G → kx:G⊢ (fun u x ↦ f (x * ↑u)) 1 x = f x All goals completed! 🐙⟩

f is K-finite: the span of its right K-translates is finite-dimensional. This is condition (b2) in the definition of an automorphic form.

abbrev IsKFinite : Prop := FiniteDimensional k (rightTranslateSpan K k f)variable {K k f}

A function invariant under right translation by K is K-finite.

lemma isKFinite_of_rightInvariant (h : ∀ (x : G) (u : K), f (x * (u : G)) = f x) : IsKFinite K k f := FiniteDimensional.span_of_finite k <| (Set.finite_singleton f).subset <| Set.range_subset_iff.mpr fun u => funext fun x => h x u

If K is finite then every function is K-finite.

lemma isKFinite_of_finite [Finite K] : IsKFinite K k f := FiniteDimensional.span_of_finite k (Set.finite_range _)

K-finiteness is closed under addition: the translate span of f + g sits inside the sum of the translate spans.

protected lemma IsKFinite.add {f g : G → k} (hf : IsKFinite K k f) (hg : IsKFinite K k g) : IsKFinite K k (f + g) := Submodule.finiteDimensional_of_le (S₂ := rightTranslateSpan K k f ⊔ rightTranslateSpan K k g) <| Submodule.span_le.mpr <| Set.range_subset_iff.mpr fun u => add_mem (Submodule.mem_sup_left (Submodule.subset_span ⟨u, rfl⟩)) (Submodule.mem_sup_right (Submodule.subset_span ⟨u, rfl⟩))protected lemma IsKFinite.const_smul {f : G → k} (hf : IsKFinite K k f) (c : k) : IsKFinite K k (c • f) := Submodule.finiteDimensional_of_le (S₂ := rightTranslateSpan K k f) <| Submodule.span_le.mpr <| Set.range_subset_iff.mpr fun u => Submodule.smul_mem _ c (Submodule.subset_span ⟨u, rfl⟩)end KFinitesection ZFinitevariable (k : Type*) [Field k] (Z : Type*) [CommRing Z] [Algebra k Z] {M : Type*} [AddCommGroup M] [Module Z M]

m is Z-finite: it is annihilated by an ideal of Z of finite codimension over k. This is condition (c), with Z the centre of the universal enveloping algebra of the complexified Lie algebra of G(ℝ), i.e. Matrix.GeneralLinearGroup.centerUniversalEnveloping n.

This is Getz-Hahn's Definition 6.2, in the form they state for a vector of an arbitrary Z(𝔤)-module. They note it is equivalent to Z • m being finite-dimensional over k.

def IsZFinite (m : M) : Prop := ∃ I : Ideal Z, FiniteDimensional k (Z ⧸ I) ∧ ∀ z ∈ I, z • m = 0variable {k Z}lemma isZFinite_zero : IsZFinite k Z (0 : M) := ⟨⊤, inferInstance, fun z _ => smul_zero z⟩

Z-finiteness is closed under addition: the intersection of the two annihilating ideals works, since Z ⧸ (I ⊓ J) embeds in (Z ⧸ I) × (Z ⧸ J).

k:Type u_1inst✝⁴:Field kZ:Type u_2inst✝³:CommRing Zinst✝²:Algebra k ZM:Type u_3inst✝¹:AddCommGroup Minst✝:Module Z Mm₁:Mm₂:MI:Ideal ZhI:FiniteDimensional k (Z ⧸ I)hIann:∀ z ∈ I, z • m₁ = 0J:Ideal ZhJ:FiniteDimensional k (Z ⧸ J)hJann:∀ z ∈ J, z • m₂ = 0hker:((Submodule.mkQ I).prod (Submodule.mkQ J)).ker = I ⊓ J⊢ IsZFinite k Z (m₁ + m₂) refine ⟨I ⊓ J, FiniteDimensional.of_injective (((I ⊓ J).liftQ (I.mkQ.prod J.mkQ) hker.ge).restrictScalars k) ?_, fun z hz => k:Type u_1inst✝⁴:Field kZ:Type u_2inst✝³:CommRing Zinst✝²:Algebra k ZM:Type u_3inst✝¹:AddCommGroup Minst✝:Module Z Mm₁:Mm₂:MI:Ideal ZhI:FiniteDimensional k (Z ⧸ I)hIann:∀ z ∈ I, z • m₁ = 0J:Ideal ZhJ:FiniteDimensional k (Z ⧸ J)hJann:∀ z ∈ J, z • m₂ = 0hker:((Submodule.mkQ I).prod (Submodule.mkQ J)).ker = I ⊓ Jz:Zhz:z ∈ I ⊓ J⊢ z • (m₁ + m₂) = 0 All goals completed! 🐙⟩ All goals completed! 🐙

Z-finiteness is preserved by scalar multiplication: the same ideal works.

All goals completed! 🐙

An element on which Z acts through a k-algebra character is Z-finite: the kernel of the character is an ideal of finite codimension annihilating it.

All goals completed! 🐙⟩

A constant family with Z-finite value is Z-finite, with the same ideal.

protected lemma IsZFinite.pi_const {ι : Type*} {m₀ : M} (h : IsZFinite k Z m₀) : IsZFinite k Z (fun _ : ι => m₀) := h.imp fun _ => And.imp_right fun hann z hz => funext fun _ => hann z hz

Precomposition preserves Z-finiteness of a family, with the same ideal.

protected lemma IsZFinite.comp {ι' ι : Type*} {m : ι → M} (h : IsZFinite k Z m) (σ : ι' → ι) : IsZFinite k Z (m ∘ σ) := h.imp fun _ => And.imp_right fun hann z hz => funext fun x => congrFun (hann z hz) (σ x)end ZFiniteend AutomorphicFormnamespace Matrix.GeneralLinearGroupopen AutomorphicFormopen scoped IsDedekindDomain.FiniteAdeleRing NNRealvariable {n : Type*} [Fintype n]

Slow increase: condition (d)

The sup norm on the entries of a matrix: for n = 2 this is |(a b; c d)| = max {|a|, |b|, |c|, |d|}.

The supremum is taken in ℝ≥0 rather than ℝ so that it is also defined when n is empty, where it takes the value 0 — the right answer, since then Matrix n n ℝ is the zero ring.

noncomputable def entrySup (M : Matrix n n ℝ) : ℝ := ((Finset.univ.sup fun i => Finset.univ.sup fun j => ‖M i j‖₊ : ℝ≥0) : ℝ)lemma le_entrySup (M : Matrix n n ℝ) (i j : n) : |M i j| ≤ entrySup M := n:Type u_1inst✝:Fintype nM:Matrix n n ℝi:nj:n⊢ |M i j| ≤ entrySup M n:Type u_1inst✝:Fintype nM:Matrix n n ℝi:nj:nh:‖M i j‖₊ ≤ Finset.univ.sup fun i ↦ Finset.univ.sup fun j ↦ ‖M i j‖₊⊢ |M i j| ≤ entrySup M All goals completed! 🐙lemma entrySup_nonneg (M : Matrix n n ℝ) : 0 ≤ entrySup M := n:Type u_1inst✝:Fintype nM:Matrix n n ℝ⊢ 0 ≤ entrySup M n:Type u_1inst✝:Fintype nM:Matrix n n ℝ⊢ 0 ≤ ↑(Finset.univ.sup fun i ↦ Finset.univ.sup fun j ↦ ‖M i j‖₊); All goals completed! 🐙variable [DecidableEq n]

The norm ‖y‖ = max (|y|, |y⁻¹|) on GL n ℝ, with |·| the sup norm on matrix entries. This is the norm used to define slow increase.

For G = GL n this is exactly the archimedean factor of the norm Getz-Hahn use for a general reductive G: theirs is the sup of the entries of ι y, for ι : G → SL (2 * n) the embedding y ↦ (y, (y⁻¹)ᵗ), whose entries are those of y together with those of y⁻¹.

noncomputable def gnorm (y : GL n ℝ) : ℝ := max (entrySup (y : Matrix n n ℝ)) (entrySup ((y⁻¹ : GL n ℝ) : Matrix n n ℝ))lemma gnorm_nonneg (y : GL n ℝ) : 0 ≤ gnorm y := le_max_of_le_left (entrySup_nonneg _)All goals completed! 🐙

gnorm is uniformly bounded below: since y * y⁻¹ = 1, the entries of y and y⁻¹ cannot all be small. This makes the exponent in a slow-increase bound enlargeable, hence IsSlowlyIncreasing closed under addition.

n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq ny:GL n ℝhcard:1 ≤ ↑(Fintype.card n)i:nhy:∑ k, ↑y i k * ↑y⁻¹ k i = 1hk:∀ (k : n), |↑y i k * ↑y⁻¹ k i| ≤ y.gnorm * y.gnormhbound:1 ≤ ↑(Fintype.card n) * (y.gnorm * y.gnorm)⊢ 1 ≤ y.gnorm * ↑(Fintype.card n); All goals completed! 🐙lemma gnorm_pos [Nonempty n] (y : GL n ℝ) : 0 < gnorm y := ((inv_pos.mpr (n:Type u_1inst✝²:Fintype ninst✝¹:DecidableEq ninst✝:Nonempty ny:GL n ℝ⊢ 0 < ↑(Fintype.card n) All goals completed! 🐙)).trans_le (inv_card_le_gnorm y))

A function φ : GL n ℝ → ℂ is slowly increasing, or of moderate growth, if ‖φ y‖ ≤ C * ‖y‖ ^ r for some real C and natural number r. This is condition (d) in the definition of an automorphic form.

Taking the exponent to be a natural number rather than a real is no loss — a real exponent can always be rounded up, since gnorm ≥ 1 / Fintype.card n — and it makes the definition come out right for GL 0, where gnorm is identically 0 and (0 : ℝ) ^ (0 : ℕ) = 1.

def IsSlowlyIncreasing (φ : GL n ℝ → ℂ) : Prop := ∃ (C : ℝ) (r : ℕ), ∀ y : GL n ℝ, ‖φ y‖ ≤ C * gnorm y ^ rlemma IsSlowlyIncreasing.of_bounded {φ : GL n ℝ → ℂ} {C : ℝ} (h : ∀ y, ‖φ y‖ ≤ C) : IsSlowlyIncreasing φ := ⟨C, 0, fun y => n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂC:ℝh:∀ (y : GL n ℝ), ‖φ y‖ ≤ Cy:GL n ℝ⊢ ‖φ y‖ ≤ C * y.gnorm ^ 0 All goals completed! 🐙⟩lemma isSlowlyIncreasing_const (c : ℂ) : IsSlowlyIncreasing (fun _ : GL n ℝ => c) := IsSlowlyIncreasing.of_bounded fun _ => le_rfln:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂc:ℂC:ℝr:ℕhC:∀ (y : GL n ℝ), ‖φ y‖ ≤ C * y.gnorm ^ ry:GL n ℝ⊢ ‖c‖ * ‖φ y‖ ≤ ‖c‖ * (C * y.gnorm ^ r) All goals completed! 🐙

A slow-increase bound with exponent r gives one with any exponent r' ≥ r: gnorm is bounded below by (Fintype.card n)⁻¹ > 0, so enlarging the exponent costs only the constant factor (Fintype.card n) ^ (r' - r).

n:Type u_1inst✝²:Fintype ninst✝¹:DecidableEq ninst✝:Nonempty nφ:GL n ℝ → ℂC:ℝr:ℕh:∀ (y : GL n ℝ), ‖φ y‖ ≤ C * y.gnorm ^ rhcard:0 < ↑(Fintype.card n)hC0:0 ≤ Cd:ℕhr:r ≤ r + dy:GL n ℝhcg:1 ≤ ↑(Fintype.card n) * y.gnorm⊢ ↑(Fintype.card n) ^ d * y.gnorm ^ d * (C * y.gnorm ^ r) = C * ↑(Fintype.card n) ^ d * (y.gnorm ^ r * y.gnorm ^ d); All goals completed! 🐙protected lemma IsSlowlyIncreasing.add {φ ψ : GL n ℝ → ℂ} (hφ : IsSlowlyIncreasing φ) (hψ : IsSlowlyIncreasing ψ) : IsSlowlyIncreasing (φ + ψ) := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSlowlyIncreasing φhψ:IsSlowlyIncreasing ψ⊢ IsSlowlyIncreasing (φ + ψ) n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhψ:IsSlowlyIncreasing ψC₁:ℝr₁:ℕh₁:∀ (y : GL n ℝ), ‖φ y‖ ≤ C₁ * y.gnorm ^ r₁⊢ IsSlowlyIncreasing (φ + ψ); n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂC₁:ℝr₁:ℕh₁:∀ (y : GL n ℝ), ‖φ y‖ ≤ C₁ * y.gnorm ^ r₁C₂:ℝr₂:ℕh₂:∀ (y : GL n ℝ), ‖ψ y‖ ≤ C₂ * y.gnorm ^ r₂⊢ IsSlowlyIncreasing (φ + ψ) n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂC₁:ℝr₁:ℕh₁:∀ (y : GL n ℝ), ‖φ y‖ ≤ C₁ * y.gnorm ^ r₁C₂:ℝr₂:ℕh₂:∀ (y : GL n ℝ), ‖ψ y‖ ≤ C₂ * y.gnorm ^ r₂h✝:IsEmpty n⊢ IsSlowlyIncreasing (φ + ψ)n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂC₁:ℝr₁:ℕh₁:∀ (y : GL n ℝ), ‖φ y‖ ≤ C₁ * y.gnorm ^ r₁C₂:ℝr₂:ℕh₂:∀ (y : GL n ℝ), ‖ψ y‖ ≤ C₂ * y.gnorm ^ r₂h✝:Nonempty n⊢ IsSlowlyIncreasing (φ + ψ) n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂC₁:ℝr₁:ℕh₁:∀ (y : GL n ℝ), ‖φ y‖ ≤ C₁ * y.gnorm ^ r₁C₂:ℝr₂:ℕh₂:∀ (y : GL n ℝ), ‖ψ y‖ ≤ C₂ * y.gnorm ^ r₂h✝:IsEmpty n⊢ IsSlowlyIncreasing (φ + ψ) -- `GL 0 ℝ` is trivial, so every function on it is bounded. n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂC₁:ℝr₁:ℕh₁:∀ (y : GL n ℝ), ‖φ y‖ ≤ C₁ * y.gnorm ^ r₁C₂:ℝr₂:ℕh₂:∀ (y : GL n ℝ), ‖ψ y‖ ≤ C₂ * y.gnorm ^ r₂h✝:IsEmpty nthis:Subsingleton (GL n ℝ)⊢ IsSlowlyIncreasing (φ + ψ) exact IsSlowlyIncreasing.of_bounded (C := ‖φ 1‖ + ‖ψ 1‖) fun y => n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂC₁:ℝr₁:ℕh₁:∀ (y : GL n ℝ), ‖φ y‖ ≤ C₁ * y.gnorm ^ r₁C₂:ℝr₂:ℕh₂:∀ (y : GL n ℝ), ‖ψ y‖ ≤ C₂ * y.gnorm ^ r₂h✝:IsEmpty nthis:Subsingleton (GL n ℝ)y:GL n ℝ⊢ ‖(φ + ψ) y‖ ≤ ‖φ 1‖ + ‖ψ 1‖ n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂC₁:ℝr₁:ℕh₁:∀ (y : GL n ℝ), ‖φ y‖ ≤ C₁ * y.gnorm ^ r₁C₂:ℝr₂:ℕh₂:∀ (y : GL n ℝ), ‖ψ y‖ ≤ C₂ * y.gnorm ^ r₂h✝:IsEmpty nthis:Subsingleton (GL n ℝ)⊢ ‖(φ + ψ) 1‖ ≤ ‖φ 1‖ + ‖ψ 1‖ All goals completed! 🐙 n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂC₁:ℝr₁:ℕh₁:∀ (y : GL n ℝ), ‖φ y‖ ≤ C₁ * y.gnorm ^ r₁C₂:ℝr₂:ℕh₂:∀ (y : GL n ℝ), ‖ψ y‖ ≤ C₂ * y.gnorm ^ r₂h✝:Nonempty n⊢ IsSlowlyIncreasing (φ + ψ) n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂC₁:ℝr₁:ℕh₁:∀ (y : GL n ℝ), ‖φ y‖ ≤ C₁ * y.gnorm ^ r₁C₂:ℝr₂:ℕh₂:∀ (y : GL n ℝ), ‖ψ y‖ ≤ C₂ * y.gnorm ^ r₂h✝:Nonempty nC₁':ℝh₁':∀ (y : GL n ℝ), ‖φ y‖ ≤ C₁' * y.gnorm ^ max r₁ r₂⊢ IsSlowlyIncreasing (φ + ψ) n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂC₁:ℝr₁:ℕh₁:∀ (y : GL n ℝ), ‖φ y‖ ≤ C₁ * y.gnorm ^ r₁C₂:ℝr₂:ℕh₂:∀ (y : GL n ℝ), ‖ψ y‖ ≤ C₂ * y.gnorm ^ r₂h✝:Nonempty nC₁':ℝh₁':∀ (y : GL n ℝ), ‖φ y‖ ≤ C₁' * y.gnorm ^ max r₁ r₂C₂':ℝh₂':∀ (y : GL n ℝ), ‖ψ y‖ ≤ C₂' * y.gnorm ^ max r₁ r₂⊢ IsSlowlyIncreasing (φ + ψ) All goals completed! 🐙

Constant functions are Z(𝔤)-finite

The constant function 1 is Z(𝔤)-finite: the kernel of constantsCharacter is an ideal of finite codimension annihilating it.

lemma isZFinite_oneSmoothGL : IsZFinite ℂ ↥(centerUniversalEnveloping n) (oneSmoothGL n) := IsZFinite.of_forall_smul_eq_algHom_smul (constantsCharacter n) fun z => eq_smul_oneSmoothGL_of_mem_span (smul_oneSmoothGL_mem_span z)

Every constant function is Z(𝔤)-finite.

lemma isZFinite_const_smoothGL (c : ℂ) : IsZFinite ℂ ↥(centerUniversalEnveloping n) (⟨fun _ => c, isSmoothOnGL_const c⟩ : smoothGL n) := (Subtype.ext (funext fun _ => mul_one c) : c • oneSmoothGL n = ⟨fun _ => c, _⟩) ▸ isZFinite_oneSmoothGL.const_smul c

The definition

Smoothness of a function on G(𝔸) = G(𝔸_f) × G(ℝ), with G(𝔸_f) = GL n 𝔸ᶠ[ℤ, ℚ]: continuous, locally constant in the finite variable, and C^∞ in the archimedean variable.

structure IsSmoothAdelic (f : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂ) : Prop where continuous : Continuous f locallyConstant : ∀ y : GL n ℝ, IsLocallyConstant fun x : GL n 𝔸ᶠ[ℤ, ℚ] => f (x, y) smoothOnGL : ∀ x : GL n 𝔸ᶠ[ℤ, ℚ], IsSmoothOnGL fun y : GL n ℝ => f (x, y)

An automorphic form for (G, K) in the sense of Borel-Jacquet, with G = GL n / ℚ and K = O n ℝ: G(𝔸) is written as G(𝔸_f) × G(ℝ) = GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ, condition (a) is invariance under ratDiagonal n, the rational points embedded diagonally, condition (b2) is finiteness under the maximal compact orthogonalSubgroup n, and condition (c) is with respect to the action of the centre of the universal enveloping algebra by left invariant differential operators, centerAction.

structure IsAutomorphicForm (f : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂ) : Prop where

f is smooth.

smooth : IsSmoothAdelic f

(a) f (γ x) = f x for γ ∈ G(ℚ).

left_invariant : ∀ γ ∈ ratDiagonal n, ∀ x, f (γ * x) = f x

(b1) f is right invariant under some compact open subgroup of G(𝔸_f).

right_invariant : ∃ U : Subgroup (GL n 𝔸ᶠ[ℤ, ℚ]), IsOpen (U : Set (GL n 𝔸ᶠ[ℤ, ℚ])) ∧ IsCompact (U : Set (GL n 𝔸ᶠ[ℤ, ℚ])) ∧ ∀ u ∈ U, ∀ x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ, f (x.1 * u, x.2) = f x

(b2) f is K-finite.

kFinite : IsKFinite ((⊥ : Subgroup (GL n 𝔸ᶠ[ℤ, ℚ])).prod (orthogonalSubgroup n)) ℂ f

(c) f is annihilated by an ideal of finite codimension of the centre of the universal enveloping algebra, acting in the archimedean variable. One ideal annihilates every finite-adelic slice at once.

zFinite : IsZFinite ℂ ↥(centerUniversalEnveloping n) (fun x : GL n 𝔸ᶠ[ℤ, ℚ] => (⟨fun y => f (x, y), smooth.smoothOnGL x⟩ : smoothGL n))

(d) y ↦ f (x, y) is slowly increasing for each x ∈ G(𝔸_f).

slowlyIncreasing : ∀ x : GL n 𝔸ᶠ[ℤ, ℚ], IsSlowlyIncreasing fun y => f (x, y)

The submodule of automorphic forms and the right translation action

lemma isSmoothAdelic_const (c : ℂ) : IsSmoothAdelic (fun _ : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ => c) where continuous := continuous_const locallyConstant _ := IsLocallyConstant.const c smoothOnGL _ := isSmoothOnGL_const cprotected lemma IsSmoothAdelic.add {f g : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂ} (hf : IsSmoothAdelic f) (hg : IsSmoothAdelic g) : IsSmoothAdelic (f + g) where continuous := hf.continuous.add hg.continuous locallyConstant y := (hf.locallyConstant y).add (hg.locallyConstant y) smoothOnGL x := (hf.smoothOnGL x).add (hg.smoothOnGL x)protected lemma IsSmoothAdelic.const_smul {f : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂ} (hf : IsSmoothAdelic f) (c : ℂ) : IsSmoothAdelic (c • f) where continuous := hf.continuous.const_smul c locallyConstant y := (hf.locallyConstant y).comp (c • ·) smoothOnGL x := (hf.smoothOnGL x).const_smul cvariable (n) in

Sanity check: the constant functions are automorphic forms. This exercises every condition of the definition: condition (b1) is witnessed by the compact open subgroup integralAdelicSubgroup n and condition (c) by the kernel of constantsCharacter n.

theorem isAutomorphicForm_const (c : ℂ) : IsAutomorphicForm (fun _ : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ => c) where smooth := isSmoothAdelic_const c left_invariant _ _ _ := rfl right_invariant := ⟨integralAdelicSubgroup n, isOpen_integralAdelicSubgroup, isCompact_integralAdelicSubgroup, fun _ _ _ => rfl⟩ kFinite := isKFinite_of_rightInvariant fun _ _ => rfl zFinite := (isZFinite_const_smoothGL c).pi_const slowlyIncreasing _ := isSlowlyIncreasing_const cvariable (n) in

Sanity check: the constant function 1 is an automorphic form.

theorem isAutomorphicForm_one : IsAutomorphicForm (fun _ : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ => (1 : ℂ)) := isAutomorphicForm_const n 1protected lemma IsAutomorphicForm.add {f g : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂ} (hf : IsAutomorphicForm f) (hg : IsAutomorphicForm g) : IsAutomorphicForm (f + g) where smooth := hf.smooth.add hg.smooth left_invariant γ hγ x := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂg:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂhf:IsAutomorphicForm fhg:IsAutomorphicForm gγ:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝhγ:γ ∈ ratDiagonal nx:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ⊢ (f + g) (γ * x) = (f + g) x All goals completed! 🐙 right_invariant := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂg:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂhf:IsAutomorphicForm fhg:IsAutomorphicForm g⊢ ∃ U, IsOpen ↑U ∧ IsCompact ↑U ∧ ∀ u ∈ U, ∀ (x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ), (f + g) (x.1 * u, x.2) = (f + g) x n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂg:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂhf:IsAutomorphicForm fhg:IsAutomorphicForm gU₁:Subgroup (GL n 𝔸ᶠ[ℤ, ℚ])o₁:IsOpen ↑U₁c₁:IsCompact ↑U₁h₁:∀ u ∈ U₁, ∀ (x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ), f (x.1 * u, x.2) = f xU₂:Subgroup (GL n 𝔸ᶠ[ℤ, ℚ])o₂:IsOpen ↑U₂c₂:IsCompact ↑U₂h₂:∀ u ∈ U₂, ∀ (x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ), g (x.1 * u, x.2) = g x⊢ ∃ U, IsOpen ↑U ∧ IsCompact ↑U ∧ ∀ u ∈ U, ∀ (x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ), (f + g) (x.1 * u, x.2) = (f + g) x exact ⟨U₁ ⊓ U₂, Subgroup.coe_inf U₁ U₂ ▸ o₁.inter o₂, Subgroup.coe_inf U₁ U₂ ▸ c₁.inter_right (U₂.isClosed_of_isOpen o₂), fun u hu x => n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂg:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂhf:IsAutomorphicForm fhg:IsAutomorphicForm gU₁:Subgroup (GL n 𝔸ᶠ[ℤ, ℚ])o₁:IsOpen ↑U₁c₁:IsCompact ↑U₁h₁:∀ u ∈ U₁, ∀ (x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ), f (x.1 * u, x.2) = f xU₂:Subgroup (GL n 𝔸ᶠ[ℤ, ℚ])o₂:IsOpen ↑U₂c₂:IsCompact ↑U₂h₂:∀ u ∈ U₂, ∀ (x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ), g (x.1 * u, x.2) = g xu:GL n 𝔸ᶠ[ℤ, ℚ]hu:u ∈ U₁ ⊓ U₂x:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ⊢ (f + g) (x.1 * u, x.2) = (f + g) x All goals completed! 🐙⟩ kFinite := hf.kFinite.add hg.kFinite zFinite := hf.zFinite.add hg.zFinite slowlyIncreasing x := (hf.slowlyIncreasing x).add (hg.slowlyIncreasing x)protected lemma IsAutomorphicForm.const_smul {f : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂ} (hf : IsAutomorphicForm f) (c : ℂ) : IsAutomorphicForm (c • f) where smooth := hf.smooth.const_smul c left_invariant γ hγ x := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂhf:IsAutomorphicForm fc:ℂγ:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝhγ:γ ∈ ratDiagonal nx:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ⊢ (c • f) (γ * x) = (c • f) x All goals completed! 🐙 right_invariant := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂhf:IsAutomorphicForm fc:ℂ⊢ ∃ U, IsOpen ↑U ∧ IsCompact ↑U ∧ ∀ u ∈ U, ∀ (x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ), (c • f) (x.1 * u, x.2) = (c • f) x n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂhf:IsAutomorphicForm fc:ℂU:Subgroup (GL n 𝔸ᶠ[ℤ, ℚ])ho:IsOpen ↑Uhc':IsCompact ↑UhU:∀ u ∈ U, ∀ (x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ), f (x.1 * u, x.2) = f x⊢ ∃ U, IsOpen ↑U ∧ IsCompact ↑U ∧ ∀ u ∈ U, ∀ (x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ), (c • f) (x.1 * u, x.2) = (c • f) x exact ⟨U, ho, hc', fun u hu x => n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂhf:IsAutomorphicForm fc:ℂU:Subgroup (GL n 𝔸ᶠ[ℤ, ℚ])ho:IsOpen ↑Uhc':IsCompact ↑UhU:∀ u ∈ U, ∀ (x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ), f (x.1 * u, x.2) = f xu:GL n 𝔸ᶠ[ℤ, ℚ]hu:u ∈ Ux:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ⊢ (c • f) (x.1 * u, x.2) = (c • f) x All goals completed! 🐙⟩ kFinite := hf.kFinite.const_smul c zFinite := hf.zFinite.const_smul c slowlyIncreasing x := (hf.slowlyIncreasing x).const_mul cvariable (n) in

The automorphic forms for GL n / ℚ as a ℂ-submodule of the functions on G(𝔸).

def automorphicForms : Submodule ℂ (GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂ) where carrier := {f | IsAutomorphicForm f} add_mem' hf hg := hf.add hg zero_mem' := isAutomorphicForm_const n 0 smul_mem' c _ hf := hf.const_smul c@[simp] lemma mem_automorphicForms {f : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂ} : f ∈ automorphicForms n ↔ IsAutomorphicForm f := Iff.rfl

Automorphy is preserved by right translation in the finite variable.

n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂhf:IsAutomorphicForm fg:GL n 𝔸ᶠ[ℤ, ℚ]U:Subgroup (GL n 𝔸ᶠ[ℤ, ℚ])ho:IsOpen ↑Uhc:IsCompact ↑UhU:∀ u ∈ U, ∀ (x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ), f (x.1 * u, x.2) = f xhset:↑(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) U) = (fun x ↦ g * x * g⁻¹) '' ↑U⊢ ∃ U, IsOpen ↑U ∧ IsCompact ↑U ∧ ∀ u ∈ U, ∀ (x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ), f ((x.1 * u, x.2).1 * g, (x.1 * u, x.2).2) = f (x.1 * g, x.2) n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂhf:IsAutomorphicForm fg:GL n 𝔸ᶠ[ℤ, ℚ]U:Subgroup (GL n 𝔸ᶠ[ℤ, ℚ])ho:IsOpen ↑Uhc:IsCompact ↑UhU:∀ u ∈ U, ∀ (x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ), f (x.1 * u, x.2) = f xhset:↑(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) U) = (fun x ↦ g * x * g⁻¹) '' ↑Uu:GL n 𝔸ᶠ[ℤ, ℚ]hu:u ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) Ux:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ⊢ f ((x.1 * u, x.2).1 * g, (x.1 * u, x.2).2) = f (x.1 * g, x.2) n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂhf:IsAutomorphicForm fg:GL n 𝔸ᶠ[ℤ, ℚ]U:Subgroup (GL n 𝔸ᶠ[ℤ, ℚ])ho:IsOpen ↑Uhc:IsCompact ↑UhU:∀ u ∈ U, ∀ (x : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ), f (x.1 * u, x.2) = f xhset:↑(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) U) = (fun x ↦ g * x * g⁻¹) '' ↑Ux:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝw:GL n 𝔸ᶠ[ℤ, ℚ]hw:w ∈ Uhu:(MulEquiv.toMonoidHom (MulAut.conj g)) w ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) U⊢ f ((x.1 * (MulEquiv.toMonoidHom (MulAut.conj g)) w, x.2).1 * g, (x.1 * (MulEquiv.toMonoidHom (MulAut.conj g)) w, x.2).2) = f (x.1 * g, x.2) All goals completed! 🐙 kFinite := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂhf:IsAutomorphicForm fg:GL n 𝔸ᶠ[ℤ, ℚ]⊢ IsKFinite (⊥.prod (orthogonalSubgroup n)) ℂ fun p ↦ f (p.1 * g, p.2) n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂhf:IsAutomorphicForm fg:GL n 𝔸ᶠ[ℤ, ℚ]this:IsKFinite (⊥.prod (orthogonalSubgroup n)) ℂ f⊢ IsKFinite (⊥.prod (orthogonalSubgroup n)) ℂ fun p ↦ f (p.1 * g, p.2) refine Submodule.finiteDimensional_of_le (S₂ := Submodule.map (LinearMap.funLeft ℂ ℂ fun p : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ => (p.1 * g, p.2)) (rightTranslateSpan ((⊥ : Subgroup (GL n 𝔸ᶠ[ℤ, ℚ])).prod (orthogonalSubgroup n)) ℂ f)) (Submodule.span_le.mpr <| Set.range_subset_iff.mpr fun u => Submodule.mem_map.mpr ⟨_, Submodule.subset_span ⟨u, rfl⟩, funext fun p => n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂhf:IsAutomorphicForm fg:GL n 𝔸ᶠ[ℤ, ℚ]this:IsKFinite (⊥.prod (orthogonalSubgroup n)) ℂ fu:↥(⊥.prod (orthogonalSubgroup n))p:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ⊢ (LinearMap.funLeft ℂ ℂ fun p ↦ (p.1 * g, p.2)) ((fun u x ↦ f (x * ↑u)) u) p = (fun p ↦ f (p.1 * g, p.2)) (p * ↑u) All goals completed! 🐙⟩) zFinite := hf.zFinite.comp (· * g) slowlyIncreasing x := hf.slowlyIncreasing (x * g)variable (n) in

The right translation representation of G(𝔸_f) on the automorphic forms: g acts by f ↦ fun (x, y) => f (x * g, y).

noncomputable def rightTranslation : GL n 𝔸ᶠ[ℤ, ℚ] →* (automorphicForms n →ₗ[ℂ] automorphicForms n) where toFun g := { toFun := fun f => ⟨fun p => (f : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂ) (p.1 * g, p.2), f.2.rightTranslate g⟩ map_add' := fun _ _ => Subtype.ext rfl map_smul' := fun _ _ => Subtype.ext rfl } map_one' := LinearMap.ext fun f => Subtype.ext (funext fun p => n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nf:↥(automorphicForms n)p:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ⊢ ↑({ toFun := fun f ↦ ⟨fun p ↦ ↑f (p.1 * 1, p.2), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } f) p = ↑(1 f) p All goals completed! 🐙) map_mul' g h := LinearMap.ext fun f => Subtype.ext (funext fun p => n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq ng:GL n 𝔸ᶠ[ℤ, ℚ]h:GL n 𝔸ᶠ[ℤ, ℚ]f:↥(automorphicForms n)p:GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ⊢ ↑({ toFun := fun f ↦ ⟨fun p ↦ ↑f (p.1 * (g * h), p.2), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } f) p = ↑(({ toFun := fun f ↦ ⟨fun p ↦ ↑f (p.1 * g, p.2), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } * { toFun := fun f ↦ ⟨fun p ↦ ↑f (p.1 * h, p.2), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }) f) p All goals completed! 🐙)end Matrix.GeneralLinearGroup