Verma modules for Lie algebras with triangular decomposition

This file defines Verma modules used in Lie algebra representation theory.

Main definitions

• TriangularDecomposition: A triangular decomposition of a Lie algebra (typically to a commutative Cartan subalgebra and two nilpotent subalgebras, but these requirements are not bundled in the definition).
• TriangularDecomposition.ofBasis: The triangular decomposition of a Lie algebra 𝓰 associated with a tri-partition of a given basis of 𝓰.
• TriangularDecomposition.weight: A weight of a Lie algebra 𝓰 with triangular decomposition is a linear functional on the Cartan subalgebra 𝓱 ⊆ 𝓰.
• TriangularDecomposition.VermaHW η: The Verma module of highest weight η for a Lie algebra 𝓰 with a triangular decomposition.
• TriangularDecomposition.VermaHW.hwVec: The highest weight vector of the Verma module.
• TriangularDecomposition.VermaHW.universalMap: The universal property of the Verma module: Given another module M over 𝓤 𝕜 𝓰 and a "target" vector hwv ∈ M satisfying E • hwv = 0 for all E in the positive part of the triangular decomposition and H • hwv = η(H) • hwv for all H in the Cartan subalgebra, one obtains an A-module map from the Verma module to M uniquely specified by the requirement hwVec η ↦ hwv.

Main statements

• TriangularDecomposition.instModule𝓤VermaHW and TriangularDecomposition.instModuleVermaHW: A Verma module of a Lie algebra 𝓰 is a module over the universal enveloping algebra 𝓤 𝕜 𝓰 and a vector space over 𝕜.
• TriangularDecomposition.VermaHW.hwVec_cyclic: The Verma module is generated by its highest weight vector.
• TriangularDecomposition.VermaHW.cartan_smul_hwVec: The highest weight vector of a Verma module is an eigenvector of the Cartan subalgebra with the eigenvalues specified by the highest weight.
• TriangularDecomposition.VermaHW.upper_smul_hwVec: The highest weight vector of a Verma module is annihilated by the positive part of the triangular decomposition.
• VermaModule.range_universalMap_eq_span: The map guaranteed by the universal property of the Verma module is surjective onto the submodule generated by the "target" vector.

Implementation notes

Verma modules over Lie algebras are defined as a special case of generalized Verma module for algebras (see the file VermaModule.lean).

Tags

Verma module, Lie algebra, representation

structure VirasoroProject.TriangularDecomposition (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 : Type u_2) [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] : Type u_2

A triangular decomposition of a Lie algebra (without assumptions of commutativity of the Cartan subalgebra or nilpotency of the other parts bundled, yet).

• part : SignType → Submodule 𝕜 𝓰
• directSum : DirectSum.IsInternal self.part

