CenterAction.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 10 curated AI-written annotations and 7190 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, Formal Conjectures paper, arXiv v1

14 declarations, 0 contain sorry, 0 declared as axioms

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.

Imports (3)

Imported by 2 files

abbrev Matrix.GeneralLinearGroup.universalEnveloping The universal enveloping algebra U(𝔤𝔩 n ℂ) of the complexified Lie algebra of GL n ℝ line 65 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq
Proof uses: UniversalEnvelopingAlgebra, Complex, Matrix, LieRing.ofAssociativeRing
8 instances, coercions and auxiliary constants left out.
```
abbrev universalEnveloping (n : Type*) [Fintype n] [DecidableEq n] : Type _ :=
…
```
abbrev Matrix.GeneralLinearGroup.centerUniversalEnveloping The centre of the universal enveloping algebra of the complexified Lie algebra of GL n ℝ line 70 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Subalgebra, Complex, Matrix.GeneralLinearGroup.universalEnveloping, Matrix, LieRing.ofAssociativeRing
Proof uses: Subalgebra.center
22 instances, coercions and auxiliary constants left out.
```
abbrev centerUniversalEnveloping (n : Type*) [Fintype n] [DecidableEq n] :
    Subalgebra ℂ (universalEnveloping n) :=
…
```
Mentions: Matrix.GeneralLinearGroup.universalEnveloping
def Matrix.GeneralLinearGroup.lieDerivHom The action of 𝔤𝔩 n ℂ on the C^∞ functions on GL n ℝ by left invariant differential operators, as a homomorphism of ℂ-Lie algebras line 76 source
Source documentation
The action of 𝔤𝔩 n ℂ on the C^∞ functions on GL n ℝ by left invariant differential operators, as a homomorphism of ℂ-Lie algebras.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, LieHom, Complex, Matrix, Module.End, Subtype, Matrix.GeneralLinearGroup, Real, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, LieRing.ofAssociativeRing
Proof uses: LieHom.mk, LinearMap.mk, RingHom.id, AddHom.mk, Matrix.GeneralLinearGroup.lieDerivC, Matrix.GeneralLinearGroup.lieDerivC_add, Matrix.GeneralLinearGroup.lieDerivC_smul
84 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def lieDerivHom : Matrix n n ℂ →ₗ⁅ℂ⁆ Module.End ℂ (smoothGL n) where
…
```
Mentions: Matrix.GeneralLinearGroup.smoothGL
def Matrix.GeneralLinearGroup.envelopingAction The action of the universal enveloping algebra U(𝔤𝔩 n ℂ) on the C^∞ functions on GL n ℝ, obtained from lieDerivHom by the universal property line 85 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, AlgHom, Complex, Matrix.GeneralLinearGroup.universalEnveloping, Module.End, Subtype, Matrix.GeneralLinearGroup, Real, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, Matrix, LieRing.ofAssociativeRing
Proof uses: Equiv, LieHom, UniversalEnvelopingAlgebra, UniversalEnvelopingAlgebra.lift, Matrix.GeneralLinearGroup.lieDerivHom
79 instances, coercions and auxiliary constants left out.
```
noncomputable def envelopingAction :
    universalEnveloping n →ₐ[ℂ] Module.End ℂ (smoothGL n) :=
…
```
Mentions: Matrix.GeneralLinearGroup.universalEnveloping, Matrix.GeneralLinearGroup.smoothGL
def Matrix.GeneralLinearGroup.centerAction The centre of the universal enveloping algebra acting on the C^∞ functions on GL n ℝ line 92 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, AlgHom, Complex, Subtype, Matrix.GeneralLinearGroup.universalEnveloping, Membership.mem, Subalgebra, Matrix, LieRing.ofAssociativeRing, Matrix.GeneralLinearGroup.centerUniversalEnveloping, Module.End, Matrix.GeneralLinearGroup, Real, Submodule, Matrix.GeneralLinearGroup.smoothGL
Proof uses: AlgHom.comp, Matrix.GeneralLinearGroup.envelopingAction, Subalgebra.val
80 instances, coercions and auxiliary constants left out.
```
noncomputable def centerAction :
    ↥(centerUniversalEnveloping n) →ₐ[ℂ] Module.End ℂ (smoothGL n) :=
