GLnDefs.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

31 declarations, 4 contain sorry, 0 declared as axioms

The Global Langlands Conjectures for GL(n) over the rationals.

This code never fully worked because we didn't get as far as weights at infinity. It has then since degraded (two major problems being the bump to 4.29 and the introduction of the module system) and is now probably worth very little.

First sub-goal: definition of an automorphic form.

I've made the design decision of working with the functor Matrix.GeneralLinearGroup (Fin n) as our implementation of the GL_n functor. There's notation GL (Fin n) for this.

Imports (8)

Imported by 2 files

def IsDedekindDomain.bracketBilin The action of a Lie R-algebra on a Lie R-module, as an R-bilinear map line 50 source
Source documentation
The action of a Lie R-algebra on a Lie R-module, as an R-bilinear map.

standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, LieRing, LieAlgebra, AddCommGroup, Module, LieRingModule, LieModule, LinearMap, RingHom.id
Proof uses: LinearMap.mk₂, Bracket.bracket, add_lie, smul_lie, lie_add, lie_smul
20 instances, coercions and auxiliary constants left out.
```
def bracketBilin (R L M) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M]
    [LieRingModule L M] [LieModule R L M] :
    L →ₗ[R] M →ₗ[R] M :=
…
```
instance IsDedekindDomain.instLieAlgebra' line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, LieRing, LieAlgebra, SMulCommClass, TensorProduct
Proof uses: LieAlgebra.mk
20 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem IsDedekindDomain.diamond_fix sorry line 76 source
depends on sorry what this means
Statement uses: CommRing, Ring, Algebra, Eq, Bracket, TensorProduct, LieRing.ofAssociativeRing
Proof uses: Bracket.ext, funext, Bracket.bracket, Eq.mpr, LinearMap, RingHom.id, IsDedekindDomain.bracketBilin, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, IsDedekindDomain.bracketBilin_apply_apply, LinearMap.congr_fun₂, TensorProduct.AlgebraTensorModule.curry_injective, LinearMap.ext, TensorProduct.AlgebraTensorModule.curry, TensorProduct.tmul, HMul.hMul and 14 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
def AutomorphicForm.GLn.action The action of the Lie algebra of left-invariant derivations on a Lie group G on smooth real-valued functions on G, viewed as a Lie algebra homomorphism line 126 source
Source documentation
The action of the Lie algebra of left-invariant derivations on a Lie group G on smooth real-valued functions on G, viewed as a Lie algebra homomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Group, NormedAddCommGroup, NormedSpace, Real, ChartedSpace, LieGroup, modelWithCornersSelf, Top.top, WithTop, ENat, LieHom, LeftInvariantDerivation, Module.End, ContMDiffMap, LieRing.ofAssociativeRing
Proof uses: LieHom.mk, LinearMap.mk, RingHom.id, AddHom.mk
101 instances, coercions and auxiliary constants left out.
```
def action :
    LeftInvariantDerivation 𝓘(ℝ, E) G →ₗ⁅ℝ⁆ (Module.End ℝ C^∞⟮𝓘(ℝ, E), G; ℝ⟯) where
…
```
def AutomorphicForm.GLn.LieModuleHom.baseChange Base change of a Lie module homomorphism f : M →ₗ⁅R,L⁆ N along a commutative algebra A over R line 137 source
Source documentation
Base change of a Lie module homomorphism f : M →ₗ⁅R,L⁆ N along a commutative algebra A over R.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, LieRing, LieAlgebra, AddCommGroup, Module, LieRingModule, LieModule, LieModuleHom, TensorProduct, LieRing.ofAssociativeRing
Proof uses: LinearMap, RingHom.id, LinearMap.baseChange, LieModuleHom.mk
33 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
def LieModuleHom.baseChange
    (A : Type*) {R L M N : Type*}
    [CommRing R] [CommRing A] [Algebra R A]
    [LieRing L] [LieAlgebra R L]
    [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]
    [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N]
    (f : M →ₗ⁅R,L⁆ N) : A ⊗[R] M →ₗ⁅A, A ⊗[R] L⁆ A ⊗[R] N where