def VirasoroProject.TriangularDecomposition.ofBasis {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {ι : Type u_3} [Nontrivial 𝕜] [NoZeroSMulDivisors 𝕜 𝓰] (B : Module.Basis ι 𝕜 𝓰) (Bp : SignType → Set ι) (Bp_disj : Pairwise fun (ε₁ ε₂ : SignType) => Disjoint (Bp ε₁) (Bp ε₂)) (Bp_cover : ⋃ (ε : SignType), Bp ε = Set.univ) : TriangularDecomposition 𝕜 𝓰

Equations

• VirasoroProject.TriangularDecomposition.ofBasis B Bp Bp_disj Bp_cover = { part := fun (ε : SignType) => Submodule.span 𝕜 (⇑B '' Bp ε), directSum := ⋯ }

noncomputable def VirasoroProject.TriangularDecomposition.ofBasis.basis_part {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {ι : Type u_3} [Nontrivial 𝕜] [NoZeroSMulDivisors 𝕜 𝓰] (B : Module.Basis ι 𝕜 𝓰) (Bp : SignType → Set ι) (Bp_disj : Pairwise fun (ε₁ ε₂ : SignType) => Disjoint (Bp ε₁) (Bp ε₂)) (Bp_cover : ⋃ (ε : SignType), Bp ε = Set.univ) (ε : SignType) : Module.Basis (↑(Bp ε)) 𝕜 ↥((ofBasis B Bp Bp_disj Bp_cover).part ε)

The parts of a triangular decomposition determined by a basis have natural bases by construction.

Equations

• VirasoroProject.TriangularDecomposition.ofBasis.basis_part B Bp Bp_disj Bp_cover ε = B.basis_submodule_span (Bp ε)

@[reducible, inline]

abbrev VirasoroProject.TriangularDecomposition.cartan {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] (tri : TriangularDecomposition 𝕜 𝓰) : Submodule 𝕜 𝓰

The Cartan subalgebra of a given triangular decomposition of a Lie algebra.

Equations

• tri.cartan = tri.part 0

@[reducible, inline]

abbrev VirasoroProject.TriangularDecomposition.upper {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] (tri : TriangularDecomposition 𝕜 𝓰) : Submodule 𝕜 𝓰

Equations

• tri.upper = tri.part 1

@[reducible, inline]

abbrev VirasoroProject.TriangularDecomposition.lower {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] (tri : TriangularDecomposition 𝕜 𝓰) : Submodule 𝕜 𝓰

Equations

• tri.lower = tri.part (-1)

@[reducible, inline]

abbrev VirasoroProject.TriangularDecomposition.weight {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] (tri : TriangularDecomposition 𝕜 𝓰) : Type (max u_2 u_1)

Weights of a Lie algebra with triangular decomposition are functionals on the Cartan subalgebra.

Equations

• tri.weight = (↥tri.cartan →ₗ[𝕜] 𝕜)

noncomputable def VirasoroProject.TriangularDecomposition.weightHW {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {tri : TriangularDecomposition 𝕜 𝓰} (η : tri.weight) (i : ↥tri.cartan ⊕ ↥tri.upper) : 𝓤 𝕜 𝓰 × 𝕜

The data associated to a weight for the purpose of constructing a highest weight representation.

Equations

• VirasoroProject.TriangularDecomposition.weightHW η (Sum.inl H) = ((ιUEA 𝕜) ↑H, η H)
• VirasoroProject.TriangularDecomposition.weightHW η (Sum.inr E) = ((ιUEA 𝕜) ↑E, 0)

def VirasoroProject.TriangularDecomposition.VermaHW {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {tri : TriangularDecomposition 𝕜 𝓰} (η : tri.weight) : Type (max u_2 u_1)

The Verma module of highest weight η.

Equations

• VirasoroProject.TriangularDecomposition.VermaHW η = VirasoroProject.VermaModule (VirasoroProject.TriangularDecomposition.weightHW η)

noncomputable def VirasoroProject.TriangularDecomposition.VermaHW.hwVec {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {tri : TriangularDecomposition 𝕜 𝓰} (η : tri.weight) : VermaHW η

The highest weight vector of the Verma module of highest weight η.

Equations

• VirasoroProject.TriangularDecomposition.VermaHW.hwVec η = VirasoroProject.VermaModule.hwVec (VirasoroProject.TriangularDecomposition.weightHW η)

noncomputable instance VirasoroProject.TriangularDecomposition.instAddCommGroupVermaHW {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {tri : TriangularDecomposition 𝕜 𝓰} (η : tri.weight) : AddCommGroup (VermaHW η)

Equations

• VirasoroProject.TriangularDecomposition.instAddCommGroupVermaHW η = VirasoroProject.instAddCommGroupVermaModule (VirasoroProject.TriangularDecomposition.weightHW η)

noncomputable instance VirasoroProject.TriangularDecomposition.instModule𝓤VermaHW {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {tri : TriangularDecomposition 𝕜 𝓰} (η : tri.weight) : Module (𝓤 𝕜 𝓰) (VermaHW η)

Equations

• VirasoroProject.TriangularDecomposition.instModule𝓤VermaHW η = VirasoroProject.instModuleVermaModule (VirasoroProject.TriangularDecomposition.weightHW η)

noncomputable instance VirasoroProject.TriangularDecomposition.instModuleVermaHW {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {tri : TriangularDecomposition 𝕜 𝓰} (η : tri.weight) : Module 𝕜 (VermaHW η)

Equations

• VirasoroProject.TriangularDecomposition.instModuleVermaHW η = moduleScalarOfModule 𝕜 (𝓤 𝕜 𝓰) (VirasoroProject.TriangularDecomposition.VermaHW η)

instance VirasoroProject.TriangularDecomposition.instIsScalarTower𝓤VermaHW {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {tri : TriangularDecomposition 𝕜 𝓰} (η : tri.weight) : IsScalarTower 𝕜 (𝓤 𝕜 𝓰) (VermaHW η)

theorem VirasoroProject.TriangularDecomposition.VermaHW.smul_eq_algebraHom_smul {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {tri : TriangularDecomposition 𝕜 𝓰} {η : tri.weight} (r : 𝕜) (v : VermaHW η) : r • v = (algebraMap 𝕜 (𝓤 𝕜 𝓰)) r • v

instance VirasoroProject.TriangularDecomposition.instSMulCommClass𝓤VermaHW {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {tri : TriangularDecomposition 𝕜 𝓰} (η : tri.weight) : SMulCommClass 𝕜 (𝓤 𝕜 𝓰) (VermaHW η)

theorem VirasoroProject.TriangularDecomposition.VermaHW.hwVec_cyclic {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {tri : TriangularDecomposition 𝕜 𝓰} (η : tri.weight) : Submodule.span (𝓤 𝕜 𝓰) {hwVec η} = ⊤

theorem VirasoroProject.TriangularDecomposition.VermaHW.upper_smul_hwVec {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {tri : TriangularDecomposition 𝕜 𝓰} (η : tri.weight) {E : 𝓰} (hE : E ∈ tri.upper) : (ιUEA 𝕜) E • hwVec η = 0

theorem VirasoroProject.TriangularDecomposition.VermaHW.cartan_smul_hwVec {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {tri : TriangularDecomposition 𝕜 𝓰} (η : tri.weight) {H : 𝓰} (hH : H ∈ tri.cartan) : (ιUEA 𝕜) H • hwVec η = η ⟨H, hH⟩ • hwVec η

noncomputable def VirasoroProject.TriangularDecomposition.VermaHW.universalMap {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {tri : TriangularDecomposition 𝕜 𝓰} (η : tri.weight) (M : Type u_3) [AddCommGroup M] [Module (𝓤 𝕜 𝓰) M] {hwv : M} (hwv_cartan : ∀ {H : 𝓰} (hH : H ∈ tri.cartan), (ιUEA 𝕜) H • hwv = (algebraMap 𝕜 (𝓤 𝕜 𝓰)) (η ⟨H, hH⟩) • hwv) (hwv_upper : ∀ {E : 𝓰}, E ∈ tri.upper → (ιUEA 𝕜) E • hwv = 0) : VermaHW η →ₗ[𝓤 𝕜 𝓰] M

Equations

• VirasoroProject.TriangularDecomposition.VermaHW.universalMap η M hwv_cartan hwv_upper = VirasoroProject.VermaModule.universalMap (VirasoroProject.TriangularDecomposition.weightHW η) ⋯

theorem VirasoroProject.TriangularDecomposition.VermaHW.universalMap_hwVec {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {tri : TriangularDecomposition 𝕜 𝓰} (η : tri.weight) (M : Type u_3) [AddCommGroup M] [Module (𝓤 𝕜 𝓰) M] {hwv : M} (hwv_cartan : ∀ {H : 𝓰} (hH : H ∈ tri.cartan), (ιUEA 𝕜) H • hwv = (algebraMap 𝕜 (𝓤 𝕜 𝓰)) (η ⟨H, hH⟩) • hwv) (hwv_upper : ∀ {E : 𝓰}, E ∈ tri.upper → (ιUEA 𝕜) E • hwv = 0) : (universalMap η M ⋯ ⋯) (hwVec η) = hwv

class VirasoroProject.HasCentralValue (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 : Type u_2) [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] (M : Type u_3) [AddCommGroup M] [Module 𝕜 M] [Module (𝓤 𝕜 𝓰) M] (C : 𝓰) (c : 𝕜) : Prop

A type class for recording that a (central) element acts as a particular scalar on a representation.

• central_smul' (v : M) : (ιUEA 𝕜) C • v = c • v

@[simp]

theorem VirasoroProject.HasCentralValue.central_smul (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 : Type u_2) [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] (M : Type u_3) [AddCommGroup M] [Module 𝕜 M] [Module (𝓤 𝕜 𝓰) M] {C : 𝓰} {c : 𝕜} [HasCentralValue 𝕜 𝓰 M C c] (v : M) : (ιUEA 𝕜) C • v = c • v