…
```
Mentions: Matrix.GeneralLinearGroup.centerUniversalEnveloping, Matrix.GeneralLinearGroup.smoothGL
instance Matrix.GeneralLinearGroup.instModuleCenterSmoothGL The C^∞ functions on GL n ℝ as a module over the centre of the universal enveloping algebra, via left invariant differential operators line 98 source
Source documentation
The C^∞ functions on GL n ℝ as a module over the centre of the universal enveloping algebra, via left invariant differential operators.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Module, Subtype, Matrix.GeneralLinearGroup.universalEnveloping, Membership.mem, Subalgebra, Complex, Matrix, LieRing.ofAssociativeRing, Matrix.GeneralLinearGroup.centerUniversalEnveloping, Matrix.GeneralLinearGroup, Real, Submodule, Matrix.GeneralLinearGroup.smoothGL
Proof uses: Module.compHom, Module.End, AlgHom.toRingHom, Matrix.GeneralLinearGroup.centerAction
53 instances, coercions and auxiliary constants left out.
```
noncomputable instance instModuleCenterSmoothGL :
    Module ↥(centerUniversalEnveloping n) (smoothGL n) :=
…
```
Mentions: Matrix.GeneralLinearGroup.centerUniversalEnveloping, Matrix.GeneralLinearGroup.smoothGL
lemma Matrix.GeneralLinearGroup.centerAction_smul line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Subtype, Matrix.GeneralLinearGroup.universalEnveloping, Membership.mem, Subalgebra, Complex, Matrix, LieRing.ofAssociativeRing, Matrix.GeneralLinearGroup.centerUniversalEnveloping, Matrix.GeneralLinearGroup, Real, Submodule, Matrix.GeneralLinearGroup.smoothGL, Eq, HSMul.hSMul, Module.End, RingHom.id, AlgHom, Matrix.GeneralLinearGroup.centerAction
Proof uses: rfl
100 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance Matrix.GeneralLinearGroup.(instance at line 105) line 105 source
instance Matrix.GeneralLinearGroup.(instance at line 108) line 108 source
def Matrix.GeneralLinearGroup.oneSmoothGL The constant function 1 as an element of smoothGL n; the constant functions are the line it spans line 123 source
Source documentation
The constant function 1 as an element of smoothGL n; the constant functions are the line it spans.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Subtype, Matrix.GeneralLinearGroup, Real, Complex, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL
Proof uses: Subtype.mk, OfNat.ofNat
19 instances, coercions and auxiliary constants left out.
```
def oneSmoothGL : smoothGL n := ⟨fun _ => 1, isSmoothOnGL_const 1⟩
```
Mentions: Matrix.GeneralLinearGroup.smoothGL, Matrix.GeneralLinearGroup.isSmoothOnGL_const
lemma Matrix.GeneralLinearGroup.eq_smul_oneSmoothGL_of_mem_span An element of the line of constant functions is determined by its value at 1 line 126 source
Source documentation
An element of the line of constant functions is determined by its value at 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Subtype, Matrix.GeneralLinearGroup, Real, Complex, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, Submodule.span, Singleton.singleton, Set, Matrix.GeneralLinearGroup.oneSmoothGL, Eq, HSMul.hSMul, OfNat.ofNat, Matrix
Proof uses: Exists, Iff.mp, Submodule.mem_span_singleton, of_eq_true, Subtype.mk, Eq.trans, True, congrArg, congrFun', mul_one, eq_self
74 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma eq_smul_oneSmoothGL_of_mem_span {φ : smoothGL n} (hφ : φ ∈ (ℂ ∙ oneSmoothGL n)) :
    φ = (φ : GL n ℝ → ℂ) 1 • oneSmoothGL n := by
…
```
Mentions: Matrix.GeneralLinearGroup.smoothGL, Matrix.GeneralLinearGroup.oneSmoothGL
lemma Matrix.GeneralLinearGroup.envelopingAction_mem_span_oneSmoothGL Left invariant differential operators map the constant functions to constant functions: the generators lieDerivC X kill them line 133 source
Source documentation
Left invariant differential operators map the constant functions to constant functions: the generators lieDerivC X kill them.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup.universalEnveloping, Subtype, Matrix.GeneralLinearGroup, Real, Complex, Membership.mem, Submodule, Matrix.GeneralLinearGroup.smoothGL, Submodule.span, Singleton.singleton, Set, Matrix.GeneralLinearGroup.oneSmoothGL, Module.End, RingHom.id, AlgHom, Matrix, LieRing.ofAssociativeRing, Matrix.GeneralLinearGroup.envelopingAction
Proof uses: Function.Surjective, TensorAlgebra, UniversalEnvelopingAlgebra, UniversalEnvelopingAlgebra.mkAlgHom, RingCon.mkₐ_surjective, UniversalEnvelopingAlgebra.ringCon, Eq, Exists, TensorAlgebra.induction, Eq.mpr, RingHom, Algebra.algebraMap, HSMul.hSMul, id, congrArg, congrFun', Eq.trans, AlgHom.commutes, Submodule.smul_mem, LinearMap and 31 more
170 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma envelopingAction_mem_span_oneSmoothGL (u : universalEnveloping n) :
    ∀ φ ∈ (ℂ ∙ oneSmoothGL n), envelopingAction u φ ∈ (ℂ ∙ oneSmoothGL n) := by