…
```
def AutomorphicForm.GLn.LieHom.baseChange Base change of a Lie algebra homomorphism f : L →ₗ⁅R⁆ L' along a commutative algebra A over R line 154 source
Source documentation
Base change of a Lie algebra homomorphism f : L →ₗ⁅R⁆ L' along a commutative algebra A over R.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, LieRing, LieAlgebra, LieHom, TensorProduct, LieRing.ofAssociativeRing
Proof uses: LinearMap, RingHom.id, LinearMap.baseChange, LieHom.mk
31 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
def LieHom.baseChange
    (A : Type*) {R L L' : Type*}
    [CommRing R] [CommRing A] [Algebra R A]
    [LieRing L] [LieAlgebra R L]
    [LieRing L'] [LieAlgebra R L']
    (f : L →ₗ⁅R⁆ L') : A ⊗[R] L →ₗ⁅A⁆ A ⊗[R] L' where
…
```
def AutomorphicForm.GLn.actionTensorC Complexification of AutomorphicForm.GLn.action: the Lie action of the complexified Lie algebra on the complexification of smooth real functions on G line 170 source
Source documentation
Complexification of AutomorphicForm.GLn.action: the Lie action of the complexified Lie algebra on the complexification of smooth real functions on G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Group, NormedAddCommGroup, NormedSpace, Real, ChartedSpace, LieGroup, modelWithCornersSelf, Top.top, WithTop, ENat, LieHom, Complex, TensorProduct, LeftInvariantDerivation, Module.End, ContMDiffMap, RingHom.id, LieRing.ofAssociativeRing
Proof uses: AutomorphicForm.GLn.LieHom.baseChange, AutomorphicForm.GLn.action
124 instances, coercions and auxiliary constants left out.
```
def actionTensorC :
    ℂ ⊗[ℝ] LeftInvariantDerivation 𝓘(ℝ, E) G →ₗ⁅ℂ⁆ (ℂ ⊗[ℝ] (Module.End ℝ C^∞⟮𝓘(ℝ, E), G; ℝ⟯)) :=
…
```
def AutomorphicForm.GLn.actionTensorCAlg Extension of AutomorphicForm.GLn.actionTensorC to the universal enveloping algebra of the complexified Lie algebra sorry line 176 source
Source documentation
Extension of AutomorphicForm.GLn.actionTensorC to the universal enveloping algebra of the complexified Lie algebra.

depends on sorry what this means
Statement uses: TopologicalSpace, Group, NormedAddCommGroup, NormedSpace, Real, ChartedSpace, LieGroup, modelWithCornersSelf, Top.top, WithTop, ENat, AlgHom, Complex, UniversalEnvelopingAlgebra, TensorProduct, LeftInvariantDerivation, Module.End, ContMDiffMap, RingHom.id
Proof uses: LieHom, LieRing.ofAssociativeRing, AutomorphicForm.GLn.actionTensorC, Eq.mpr, implies_congr, eq_of_heq, Eq.refl, id, HEq, LieAlgebra, sorryAx, Lean.Name, Eq, LieRing, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat and 15 more
201 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
def actionTensorCAlg :
  UniversalEnvelopingAlgebra ℂ (ℂ ⊗[ℝ] LeftInvariantDerivation 𝓘(ℝ, E) G) →ₐ[ℂ]
    ℂ ⊗[ℝ] (Module.End ℝ C^∞⟮𝓘(ℝ, E), G; 𝓘(ℝ, ℝ), ℝ⟯) := by
