Modules over the universal enveloping algebra of a Lie algebra

This file contains some basics of the relationship between representations of a Lie algebra 𝓰 and modules over the universal enveloping algebra 𝓤 𝕜 𝓰.

Main definitions

As an auxiliary tool, we often need that any module M over a 𝕜-algebra A is a module over 𝕜. We need to be able to talk separately about left A-multiplication and left 𝕜-multiplication on M, and more crucially yet, we need to be able to talk separately about A-module maps and 𝕜-linear maps.

• ModuleOfModuleAlgebra: This is a type synonym of the A-module M equipped with the instance of a 𝕜-module.
• ModuleOfModuleAlgebra.lsmul: The left multiplication by an element a ∈ A defines a 𝕜-linear map M → M.
• centralSMulHom: The left multiplication by a central element z ∈ A defines an A-module map M → M.
• centralValueSubmodule: Given a central element z ∈ A and a scalar ζ ∈ 𝕜, this is the A-submodule of M consisting of vectors on which z acts as multiplication by ζ.

The correspondence between representations of a Lie algebra 𝓰 and modules over the universal enveloping algebra 𝓤 𝕜 𝓰 consists of two directions:

• UniversalEnvelopingAlgebra.representation: Any module V over 𝓤 𝕜 𝓰 gives rise to a representation 𝓰 → End(V) of the Lie algebra 𝓰 by restricting the module left multiplication to 𝓰 ⊆ 𝓤 𝕜 𝓰.
• LieAlgebra.Representation.moduleUniversalEnvelopingAlgebra: Any representation 𝓰 → End(V) of a Lie algebra 𝓰 over 𝕜 gives rise to a structure of a 𝓤 𝕜 𝓰-module on V in such a way that the representation defines the left multiplication by elements of 𝓰 ⊆ 𝓤 𝕜 𝓰.

Main statements

• UniversalEnvelopingAlgebra.induction: Induction principle for the universal enveloping algebra: In order to prove a property for all elements of the universal enveloping algebra 𝓤 𝕜 𝓰 of a Lie algebra 𝓰, it is enough to prove that (1): the property holds for scalars r ∈ 𝕜 ⊆ 𝓤 𝕜 𝓰, (2): the property holds for all Lie algebra elements X ∈ 𝓰 ⊆ 𝓤 𝕜 𝓰, (3): the property is preserved under multiplication, and (4): the property is preserved under addition.
• UniversalEnvelopingAlgebra.central_of_forall_lie_eq_zero: If Z ∈ 𝓰 has vanishing Lie bracket with all other elements of 𝓰, then it is a central element in the universal enveloping algebra 𝓤 𝕜 𝓰.

Notation

• 𝓤 is introduced as a notation for UniversalEnvelopingAlgebra.
• ιUEA is introduced as a notation for the inclusion 𝓰 → 𝓤 𝕜 𝓰 (a Lie algebra homomorphism) of a Lie algebra 𝓰 into its universal enveloping algebra 𝓤 𝕜 𝓰.

Tags

Lie algebra, universal enveloping algebra

theorem Algebra.scalar_smul_eq_smul_algebraMap_mul (𝕜 : Type u_1) (A : Type u_2) [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] (c : 𝕜) (a : A) : c • a = c • 1 * a

theorem Algebra.smul_scalar_smul_eq_smul_algebraMap_mul (𝕜 : Type u_1) (A : Type u_2) [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] (c : 𝕜) (a : A) : c • a = a * c • 1

@[reducible]

def moduleScalarOfModule (𝕜 : Type u_1) (A : Type u_2) [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] (V : Type u_3) [AddCommGroup V] [Module A V] : Module 𝕜 V

Any module over an algebra is a module over the scalars.

Equations

• moduleScalarOfModule 𝕜 A V = Module.compHom V (algebraMap 𝕜 A)

theorem moduleScalarOfModule.smul_def (𝕜 : Type u_1) (A : Type u_2) [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] (V : Type u_3) [AddCommGroup V] [Module A V] (r : 𝕜) (v : V) : SMul.smul r v = (algebraMap 𝕜 A) r • v

theorem isScalarTowerModuleScalarOfModule (𝕜 : Type u_1) (A : Type u_2) [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] (V : Type u_3) [AddCommGroup V] [Module A V] : IsScalarTower 𝕜 A V

When making any module over an algebra a module over the scalars, these form an IsScalarTower.

