/-
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.LieDeriv
public import Mathlib.Algebra.Lie.OfAssociative
public import Mathlib.Algebra.Lie.UniversalEnveloping@[expose] public section
The enveloping algebra of 𝔤𝔩 n ℂ, its centre, and their action
The universal enveloping algebra U(𝔤𝔩 n ℂ) of the complexified Lie algebra of GL n ℝ and
the action of its centre on the complex-valued C^∞ functions on GL n ℝ by left invariant
differential operators. This is the action that condition (c) in the Borel-Jacquet definition
of an automorphic form refers to; 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:
universalEnveloping and centerUniversalEnveloping: U(𝔤𝔩 n ℂ) and its centre.
lieDerivHom, envelopingAction, centerAction: the action of 𝔤𝔩 n ℂ on smoothGL n
as a homomorphism of Lie algebras, its extension to U(𝔤𝔩 n ℂ) by the universal property,
and the restriction to the centre, which also makes smoothGL n a module over the centre.
constantsCharacter: the character by which the centre acts on the line of constant
functions; its kernel is an ideal of finite codimension annihilating the constants, which
gives condition (c) for constant automorphic forms.
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.GeneralLinearGroupvariable {n : Type*} [Fintype n] [DecidableEq n]-- `Matrix n n ℂ` is a Lie ring under the commutator; Mathlib keeps this instance local, since
-- it competes with the bracket of a Lie algebra given abstractly.
attribute [local instance 100] LieRing.ofAssociativeRing
The universal enveloping algebra U(𝔤𝔩 n ℂ) of the complexified Lie algebra of GL n ℝ.
The complexification of 𝔤𝔩 n ℝ is 𝔤𝔩 n ℂ = Matrix n n ℂ with its commutator bracket.
This abbreviation records the choice of LieRing.ofAssociativeRing as the bracket, so that
downstream files can name the algebra without re-enabling that local instance.
abbrev universalEnveloping (n : Type*) [Fintype n] [DecidableEq n] : Type _ :=
UniversalEnvelopingAlgebra ℂ (Matrix n n ℂ)
The centre of the universal enveloping algebra of the complexified Lie algebra of GL n ℝ.
This is the algebra acting in condition (c) in the definition of an automorphic form.
abbrev centerUniversalEnveloping (n : Type*) [Fintype n] [DecidableEq n] :
Subalgebra ℂ (universalEnveloping n) :=
Subalgebra.center ℂ (universalEnveloping n)
The action of 𝔤𝔩 n ℂ on the C^∞ functions on GL n ℝ by left invariant differential
operators, as a homomorphism of ℂ-Lie algebras.
noncomputable def lieDerivHom : Matrix n n ℂ →ₗ⁅ℂ⁆ Module.End ℂ (smoothGL n) where
toFun := lieDerivC
map_add' := lieDerivC_add
map_smul' := lieDerivC_smul
map_lie' {Z W} := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDerivC ⁅Z, W⁆ = ⁅lieDerivC Z, lieDerivC W⁆ All goals completed! 🐙
The action of the universal enveloping algebra U(𝔤𝔩 n ℂ) on the C^∞ functions on
GL n ℝ, obtained from lieDerivHom by the universal property. A monomial X₁ ⋯ Xₖ acts as
the composite of the corresponding left invariant derivatives.
noncomputable def envelopingAction :
universalEnveloping n →ₐ[ℂ] Module.End ℂ (smoothGL n) :=
UniversalEnvelopingAlgebra.lift ℂ lieDerivHom
The centre of the universal enveloping algebra acting on the C^∞ functions on GL n ℝ.
Restricting envelopingAction to the centre, this is the action condition (c) in the definition
of an automorphic form refers to.
noncomputable def centerAction :
↥(centerUniversalEnveloping n) →ₐ[ℂ] Module.End ℂ (smoothGL n) :=
envelopingAction.comp (centerUniversalEnveloping n).val
The C^∞ functions on GL n ℝ as a module over the centre of the universal enveloping
algebra, via left invariant differential operators.
noncomputable instance instModuleCenterSmoothGL :
Module ↥(centerUniversalEnveloping n) (smoothGL n) :=
Module.compHom (smoothGL n) (centerAction (n := n)).toRingHomlemma centerAction_smul (z : ↥(centerUniversalEnveloping n)) (φ : smoothGL n) :
z • φ = centerAction z φ := rflAll goals completed! 🐙All goals completed! 🐙Constant functions span an invariant line
Left invariant derivatives kill constants, so the enveloping algebra maps the line of constant
functions to itself, through the character constantsCharacter; its kernel is an ideal of
finite codimension annihilating the constants.
variable (n) in
The constant function 1 as an element of smoothGL n; the constant functions are the
line it spans.
def oneSmoothGL : smoothGL n := ⟨fun _ => 1, isSmoothOnGL_const 1⟩
An element of the line of constant functions is determined by its value at 1.
lemma eq_smul_oneSmoothGL_of_mem_span {φ : smoothGL n} (hφ : φ ∈ (ℂ ∙ oneSmoothGL n)) :
φ = (φ : GL n ℝ → ℂ) 1 • oneSmoothGL n := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:↥(smoothGL n)hφ:φ ∈ ℂ ∙ oneSmoothGL n⊢ φ = ↑φ 1 • oneSmoothGL n
n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq na:ℂhφ:a • oneSmoothGL n ∈ ℂ ∙ oneSmoothGL n⊢ a • oneSmoothGL n = ↑(a • oneSmoothGL n) 1 • oneSmoothGL n
All goals completed! 🐙
Left invariant differential operators map the constant functions to constant functions:
the generators lieDerivC X kill them.
n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nhsurj:Function.Surjective ⇑(UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ))X:Matrix n n ℂa:ℂhφ:a • oneSmoothGL n ∈ ℂ ∙ oneSmoothGL nhone:(lieDerivC X) (oneSmoothGL n) = 0⊢ (envelopingAction ((UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ)) ((TensorAlgebra.ι ℂ) X)))
(a • oneSmoothGL n) ∈
ℂ ∙ oneSmoothGL n
All goals completed! 🐙
n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nhsurj:Function.Surjective ⇑(UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ))a:TensorAlgebra ℂ (Matrix n n ℂ)b:TensorAlgebra ℂ (Matrix n n ℂ)ha:∀ φ ∈ ℂ ∙ oneSmoothGL n,
(envelopingAction ((UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ)) a)) φ ∈ ℂ ∙ oneSmoothGL nhb:∀ φ ∈ ℂ ∙ oneSmoothGL n,
(envelopingAction ((UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ)) b)) φ ∈ ℂ ∙ oneSmoothGL n⊢ ∀ φ ∈ ℂ ∙ oneSmoothGL n,
(envelopingAction ((UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ)) (a * b))) φ ∈ ℂ ∙ oneSmoothGL n
exact fun φ hφ => n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nhsurj:Function.Surjective ⇑(UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ))a:TensorAlgebra ℂ (Matrix n n ℂ)b:TensorAlgebra ℂ (Matrix n n ℂ)ha:∀ φ ∈ ℂ ∙ oneSmoothGL n,
(envelopingAction ((UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ)) a)) φ ∈ ℂ ∙ oneSmoothGL nhb:∀ φ ∈ ℂ ∙ oneSmoothGL n,
(envelopingAction ((UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ)) b)) φ ∈ ℂ ∙ oneSmoothGL nφ:↥(smoothGL n)hφ:φ ∈ ℂ ∙ oneSmoothGL n⊢ (envelopingAction ((UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ)) (a * b))) φ ∈ ℂ ∙ oneSmoothGL n All goals completed! 🐙
n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nhsurj:Function.Surjective ⇑(UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ))a:TensorAlgebra ℂ (Matrix n n ℂ)b:TensorAlgebra ℂ (Matrix n n ℂ)ha:∀ φ ∈ ℂ ∙ oneSmoothGL n,
(envelopingAction ((UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ)) a)) φ ∈ ℂ ∙ oneSmoothGL nhb:∀ φ ∈ ℂ ∙ oneSmoothGL n,
(envelopingAction ((UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ)) b)) φ ∈ ℂ ∙ oneSmoothGL n⊢ ∀ φ ∈ ℂ ∙ oneSmoothGL n,
(envelopingAction ((UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ)) (a + b))) φ ∈ ℂ ∙ oneSmoothGL n
exact fun φ hφ => n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nhsurj:Function.Surjective ⇑(UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ))a:TensorAlgebra ℂ (Matrix n n ℂ)b:TensorAlgebra ℂ (Matrix n n ℂ)ha:∀ φ ∈ ℂ ∙ oneSmoothGL n,
(envelopingAction ((UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ)) a)) φ ∈ ℂ ∙ oneSmoothGL nhb:∀ φ ∈ ℂ ∙ oneSmoothGL n,
(envelopingAction ((UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ)) b)) φ ∈ ℂ ∙ oneSmoothGL nφ:↥(smoothGL n)hφ:φ ∈ ℂ ∙ oneSmoothGL n⊢ (envelopingAction ((UniversalEnvelopingAlgebra.mkAlgHom ℂ (Matrix n n ℂ)) (a + b))) φ ∈ ℂ ∙ oneSmoothGL n All goals completed! 🐙n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nz:↥(centerUniversalEnveloping n)⊢ (centerAction z) (oneSmoothGL n) ∈ ℂ ∙ oneSmoothGL n
All goals completed! 🐙variable (n) in
The character by which the centre of the enveloping algebra acts on the constant
functions: z • 1 = constantsCharacter n z • 1. Its kernel is an ideal of finite codimension
annihilating the constants, which gives condition (c) for constant automorphic forms.
n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂ⊢ c • ↑(oneSmoothGL n) 1 = (algebraMap ℂ ℂ) c
All goals completed! 🐙end Matrix.GeneralLinearGroup