…
```
def AutomorphicForm.GLn.actionTensorCAlg' Variant of actionTensorCAlg whose codomain is the ℂ-linear endomorphisms of the complexified function space line 193 source
Source documentation
Variant of actionTensorCAlg whose codomain is the ℂ-linear endomorphisms of the complexified function space.

depends on sorry what this means
Statement uses: TopologicalSpace, Group, NormedAddCommGroup, NormedSpace, Real, ChartedSpace, LieGroup, modelWithCornersSelf, Top.top, WithTop, ENat, AlgHom, Complex, UniversalEnvelopingAlgebra, TensorProduct, LeftInvariantDerivation, Module.End, ContMDiffMap
Proof uses: AlgHom.comp, RingHom.id, LinearMap.tensorProductEnd, AutomorphicForm.GLn.actionTensorCAlg
146 instances, coercions and auxiliary constants left out.
```
def actionTensorCAlg' :
  UniversalEnvelopingAlgebra ℂ (ℂ ⊗[ℝ] LeftInvariantDerivation 𝓘(ℝ, E) G) →ₐ[ℂ]
    Module.End ℂ (ℂ ⊗[ℝ] C^∞⟮𝓘(ℝ, E), G; 𝓘(ℝ, ℝ), ℝ⟯) :=
…
```
def AutomorphicForm.GLn.actionTensorCAlg'2 Restriction of actionTensorCAlg' to the centre of the universal enveloping algebra line 199 source
Source documentation
Restriction of actionTensorCAlg' to the centre of the universal enveloping algebra.

depends on sorry what this means
Statement uses: TopologicalSpace, Group, NormedAddCommGroup, NormedSpace, Real, ChartedSpace, LieGroup, modelWithCornersSelf, Top.top, WithTop, ENat, AlgHom, Complex, Subtype, UniversalEnvelopingAlgebra, TensorProduct, LeftInvariantDerivation, Membership.mem, Subalgebra, Subalgebra.center and 2 more
Proof uses: AlgHom.comp, AutomorphicForm.GLn.actionTensorCAlg', SubalgebraClass.val
146 instances, coercions and auxiliary constants left out.
```
def actionTensorCAlg'2 :
  Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ
    (ℂ ⊗[ℝ] LeftInvariantDerivation 𝓘(ℝ, E) G)) →ₐ[ℂ]
    Module.End ℂ (ℂ ⊗[ℝ] C^∞⟮𝓘(ℝ, E), G; 𝓘(ℝ, ℝ), ℝ⟯) :=