(The reason this is needed as a separate lemma is that the actual meaning of the scalar multiplication on representations of an algebra cannot be inferred by the type classes; this must be hand-crafted by moduleScalarOfModule .)

def ModuleOfModuleAlgebra (𝕜 : Type u_4) (A : Type u_5) (V : Type u_6) [CommRing 𝕜] [Semiring A] [algebra : Algebra 𝕜 A] [AddCommGroup V] [module : Module A V] : Type u_6

Type synonym of a module over an algebra, when it is to be viewed as a module over the scalars.

Equations

• ModuleOfModuleAlgebra 𝕜 A V = V

@[implicit_reducible]

instance instAddCommGroupModuleOfModuleAlgebra (𝕜 : Type u_1) (A : Type u_2) [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] (V : Type u_3) [AddCommGroup V] [Module A V] : AddCommGroup (ModuleOfModuleAlgebra 𝕜 A V)

Equations

• instAddCommGroupModuleOfModuleAlgebra 𝕜 A V = inst✝¹

@[implicit_reducible]

instance instModuleModuleOfModuleAlgebra (𝕜 : Type u_1) (A : Type u_2) [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] (V : Type u_3) [AddCommGroup V] [Module A V] : Module 𝕜 (ModuleOfModuleAlgebra 𝕜 A V)

Equations

• instModuleModuleOfModuleAlgebra 𝕜 A V = moduleScalarOfModule 𝕜 A V

def ModuleOfModuleAlgebra.mk (𝕜 : Type u_1) (A : Type u_2) [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] (V : Type u_3) [AddCommGroup V] [Module A V] (v : V) : ModuleOfModuleAlgebra 𝕜 A V

The map from V to its type synonym ModuleOfModuleAlgebra 𝕜 A V.

Equations

• ModuleOfModuleAlgebra.mk 𝕜 A V v = v

def ModuleOfModuleAlgebra.mkAddHom (𝕜 : Type u_1) (A : Type u_2) [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] (V : Type u_3) [AddCommGroup V] [Module A V] : V →+ ModuleOfModuleAlgebra 𝕜 A V

The map from V to its type synonym ModuleOfModuleAlgebra 𝕜 A V as a homomorphism of additive groups.

Equations

• ModuleOfModuleAlgebra.mkAddHom 𝕜 A V = { toFun := ModuleOfModuleAlgebra.mk 𝕜 A V, map_zero' := ⋯, map_add' := ⋯ }

def ModuleOfModuleAlgebra.unMk (𝕜 : Type u_1) (A : Type u_2) [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] (V : Type u_3) [AddCommGroup V] [Module A V] (v : ModuleOfModuleAlgebra 𝕜 A V) : V

The map from the type synonym ModuleOfModuleAlgebra 𝕜 A V back to V.

Equations

• ModuleOfModuleAlgebra.unMk 𝕜 A V v = v

def ModuleOfModuleAlgebra.unMkAddHom (𝕜 : Type u_4) (A : Type u_5) (V : Type u_6) [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] [AddCommGroup V] [Module A V] : ModuleOfModuleAlgebra 𝕜 A V →+ V

The map from the type synonym ModuleOfModuleAlgebra 𝕜 A V back to V as a homomorphism of additive groups.

Equations

• ModuleOfModuleAlgebra.unMkAddHom 𝕜 A V = { toFun := ModuleOfModuleAlgebra.unMk 𝕜 A V, map_zero' := ⋯, map_add' := ⋯ }

def ModuleOfModuleAlgebra.lsmul (𝕜 : Type u_1) [CommRing 𝕜] {A : Type u_2} [Semiring A] [Algebra 𝕜 A] (V : Type u_3) [AddCommGroup V] [Module A V] (a : A) : ModuleOfModuleAlgebra 𝕜 A V →ₗ[𝕜] ModuleOfModuleAlgebra 𝕜 A V

An element a ∈ A of a 𝕜-algebra A defines a 𝕜-linear map V → V by left multiplication.

Equations

• One or more equations did not get rendered due to their size.

theorem ModuleOfModuleAlgebra.lsmul_apply (𝕜 : Type u_1) [CommRing 𝕜] {A : Type u_2} [Semiring A] [Algebra 𝕜 A] (V : Type u_3) [AddCommGroup V] [Module A V] (a : A) (v : ModuleOfModuleAlgebra 𝕜 A V) : (lsmul 𝕜 V a) v = (mkAddHom 𝕜 A V) (a • (unMkAddHom 𝕜 A V) v)

