/-
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 Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
public import Mathlib.LinearAlgebra.UnitaryGroup
public import Mathlib.NumberTheory.Padics.HeightOneSpectrum
public import Mathlib.NumberTheory.Padics.ProperSpace
public import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
public import Mathlib.Topology.Algebra.Group.Matrix
public import Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
public import Mathlib.Topology.Instances.Matrix@[expose] public sectionThe subgroups in the Borel-Jacquet definition of an automorphic form
The subgroups of G(𝔸) = G(𝔸_f) × G(ℝ), for G = GL n / ℚ, that the Borel-Jacquet
definition of an automorphic form quantifies over; see
FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet for that definition,
and Borel and Jacquet's Corvallis article, the reference below, for its source.
Main declarations
All in the namespace Matrix.GeneralLinearGroup:
diagonalEmbedding and ratDiagonal: the diagonal copy of the rational points
Γ = G(ℚ) = GL n ℚ in G(𝔸_f) × G(ℝ), the subgroup of condition (a).
orthogonalSubgroup: the orthogonal group K = O n ℝ inside GL n ℝ, the maximal compact
subgroup of condition (b2) — mathlib's Matrix.orthogonalGroup n ℝ, a submonoid of
Matrix n n ℝ, transported along the coercion to a subgroup of GL n ℝ.
integralAdeles and integralAdelicSubgroup: the integral adeles Ẑ and the compact open
subgroup GL n Ẑ of G(𝔸_f) (isOpen_integralAdelicSubgroup,
isCompact_integralAdelicSubgroup), which witnesses condition (b1) for constant automorphic
forms.
Implementation notes
Compactness of orthogonalSubgroup n and its maximality (Cartan-Iwasawa-Malcev, which also
makes it unique up to conjugacy) are asserted in its docstring but not formalised; of
compactness, the boundedness half is proved (abs_coe_le_one_of_mem_orthogonalSubgroup).
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.
namespace Matrix.GeneralLinearGroupopen scoped IsDedekindDomain.FiniteAdeleRingvariable {n : Type*} [Fintype n] [DecidableEq n]
The subgroups Γ = G(ℚ) and K = O n ℝ: conditions (a) and (b2)
variable (n) in
The diagonal embedding of the rational points G(ℚ) = GL n ℚ into
G(𝔸_f) × G(ℝ) = GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ, through the inclusions of ℚ into the finite
adeles and into ℝ.
noncomputable def diagonalEmbedding : GL n ℚ →* GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ :=
(map (algebraMap ℚ 𝔸ᶠ[ℤ, ℚ])).prod (map (algebraMap ℚ ℝ))variable (n) in
The subgroup Γ = G(ℚ) of G(𝔸_f) × G(ℝ): the range of the diagonal embedding of
GL n ℚ. Condition (a) for an automorphic form is left invariance under this subgroup.
noncomputable def ratDiagonal : Subgroup (GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ) :=
(diagonalEmbedding n).range
The orthogonal group O n ℝ as a subgroup of GL n ℝ: the units of Matrix n n ℝ whose
underlying matrix lies in mathlib's Matrix.orthogonalGroup n ℝ, the submonoid of matrices
whose transpose is their inverse. This is the maximal compact subgroup of GL n ℝ — up to
conjugacy the only one, by the Cartan-Iwasawa-Malcev theorem — and it is the K of the pair
(G, K) in the definition of an automorphic form for GL n.
Mathlib's Matrix.orthogonalGroup n ℝ is a Submonoid (Matrix n n ℝ); what the definition of
an automorphic form needs is a Subgroup (GL n ℝ), so we transport it along the coercion
GL n ℝ → Matrix n n ℝ rather than restate the orthogonality condition.
n✝:Type u_1inst✝³:Fintype n✝inst✝²:DecidableEq n✝n:Type u_2inst✝¹:Fintype ninst✝:DecidableEq na:GL n ℝha:↑a * (↑a)ᵀ = 1⊢ (↑a)ᵀ * ↑a = 1
All goals completed! 🐙lemma mem_orthogonalSubgroup {y : GL n ℝ} :
y ∈ orthogonalSubgroup n ↔ (y : Matrix n n ℝ) ∈ Matrix.orthogonalGroup n ℝ :=
Set.mem_ofPred_eq ▸ Iff.rfl@[simp]
lemma mem_orthogonalSubgroup_iff_mul_transpose {y : GL n ℝ} :
y ∈ orthogonalSubgroup n ↔ (y : Matrix n n ℝ) * (y : Matrix n n ℝ)ᵀ = 1 :=
mem_orthogonalSubgroup.trans (Matrix.mem_orthogonalGroup_iff n ℝ)n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq ny:GL n ℝh:(↑y)ᵀ = ↑y⁻¹⊢ ↑y * ↑y⁻¹ = 1; All goals completed! 🐙
The entries of an orthogonal matrix are bounded by 1: each row is a unit vector. This is
the boundedness half of the compactness of orthogonalSubgroup n; see the implementation notes
on what is and is not formalised about that.
n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq ny:GL n ℝhy:y ∈ orthogonalSubgroup ni:nj:nM:Matrix n n ℝ := ↑yhM:M = ↑yhd:∑ k, M i k * M i k = 1⊢ |M i j| ≤ 1
All goals completed! 🐙
The compact open subgroup GL n Ẑ: condition (b1)
section IntegralSubgroupopen IsDedekindDomain RestrictedProduct
The v-adic integers of ℚ are compact: they are homeomorphic to ℤ_[p] for the
corresponding prime p.
instance (v : HeightOneSpectrum ℤ) : CompactSpace (v.adicCompletionIntegers ℚ) := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nv:HeightOneSpectrum ℤ⊢ CompactSpace ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)
n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nv:HeightOneSpectrum ℤthis:Fact (Nat.Prime ↑(Rat.HeightOneSpectrum.primesEquiv v))⊢ CompactSpace ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)
n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nv:HeightOneSpectrum ℤthis:Fact (Nat.Prime ↑(Rat.HeightOneSpectrum.primesEquiv v))x✝:Algebra ℤ ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v) := Ring.toIntAlgebra ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)⊢ CompactSpace ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)
All goals completed! 🐙instance : T2Space 𝔸ᶠ[ℤ, ℚ] :=
inferInstanceAs (T2Space (Πʳ v : HeightOneSpectrum ℤ,
[v.adicCompletion ℚ, v.adicCompletionIntegers ℚ]))
The integral adeles Ẑ = ∏ᵥ ℤᵥ as a subring of the finite adeles of ℚ: the adeles that
are integral at every place.
def integralAdeles : Subring 𝔸ᶠ[ℤ, ℚ] where
carrier := {x | ∀ v, x v ∈ v.adicCompletionIntegers ℚ}
one_mem' _v := one_mem _
mul_mem' hx hy v := mul_mem (hx v) (hy v)
zero_mem' _v := zero_mem _
add_mem' hx hy v := add_mem (hx v) (hy v)
neg_mem' hx v := neg_mem (hx v)lemma isOpen_integralAdeles : IsOpen (integralAdeles : Set 𝔸ᶠ[ℤ, ℚ]) :=
RestrictedProduct.isOpen_forall_mem fun _ => Valued.isOpen_valuationSubring _h:↑integralAdeles =
Set.range
(structureMap (fun v ↦ HeightOneSpectrum.adicCompletion ℚ v)
(fun v ↦ ↑(HeightOneSpectrum.adicCompletionIntegers ℚ v)) Filter.cofinite)⊢ IsCompact
(structureMap (fun v ↦ HeightOneSpectrum.adicCompletion ℚ v) (fun v ↦ ↑(HeightOneSpectrum.adicCompletionIntegers ℚ v))
Filter.cofinite ''
Set.univ)
All goals completed! 🐙variable (n) in
GL n Ẑ inside GL n 𝔸ᶠ[ℤ, ℚ]: the matrices whose entries, and whose inverse's entries,
are integral adeles. It is a compact open subgroup of G(𝔸_f)
(isOpen_integralAdelicSubgroup, isCompact_integralAdelicSubgroup), as condition (b1)
requires.
n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq na:GL n 𝔸ᶠ[ℤ, ℚ]ha:a ∈ {g | (∀ (i j : n), ↑g i j ∈ integralAdeles) ∧ ∀ (i j : n), ↑g⁻¹ i j ∈ integralAdeles}⊢ ∀ (i j : n), ↑a i j ∈ integralAdeles; All goals completed! 🐙⟩n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nhW:IsOpen {M | ∀ (i j : n), M i j ∈ integralAdeles}⊢ IsOpen ↑(integralAdelicSubgroup n)
All goals completed! 🐙n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nW:Set (Matrix n n 𝔸ᶠ[ℤ, ℚ]) := {M | ∀ (i j : n), M i j ∈ integralAdeles}hWdef:W = {M | ∀ (i j : n), M i j ∈ integralAdeles}hWc:IsCompact Whimg:⇑(Units.embedProduct (Matrix n n 𝔸ᶠ[ℤ, ℚ])) '' ↑(integralAdelicSubgroup n) =
(fun p ↦ (p.1, MulOpposite.op p.2)) '' (W ×ˢ W ∩ {p | p.1 * p.2 = 1} ∩ {p | p.2 * p.1 = 1})⊢ IsCompact ((fun p ↦ (p.1, MulOpposite.op p.2)) '' (W ×ˢ W ∩ {p | p.1 * p.2 = 1} ∩ {p | p.2 * p.1 = 1}))
All goals completed! 🐙end IntegralSubgroupend Matrix.GeneralLinearGroup