…
```
instance AutomorphicForm.GLn.(instance at line 205) line 205 source
instance AutomorphicForm.GLn.(instance at line 206) sorry line 206 source
def AutomorphicForm.GLn.Alg The universal enveloping algebra over ℂ of the complexified Lie algebra of G line 209 source
Source documentation
The universal enveloping algebra over ℂ of the complexified Lie algebra of G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Group, NormedAddCommGroup, NormedSpace, Real, ChartedSpace, LieGroup, modelWithCornersSelf, Top.top, WithTop, ENat
Proof uses: UniversalEnvelopingAlgebra, Complex, TensorProduct, LeftInvariantDerivation
47 instances, coercions and auxiliary constants left out.
```
def Alg := UniversalEnvelopingAlgebra ℂ (ℂ ⊗[ℝ] LeftInvariantDerivation 𝓘(ℝ, E) G)
```
instance AutomorphicForm.GLn.(instance at line 210) line 210 source
instance AutomorphicForm.GLn.(instance at line 211) line 211 source
def AutomorphicForm.GLn.Z The centre of the universal enveloping algebra Alg G E line 214 source
Source documentation
The centre of the universal enveloping algebra Alg G E.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Group, NormedAddCommGroup, NormedSpace, Real, ChartedSpace, LieGroup, modelWithCornersSelf, Top.top, WithTop, ENat
Proof uses: Subtype, AutomorphicForm.GLn.Alg, Membership.mem, Subalgebra, Complex, Subalgebra.center
22 instances, coercions and auxiliary constants left out.
```
def Z : Type _ := Subalgebra.center ℂ (Alg G E)
```
Mentions: AutomorphicForm.GLn.Alg
instance AutomorphicForm.GLn.(instance at line 215) line 215 source
instance AutomorphicForm.GLn.(instance at line 216) line 216 source
instance AutomorphicForm.GLn.(instance at line 217) line 217 source
def AutomorphicForm.GLn.actionTensorCAlg'3 The ℂ-algebra map from the centre of the universal enveloping algebra to the endomorphism algebra of complex-valued smooth functions on G sorry line 221 source
Source documentation
The ℂ-algebra map from the centre of the universal enveloping algebra to the endomorphism algebra of complex-valued smooth functions on G.

depends on sorry what this means
Statement uses: TopologicalSpace, Group, NormedAddCommGroup, NormedSpace, Real, ChartedSpace, LieGroup, modelWithCornersSelf, Top.top, WithTop, ENat, AlgHom, Complex, AutomorphicForm.GLn.Z, Module.End, ContMDiffMap
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
80 instances, coercions and auxiliary constants left out.
```
def actionTensorCAlg'3 : Z G E →ₐ[ℂ] Module.End ℂ C^∞⟮𝓘(ℝ, E), G; 𝓘(ℝ, ℂ), ℂ⟯ := sorry
…
```
Mentions: AutomorphicForm.GLn.Z
structure AutomorphicForm.GLn.IsSmooth A function on GL_n(𝔸_f) × GL_n(ℝ) is smooth if it is continuous, locally constant in the finite-adelic variable, and C^∞ in the archimedean variable line 233 source
Source documentation
A function on GL_n(𝔸_f) × GL_n(ℝ) is smooth if it is continuous, locally constant in the finite-adelic variable, and C^∞ in the archimedean variable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Matrix.GeneralLinearGroup, Fin, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real, Complex
16 instances, coercions and auxiliary constants left out.
```
structure IsSmooth (f : GL (Fin n) (FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂ) : Prop where
…
```
abbrev AutomorphicForm.GLn.s An auxiliary "size" function on invertible real matrices used in the slowly increasing condition; namely tr(MMᵀ) + tr(M⁻¹(M⁻¹)ᵀ) line 244 source
Source documentation
An auxiliary "size" function on invertible real matrices used in the slowly increasing condition; namely tr(MMᵀ) + tr(M⁻¹(M⁻¹)ᵀ).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, Real
Proof uses: HAdd.hAdd, Matrix.trace, HMul.hMul, Matrix.transpose, Inv.inv
9 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev s (M : Matrix (Fin n) (Fin n) ℝ) : ℝ :=
…
```
structure AutomorphicForm.GLn.IsSlowlyIncreasing A function f : GL_n(ℝ) → ℂ is slowly increasing if there exist C, N such that ‖f M‖ ≤ C · s(M)^N for all M, where s is an auxiliary "size" function line 249 source
Source documentation
A function f : GL_n(ℝ) → ℂ is slowly increasing if there exist C, N such that ‖f M‖ ≤ C · s(M)^N for all M, where s is an auxiliary "size" function.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix.GeneralLinearGroup, Fin, Real, Complex
3 instances, coercions and auxiliary constants left out.
```
structure IsSlowlyIncreasing (f : GeneralLinearGroup (Fin n) ℝ → ℂ) : Prop where
…
```
structure AutomorphicForm.GLn.preweight A preweight for GLₙ is a continuous representation of the real orthogonal group O(n) on a finite-dimensional complex vector space line 256 source
Source documentation
A preweight for GLₙ is a continuous representation of the real orthogonal group O(n) on a finite-dimensional complex vector space.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
```
structure preweight (n : ℕ) where
…
```
def AutomorphicForm.GLn.preweight.fdRep The finite-dimensional ℂ-representation of O(n) associated to a preweight w line 266 source
Source documentation
The finite-dimensional ℂ-representation of O(n) associated to a preweight w.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, AutomorphicForm.GLn.preweight, FDRep, Complex, Subtype, Matrix, Fin, Real, Membership.mem, Submonoid, Matrix.orthogonalGroup
Proof uses: Action.mk, FGModuleCat, ModuleCat, ModuleCat.isFG, FGModuleCat.of, AutomorphicForm.GLn.preweight.d, MonoidHom.mk, CategoryTheory.End, OneHom.mk, FGModuleCat.ofHom, LinearMap.mk, RingHom.id, AddHom.mk, Matrix.mulVec, MonoidHom, Matrix.GeneralLinearGroup, AutomorphicForm.GLn.preweight.rho
61 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
noncomputable def preweight.fdRep (n : ℕ) (w : preweight n) :
    FDRep ℂ (orthogonalGroup (Fin n) ℝ) where
…
```
Mentions: AutomorphicForm.GLn.preweight
structure AutomorphicForm.GLn.Weight A weight for GLₙ: a preweight whose associated O(n)-representation is simple line 280 source
Source documentation
A weight for GLₙ: a preweight whose associated O(n)-representation is simple.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
```
structure Weight (n : ℕ) where
…
```
def AutomorphicForm.GLn._root_.RingHom.GL Functoriality of GLₘ: a ring homomorphism A →+* B induces a group homomorphism GLₘ(A) →* GLₘ(B) by applying it entrywise line 287 source
Source documentation
Functoriality of GLₘ: a ring homomorphism A →+* B induces a group homomorphism GLₘ(A) →* GLₘ(B) by applying it entrywise.
```
def _root_.RingHom.GL {A B : Type*} [CommRing A] [CommRing B] (φ : A →+* B)
  (m : Type*) [Fintype m] [DecidableEq m] :
  GL m A →* GL m B := Units.map <| (RingHom.mapMatrix φ).toMonoidHom
```
structure AutomorphicForm.GLn.IsConstantOn The function f : GL_n(𝔸_f) × GL_n(ℝ) → ℂ is right-U-invariant in the finite-adelic variable, where U is an open compact subgroup line 293 source
Source documentation
The function f : GL_n(𝔸_f) × GL_n(ℝ) → ℂ is right-U-invariant in the finite-adelic variable, where U is an open compact subgroup.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Subgroup, Matrix.GeneralLinearGroup, Fin, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Matrix, Prod, Real, Complex
19 instances, coercions and auxiliary constants left out.
```
structure IsConstantOn (U : Subgroup (GL (Fin n) (FiniteAdeleRing ℤ ℚ)))
  (f : (GL (Fin n) (FiniteAdeleRing ℤ ℚ)) × (GL (Fin n) ℝ) → ℂ) : Prop where
…
```
def AutomorphicForm.GLn.annihilator The annihilator of an element a : M in the module of R-linear maps M →ₗ[R] N: those f with f a = 0 line 302 source
Source documentation
The annihilator of an element a : M in the module of R-linear maps M →ₗ[R] N: those f with f a = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommSemiring, AddCommMonoid, Module, Submodule, LinearMap, RingHom.id
Proof uses: Submodule.compatibleMaps, Submodule.span, Singleton.singleton, Set, Bot.bot
13 instances, coercions and auxiliary constants left out.
```
def annihilator {R} [CommSemiring R]
    {M} [AddCommMonoid M] [Module R M]
    {N} [AddCommMonoid N] [Module R N]
    (a : M) : Submodule R (M →ₗ[R] N) :=
…
```
structure AutomorphicForm.GLn.AutomorphicFormForGLnOverQ Automorphic forms for GL_n/Q with weight ρ line 310 source
Source documentation
Automorphic forms for GL_n/Q with weight ρ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, AutomorphicForm.GLn.Weight
```
structure AutomorphicFormForGLnOverQ (n : ℕ) (ρ : Weight n) where
…
```
Mentions: AutomorphicForm.GLn.Weight
instance AutomorphicForm.GLn.AutomorphicFormForGLnOverQ.(instance at line 338) line 338 source