def centralSMulHom {R : Type u_1} [Semiring R] {z : R} (z_central : ∀ (a : R), z * a = a * z) (M : Type u_2) [AddCommMonoid M] [Module R M] : M →ₗ[R] M

In a module M over a ring R, left multiplication by a central element z ∈ R is an R-linear map M → M.

Equations

• centralSMulHom z_central M = { toFun := ⇑((Module.toAddMonoidEnd R M) z), map_add' := ⋯, map_smul' := ⋯ }

theorem centralSMulHom_apply {R : Type u_1} [Semiring R] {z : R} (z_central : ∀ (a : R), Commute z a) (M : Type u_2) [AddCommMonoid M] [Module R M] (v : M) : (centralSMulHom z_central M) v = z • v

def centralValueSubmodule {𝕜 : Type u_2} {A : Type u_3} [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] (M : Type u_4) [AddCommGroup M] [Module 𝕜 M] [Module A M] [IsScalarTower 𝕜 A M] {z : A} (z_central : ∀ (a : A), Commute z a) (ζ : 𝕜) : Submodule A M

The set of vectors on which a given central element acts by a given scalar multiple as a submodule.

Equations

• centralValueSubmodule M z_central ζ = (centralSMulHom z_central M - ζ • LinearMap.id).ker

theorem mem_centralValueSubmodule_iff {𝕜 : Type u_2} {A : Type u_3} [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] (M : Type u_4) [AddCommGroup M] [Module 𝕜 M] [Module A M] [IsScalarTower 𝕜 A M] {z : A} (z_central : ∀ (a : A), Commute z a) (ζ : 𝕜) (v : M) : v ∈ centralValueSubmodule M z_central ζ ↔ z • v = ζ • v

The defining property of centralValueSubmodule is the eigenvalue property for the central element action.

theorem smul_eq_scalar_smul_of_central_of_mem_span {𝕜 : Type u_2} {A : Type u_3} [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] (M : Type u_4) [AddCommGroup M] [Module 𝕜 M] [Module A M] [IsScalarTower 𝕜 A M] {z : A} (z_central : ∀ (a : A), Commute z a) {u : M} {ζ : 𝕜} (hzu : z • u = ζ • u) {v : M} (hv : v ∈ A ∙ u) : z • v = ζ • v

theorem smul_eq_scalar_smul_of_central {𝕜 : Type u_2} {A : Type u_3} [CommRing 𝕜] [Semiring A] [Algebra 𝕜 A] (M : Type u_4) [AddCommGroup M] [Module 𝕜 M] [Module A M] [IsScalarTower 𝕜 A M] {z : A} (z_central : ∀ (a : A), Commute z a) {u : M} {ζ : 𝕜} (hau : z • u = ζ • u) {v : M} (v_cyclic : A ∙ u = ⊤) : z • v = ζ • v

@[reducible, inline]

abbrev 𝓤 (R : Type u_3) (L : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] : Type (max u_3 u_4)

The universal enveloping algebra of a Lie algebra.

Equations

• 𝓤 = UniversalEnvelopingAlgebra

@[reducible, inline]

abbrev ιUEA (R : Type u_3) {L : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] : L →ₗ⁅R⁆ UniversalEnvelopingAlgebra R L

The natural Lie algebra morphism from a Lie algebra to its universal enveloping algebra.

Equations

• ιUEA = UniversalEnvelopingAlgebra.ι

theorem UniversalEnvelopingAlgebra.mkAlgHom_range_eq_top (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 : Type u_2) [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] : (mkAlgHom 𝕜 𝓰).range = ⊤

theorem UniversalEnvelopingAlgebra.mkAlgHom_surjective {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 : Type u_2} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] : Function.Surjective ⇑(mkAlgHom 𝕜 𝓰)

theorem UniversalEnvelopingAlgebra.induction (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 : Type u_2) [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] (C : 𝓤 𝕜 𝓰 → Prop) (hAM : ∀ (r : 𝕜), C ((algebraMap 𝕜 (𝓤 𝕜 𝓰)) r)) (hι : ∀ (X : 𝓰), C ((ιUEA 𝕜) X)) (hMul : ∀ (a b : 𝓤 𝕜 𝓰), C a → C b → C (a * b)) (hAdd : ∀ (a b : 𝓤 𝕜 𝓰), C a → C b → C (a + b)) (a : 𝓤 𝕜 𝓰) : C a