…
```
Mentions: Matrix.GeneralLinearGroup.universalEnveloping, Matrix.GeneralLinearGroup.oneSmoothGL, Matrix.GeneralLinearGroup.envelopingAction
lemma Matrix.GeneralLinearGroup.smul_oneSmoothGL_mem_span line 154 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Subtype, Matrix.GeneralLinearGroup.universalEnveloping, Membership.mem, Subalgebra, Complex, Matrix, LieRing.ofAssociativeRing, Matrix.GeneralLinearGroup.centerUniversalEnveloping, Matrix.GeneralLinearGroup, Real, Submodule, Matrix.GeneralLinearGroup.smoothGL, Submodule.span, Singleton.singleton, Set, Matrix.GeneralLinearGroup.oneSmoothGL, HSMul.hSMul
Proof uses: Eq.mpr, Module.End, RingHom.id, AlgHom, Matrix.GeneralLinearGroup.centerAction, id, Eq, congrArg, Matrix.GeneralLinearGroup.centerAction_smul, Matrix.GeneralLinearGroup.envelopingAction_mem_span_oneSmoothGL, Submodule.mem_span_singleton_self
104 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Matrix.GeneralLinearGroup.constantsCharacter The character by which the centre of the enveloping algebra acts on the constant functions: z • 1 = constantsCharacter n z • 1 line 164 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, AlgHom, Complex, Subtype, Matrix.GeneralLinearGroup.universalEnveloping, Membership.mem, Subalgebra, Matrix, LieRing.ofAssociativeRing, Matrix.GeneralLinearGroup.centerUniversalEnveloping
Proof uses: AlgHom.mk, RingHom.mk, MonoidHom.mk, OneHom.mk, Matrix.GeneralLinearGroup, Real, Submodule, Matrix.GeneralLinearGroup.smoothGL, HSMul.hSMul, Matrix.GeneralLinearGroup.oneSmoothGL, OfNat.ofNat
69 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
noncomputable def constantsCharacter : ↥(centerUniversalEnveloping n) →ₐ[ℂ] ℂ where
…
```
Mentions: Matrix.GeneralLinearGroup.centerUniversalEnveloping

FormalConjecturesForMathlib/NumberTheory/AutomorphicForm/BorelJacquet/CenterAction.lean

The enveloping algebra of 𝔤𝔩 n ℂ, its centre, and their action

Main declarations

`FormalConjecturesForMathlib/NumberTheory/AutomorphicForm/BorelJacquet/CenterAction.lean`

The enveloping algebra of `𝔤𝔩 n ℂ`, its centre, and their action