theorem UniversalEnvelopingAlgebra.central_of_forall_lie_eq_zero (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 : Type u_2) [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {Z : 𝓰} (hZ : ∀ (X : 𝓰), ⁅Z, X⁆ = 0) (a : 𝓤 𝕜 𝓰) : Commute ((ιUEA 𝕜) Z) a

theorem UniversalEnvelopingAlgebra.smul_eq_of_cyclic_of_forall_lie_eq_zero (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 : Type u_2) [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {Z : 𝓰} {ζ : 𝕜} (hZ : ∀ (X : 𝓰), ⁅Z, X⁆ = 0) {V : Type u_3} [AddCommGroup V] [Module (𝓤 𝕜 𝓰) V] {w : V} (w_cyclic : 𝓤 𝕜 𝓰 ∙ w = ⊤) (hw : (ιUEA 𝕜) Z • w = (algebraMap 𝕜 (𝓤 𝕜 𝓰)) ζ • w) (v : V) : (ιUEA 𝕜) Z • v = (algebraMap 𝕜 (𝓤 𝕜 𝓰)) ζ • v

If a central element of a Lie algebra acts as a scalar multiplication on a cyclic vector in a representation, then it acts as the same scalar on the whole representation.

def UniversalEnvelopingAlgebra.representation (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 : Type u_2) [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {V : Type u_3} [AddCommGroup V] [Module (𝓤 𝕜 𝓰) V] : LieAlgebra.Representation 𝕜 𝕜 𝓰 (ModuleOfModuleAlgebra 𝕜 (𝓤 𝕜 𝓰) V)

Any module V over the universal enveloping algebra of a Lie algebra is a representation of the Lie algebra.

This is recorded on the type synonym ModuleOfModuleAlgebra 𝕜 (𝓤 𝕜 𝓰) V of V, in order to make the V a 𝕜-module and talk about a representation of a 𝕜-Lie algebra on it.

Equations

• UniversalEnvelopingAlgebra.representation 𝕜 𝓰 = { toFun := fun (X : 𝓰) => ModuleOfModuleAlgebra.lsmul 𝕜 V ((ιUEA 𝕜) X), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[reducible]

noncomputable def LieAlgebra.Representation.moduleUniversalEnvelopingAlgebra {𝕜 : Type u_3} {𝕂 : Type u_4} [CommRing 𝕜] [CommRing 𝕂] {𝓰 : Type u_5} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {V : Type u_6} [AddCommGroup V] [Module 𝕂 V] [Module 𝕜 V] [SMul 𝕜 𝕂] [IsScalarTower 𝕜 𝕂 V] [SMulCommClass 𝕂 𝕜 V] (ρ : Representation 𝕜 𝕂 𝓰 V) : Module (𝓤 𝕜 𝓰) V

A representation of a 𝕜-Lie algebra 𝓰 on a vector space V defines a 𝓤 𝕜 𝓰-module structure on V.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LieAlgebra.Representation.moduleUniversalEnvelopingAlgebra_smul_eq {𝕜 : Type u_3} {𝕂 : Type u_4} [CommRing 𝕜] [CommRing 𝕂] {𝓰 : Type u_5} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {V : Type u_6} [AddCommGroup V] [Module 𝕂 V] [Module 𝕜 V] [SMul 𝕜 𝕂] [IsScalarTower 𝕜 𝕂 V] [SMulCommClass 𝕂 𝕜 V] (ρ : Representation 𝕜 𝕂 𝓰 V) (a : 𝓤 𝕜 𝓰) (v : V) : SMul.smul a v = (((UniversalEnvelopingAlgebra.lift 𝕜) ρ) a) v

theorem LieAlgebra.Representation.moduleUniversalEnvelopingAlgebra_ιUEA_smul_eq {𝕜 : Type u_3} {𝕂 : Type u_4} [CommRing 𝕜] [CommRing 𝕂] {𝓰 : Type u_5} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {V : Type u_6} [AddCommGroup V] [Module 𝕂 V] [Module 𝕜 V] [SMul 𝕜 𝕂] [IsScalarTower 𝕜 𝕂 V] [SMulCommClass 𝕂 𝕜 V] (ρ : Representation 𝕜 𝕂 𝓰 V) (X : 𝓰) (v : V) : SMul.smul ((ιUEA 𝕜) X) v = (ρ X) v

The defining property of the 𝓤 𝕜 𝓰-module structure on a representation V of a 𝕜-Lie algebra 𝓰.