The enveloping-algebra dictionary for Lie modules

A module over a Lie algebra L is the same data as a module over its universal enveloping algebra U(L). This file makes that dictionary explicit and, more importantly, extends it to the structures built on top of a module: Lie submodules are exactly U(L)-submodules, and Lie module homomorphisms are exactly U(L)-linear maps.

The two translations of the underlying data are immediate from Mathlib. In one direction the representation Ado.UniversalEnvelopingAlgebra.representation supplies a U(L)-module structure by restriction of scalars. In the other direction LieRingModule.compLieHom composes the canonical Lie map UniversalEnvelopingAlgebra.ι with the commutator action of an associative algebra on a module over it.

The dictionary for submodules and homomorphisms is not immediate: it rests on U(L) being generated as an R-algebra by the canonical Lie generators (Ado.UniversalEnvelopingAlgebra.induction_ι), so that an R-submodule stable under the bracket is automatically stable under all of U(L), and likewise an R-linear map commuting with the bracket is U(L)-linear. Everything here is therefore available over an arbitrary commutative ring, with no Poincaré--Birkhoff--Witt hypothesis.

The dictionary is stated for an arbitrary U(L)-module structure compatible with the bracket (the hypothesis hcompat : ∀ x m, ι R x • m = ⁅x, m⁆), not only for the one manufactured by Ado.UniversalEnvelopingAlgebra.asModule. That is what lets a module produced as a U(L)-module elsewhere — a quotient of U(L) by a left ideal is the motivating example — be read as a Lie module without transporting it along an equivalence first.

This is the U(L) analogue of Mathlib's dictionary between representations of a group G and modules over its group algebra k[G], in Mathlib/RepresentationTheory/; the correspondence below is named after its counterparts there wherever one exists.

Main definitions

• Ado.UniversalEnvelopingAlgebra.asModule: the U(L)-module structure on a Lie module, the analogue of Representation.asModule. A def, not an instance, since a global instance would compete with the restriction-of-scalars paths already present.
• Ado.UniversalEnvelopingAlgebra.asLieRingModule and Ado.UniversalEnvelopingAlgebra.asLieModule: the Lie module structure on a U(L)-module, the converse translation.
• Ado.UniversalEnvelopingAlgebra.lieSubmoduleOrderIso: the dictionary for submodules, an order isomorphism between the Lie submodules of M and its U(L)-submodules; the analogue of Representation.mapSubmodule.
• Ado.UniversalEnvelopingAlgebra.lieSubmoduleOrderIsoAsModule: that order isomorphism at the canonical structure Ado.UniversalEnvelopingAlgebra.asModule.
• Ado.UniversalEnvelopingAlgebra.lieModuleHomEquiv: the dictionary for homomorphisms, an R-linear equivalence between Lie module homomorphisms and U(L)-linear maps.
• Ado.UniversalEnvelopingAlgebra.lieModuleEquivEquivLinearEquiv: the corresponding dictionary from Lie-module equivalences to U(L)-linear equivalences.
• Ado.UniversalEnvelopingAlgebra.lieSubmoduleLinearEquiv: the identity equivalence between a Lie submodule and its image under an arbitrary compatible submodule dictionary.

Main results

• Ado.UniversalEnvelopingAlgebra.smul_mem_of_forall_ι_smul_mem: an R-submodule stable under the canonical Lie generators is stable under the whole enveloping algebra; the analogue of Representation.asAlgebraHom_mem_of_forall_mem.
• Ado.UniversalEnvelopingAlgebra.map_smul_of_map_ι_smul: an R-linear map equivariant for the canonical Lie generators is U(L)-linear.
• Ado.UniversalEnvelopingAlgebra.representation_eq_smul_of_mem_center_of_lieSpan_eq_top: a central element acting by one scalar on a generating set acts by that scalar everywhere.
• Ado.UniversalEnvelopingAlgebra.map_representation: a homomorphism of Lie modules intertwines the two enveloping-algebra actions; the previous item at the canonical structures.
• Ado.UniversalEnvelopingAlgebra.lieSubmoduleOrderIso_lieSpan: the Lie submodule generated by a set is its U(L)-span.
• Ado.UniversalEnvelopingAlgebra.isIrreducible_iff_isSimpleModule: irreducibility of a Lie module is simplicity of the corresponding U(L)-module.
• Ado.UniversalEnvelopingAlgebra.complementedLattice_lieSubmodule_iff_isSemisimpleModule: complete reducibility of a Lie module is semisimplicity of the corresponding U(L)-module.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Chapter V, §17.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapter I, §2.
• Mathlib/RepresentationTheory/Basic.lean (Antoine Labelle) and Mathlib/RepresentationTheory/Submodule.lean (Oliver Nash): the group-algebra dictionary Representation.asAlgebraHom, Representation.asModule, Representation.asAlgebraHom_mem_of_forall_mem and Representation.mapSubmodule, which this file follows for U(L) in place of k[G].
• Mathlib/RepresentationTheory/Intertwining.lean (Stepan Nesterov, Edison Xie): Representation.IntertwiningMap.equivLinearMapAsModule, the group-algebra homomorphism dictionary that lieModuleHomEquiv follows.
• Mathlib/RepresentationTheory/Irreducible.lean and Mathlib/RepresentationTheory/Semisimple.lean (Stepan Nesterov): the source of the pattern by which the two corollaries below compose an order isomorphism of submodule lattices with isSimpleModule_iff and isSemisimpleModule_iff.

From a Lie module to a module over the enveloping algebra

@[instance_reducible]

noncomputable def Ado.UniversalEnvelopingAlgebra.asModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Module (UniversalEnvelopingAlgebra R L) M

The enveloping-algebra module structure on a Lie module, by restriction of scalars along Ado.UniversalEnvelopingAlgebra.representation. This is the U(L) analogue of Mathlib's Representation.asModule, carried by M itself rather than by a type synonym.

This is a def rather than an instance: a global instance would compete with the restriction-of-scalars paths that a module already carries, and the dictionary below is stated for an arbitrary compatible U(L)-module structure, of which this is one.

Equations

• Ado.UniversalEnvelopingAlgebra.asModule R L M = Module.compHom M (Ado.UniversalEnvelopingAlgebra.representation R L M).toRingHom

theorem Ado.UniversalEnvelopingAlgebra.asModule_smul_def (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (u : UniversalEnvelopingAlgebra R L) (m : M) : u • m = ((representation R L M) u) m

The scalar action of Ado.UniversalEnvelopingAlgebra.asModule is evaluation of Ado.UniversalEnvelopingAlgebra.representation.

theorem Ado.UniversalEnvelopingAlgebra.asModule_ι_smul (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (m : M) : (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆

The canonical Lie generators act through Ado.UniversalEnvelopingAlgebra.asModule by the Lie bracket. This is the compatibility hypothesis that the dictionary below consumes.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.asModule_ι_smul' (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (m : M) : (UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x) • m = ⁅x, m⁆

The simp-normal form of Ado.UniversalEnvelopingAlgebra.asModule_ι_smul, stated for the canonical generators as simp writes them.

theorem Ado.UniversalEnvelopingAlgebra.representation_eq_smul_of_mem_center_of_lieSpan_eq_top (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {u : UniversalEnvelopingAlgebra R L} (hu : u ∈ Subalgebra.center R (UniversalEnvelopingAlgebra R L)) {S : Set M} {c : R} (hS : ∀ v ∈ S, ((representation R L M) u) v = c • v) (hgen : LieSubmodule.lieSpan R L S = ⊤) (m : M) : ((representation R L M) u) m = c • m

A central element of the universal enveloping algebra that acts by the same scalar on every element of a Lie-generating set acts by that scalar on the whole module.

theorem Ado.UniversalEnvelopingAlgebra.isScalarTower_asModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : IsScalarTower R (UniversalEnvelopingAlgebra R L) M

The scalars of Ado.UniversalEnvelopingAlgebra.asModule extend those of R, since Ado.UniversalEnvelopingAlgebra.representation is an R-algebra homomorphism.

From a module over the enveloping algebra to a Lie module

@[instance_reducible]

def Ado.UniversalEnvelopingAlgebra.asLieRingModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module (UniversalEnvelopingAlgebra R L) M] : LieRingModule L M

The Lie module structure on a U(L)-module, obtained by composing the canonical Lie map UniversalEnvelopingAlgebra.ι with the commutator action of U(L) on M.

This cannot be an instance: the base ring R is not determined by the conclusion.

Equations

• Ado.UniversalEnvelopingAlgebra.asLieRingModule R L M = LieRingModule.compLieHom M (UniversalEnvelopingAlgebra.ι R)

theorem Ado.UniversalEnvelopingAlgebra.asLieRingModule_bracket (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module (UniversalEnvelopingAlgebra R L) M] (x : L) (m : M) : ⁅x, m⁆ = (UniversalEnvelopingAlgebra.ι R) x • m

The bracket of Ado.UniversalEnvelopingAlgebra.asLieRingModule is the action of the canonical Lie generator.

theorem Ado.UniversalEnvelopingAlgebra.asLieModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] : LieModule R L M

The bracket of Ado.UniversalEnvelopingAlgebra.asLieRingModule is R-bilinear, so a U(L)-module whose scalars extend those of R is a Lie module over R.

The dictionary for submodules and homomorphisms

theorem Ado.UniversalEnvelopingAlgebra.smul_mem_of_forall_ι_smul_mem {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] {P : Submodule R M} (hP : ∀ (x : L), ∀ m ∈ P, (UniversalEnvelopingAlgebra.ι R) x • m ∈ P) (u : UniversalEnvelopingAlgebra R L) (m : M) (hm : m ∈ P) : u • m ∈ P

An R-submodule stable under the canonical Lie generators is stable under the whole enveloping algebra. The elements of U(L) that preserve the submodule form an R-subalgebra, and it contains the generators, which generate U(L). This is the U(L) analogue of Representation.asAlgebraHom_mem_of_forall_mem.

def Ado.UniversalEnvelopingAlgebra.lieSubmoduleOrderIso {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] (hcompat : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) : LieSubmodule R L M ≃o Submodule (UniversalEnvelopingAlgebra R L) M

The enveloping-algebra dictionary for submodules. For a U(L)-module structure on M compatible with the R-structure and with the Lie action, the Lie submodules of M are exactly its U(L)-submodules, and the correspondence is the identity on underlying sets. This is the U(L) analogue of Representation.mapSubmodule, and the route from the ring-level module theory of Mathlib/RingTheory/SimpleModule/ to Lie modules.

The coe_/mem_ lemmas below are the whole interface: nothing downstream unfolds the body.

Equations

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

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.coe_lieSubmoduleOrderIso {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] (hcompat : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (P : LieSubmodule R L M) : ↑((lieSubmoduleOrderIso hcompat) P) = ↑P

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.mem_lieSubmoduleOrderIso {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] (hcompat : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) {P : LieSubmodule R L M} {m : M} : m ∈ (lieSubmoduleOrderIso hcompat) P ↔ m ∈ P

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.coe_lieSubmoduleOrderIso_symm {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] (hcompat : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (Q : Submodule (UniversalEnvelopingAlgebra R L) M) : ↑((lieSubmoduleOrderIso hcompat).symm Q) = ↑Q

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.mem_lieSubmoduleOrderIso_symm {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] (hcompat : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) {Q : Submodule (UniversalEnvelopingAlgebra R L) M} {m : M} : m ∈ (lieSubmoduleOrderIso hcompat).symm Q ↔ m ∈ Q

theorem Ado.UniversalEnvelopingAlgebra.lieSubmoduleOrderIso_lieSpan {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] (hcompat : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (S : Set M) : (lieSubmoduleOrderIso hcompat) (LieSubmodule.lieSpan R L S) = Submodule.span (UniversalEnvelopingAlgebra R L) S

The dictionary carries generated submodules to generated submodules: the Lie submodule generated by a set is its U(L)-span. In particular a Lie module is generated by a vector exactly when that vector generates it as a U(L)-module, which is how a highest weight vector is checked to generate its module.

theorem Ado.UniversalEnvelopingAlgebra.isIrreducible_iff_isSimpleModule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] (hcompat : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) : IsSimpleOrder (LieSubmodule R L M) ↔ IsSimpleModule (UniversalEnvelopingAlgebra R L) M

Irreducibility of a Lie module is simplicity over the enveloping algebra.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.isSimpleModule_lieSubmoduleOrderIso_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] (hcompat : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (P : LieSubmodule R L M) : IsSimpleModule (UniversalEnvelopingAlgebra R L) ↥((lieSubmoduleOrderIso hcompat) P) ↔ LieModule.IsIrreducible R L ↥P

A Lie submodule is irreducible exactly when its image under a compatible enveloping-algebra submodule dictionary is simple.

theorem Ado.UniversalEnvelopingAlgebra.complementedLattice_lieSubmodule_iff_isSemisimpleModule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] (hcompat : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) : ComplementedLattice (LieSubmodule R L M) ↔ IsSemisimpleModule (UniversalEnvelopingAlgebra R L) M

Complete reducibility is semisimplicity over the enveloping algebra: every Lie submodule of M has a complement exactly when M is a semisimple U(L)-module.

theorem Ado.UniversalEnvelopingAlgebra.map_smul_of_map_ι_smul {R : Type u} {L : Type v} {M : Type w} {N : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [Module (UniversalEnvelopingAlgebra R L) N] [IsScalarTower R (UniversalEnvelopingAlgebra R L) N] (f : M →ₗ[R] N) (hf : ∀ (x : L) (m : M), f ((UniversalEnvelopingAlgebra.ι R) x • m) = (UniversalEnvelopingAlgebra.ι R) x • f m) (u : UniversalEnvelopingAlgebra R L) (m : M) : f (u • m) = u • f m

An R-linear map equivariant for the canonical Lie generators is U(L)-linear. As in Ado.UniversalEnvelopingAlgebra.smul_mem_of_forall_ι_smul_mem, the elements of U(L) over which the map is equivariant form an R-subalgebra containing the generators.

def Ado.UniversalEnvelopingAlgebra.lieModuleHomEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] [Module (UniversalEnvelopingAlgebra R L) N] [IsScalarTower R (UniversalEnvelopingAlgebra R L) N] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (hN : ∀ (x : L) (n : N), (UniversalEnvelopingAlgebra.ι R) x • n = ⁅x, n⁆) : (M →ₗ⁅R,L⁆ N) ≃ₗ[R] M →ₗ[UniversalEnvelopingAlgebra R L] N

The enveloping-algebra dictionary for homomorphisms: Lie module homomorphisms M → N are exactly U(L)-linear maps, by the identity on underlying functions, R-linearly in the homomorphism. As for Ado.UniversalEnvelopingAlgebra.lieSubmoduleOrderIso, the coe_ lemmas below are the whole interface.

Equations

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

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.coe_lieModuleHomEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] [Module (UniversalEnvelopingAlgebra R L) N] [IsScalarTower R (UniversalEnvelopingAlgebra R L) N] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (hN : ∀ (x : L) (n : N), (UniversalEnvelopingAlgebra.ι R) x • n = ⁅x, n⁆) (f : M →ₗ⁅R,L⁆ N) : ⇑((lieModuleHomEquiv hM hN) f) = ⇑f

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.coe_lieModuleHomEquiv_symm {R : Type u} {L : Type v} {M : Type w} {N : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] [Module (UniversalEnvelopingAlgebra R L) N] [IsScalarTower R (UniversalEnvelopingAlgebra R L) N] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (hN : ∀ (x : L) (n : N), (UniversalEnvelopingAlgebra.ι R) x • n = ⁅x, n⁆) (g : M →ₗ[UniversalEnvelopingAlgebra R L] N) : ⇑((lieModuleHomEquiv hM hN).symm g) = ⇑g

Equivalences

def Ado.UniversalEnvelopingAlgebra.lieModuleEquivEquivLinearEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] [Module (UniversalEnvelopingAlgebra R L) N] [IsScalarTower R (UniversalEnvelopingAlgebra R L) N] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (hN : ∀ (x : L) (n : N), (UniversalEnvelopingAlgebra.ι R) x • n = ⁅x, n⁆) : (M ≃ₗ⁅R,L⁆ N) ≃ M ≃ₗ[UniversalEnvelopingAlgebra R L] N

The enveloping-algebra dictionary for equivalences: Lie module equivalences are exactly U(L)-linear equivalences when both actions are compatible with the canonical Lie generators. The correspondence is the identity on underlying functions.

Equations

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

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.coe_lieModuleEquivEquivLinearEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] [Module (UniversalEnvelopingAlgebra R L) N] [IsScalarTower R (UniversalEnvelopingAlgebra R L) N] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (hN : ∀ (x : L) (n : N), (UniversalEnvelopingAlgebra.ι R) x • n = ⁅x, n⁆) (e : M ≃ₗ⁅R,L⁆ N) : ⇑((lieModuleEquivEquivLinearEquiv hM hN) e) = ⇑e

The forward equivalence dictionary does not change the underlying function.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.coe_lieModuleEquivEquivLinearEquiv_apply_symm {R : Type u} {L : Type v} {M : Type w} {N : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] [Module (UniversalEnvelopingAlgebra R L) N] [IsScalarTower R (UniversalEnvelopingAlgebra R L) N] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (hN : ∀ (x : L) (n : N), (UniversalEnvelopingAlgebra.ι R) x • n = ⁅x, n⁆) (e : M ≃ₗ⁅R,L⁆ N) : ⇑((lieModuleEquivEquivLinearEquiv hM hN) e).symm = ⇑e.symm

The inverse of the forward equivalence dictionary is the original inverse function.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.coe_lieModuleEquivEquivLinearEquiv_symm {R : Type u} {L : Type v} {M : Type w} {N : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] [Module (UniversalEnvelopingAlgebra R L) N] [IsScalarTower R (UniversalEnvelopingAlgebra R L) N] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (hN : ∀ (x : L) (n : N), (UniversalEnvelopingAlgebra.ι R) x • n = ⁅x, n⁆) (e : M ≃ₗ[UniversalEnvelopingAlgebra R L] N) : ⇑((lieModuleEquivEquivLinearEquiv hM hN).symm e) = ⇑e

The inverse equivalence dictionary does not change the underlying function.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.coe_lieModuleEquivEquivLinearEquiv_symm_apply_symm {R : Type u} {L : Type v} {M : Type w} {N : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] [Module (UniversalEnvelopingAlgebra R L) N] [IsScalarTower R (UniversalEnvelopingAlgebra R L) N] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (hN : ∀ (x : L) (n : N), (UniversalEnvelopingAlgebra.ι R) x • n = ⁅x, n⁆) (e : M ≃ₗ[UniversalEnvelopingAlgebra R L] N) : ⇑((lieModuleEquivEquivLinearEquiv hM hN).symm e).symm = ⇑e.symm

The inverse of the backward equivalence dictionary is the original inverse function.

Submodule equivalences

noncomputable def Ado.UniversalEnvelopingAlgebra.lieSubmoduleLinearEquiv {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieModule R L M] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (P : LieSubmodule R L M) : ↥P ≃ₗ[UniversalEnvelopingAlgebra R L] ↥((lieSubmoduleOrderIso hM) P)

A Lie submodule with its canonical U(L)-action is linearly equivalent, by the identity map, to its image under an arbitrary compatible enveloping-algebra submodule dictionary.

Equations

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

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.coe_lieSubmoduleLinearEquiv {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieModule R L M] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (P : LieSubmodule R L M) : ⇑(lieSubmoduleLinearEquiv hM P) = fun (p : ↥P) => ⟨↑p, ⋯⟩

The compatible-action submodule equivalence preserves the underlying ambient element.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.coe_lieSubmoduleLinearEquiv_symm {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieModule R L M] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (P : LieSubmodule R L M) : ⇑(lieSubmoduleLinearEquiv hM P).symm = fun (p : ↥((lieSubmoduleOrderIso hM) P)) => ⟨↑p, ⋯⟩

The inverse compatible-action submodule equivalence preserves the underlying ambient element.

theorem Ado.UniversalEnvelopingAlgebra.nonempty_lieModuleEquiv_iff_nonempty_linearEquiv {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieModule R L M] (hM : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (S : Type u_1) [AddCommGroup S] [Module R S] [LieRingModule L S] [LieModule R L S] [Module (UniversalEnvelopingAlgebra R L) S] [IsScalarTower R (UniversalEnvelopingAlgebra R L) S] (hS : ∀ (x : L) (s : S), (UniversalEnvelopingAlgebra.ι R) x • s = ⁅x, s⁆) (P : LieSubmodule R L M) : Nonempty (↥P ≃ₗ⁅R,L⁆ S) ↔ Nonempty (↥((lieSubmoduleOrderIso hM) P) ≃ₗ[UniversalEnvelopingAlgebra R L] S)

Equivalence to a fixed Lie module is the same as linear equivalence from the corresponding compatible enveloping-algebra submodule.

The dictionary for the canonical enveloping-algebra module structure

The statements above take the U(L)-module structure as a hypothesis. Instantiated at Ado.UniversalEnvelopingAlgebra.asModule, they say that the lattice of Lie submodules of any Lie module is the lattice of U(L)-submodules of the same module.

noncomputable def Ado.UniversalEnvelopingAlgebra.lieSubmoduleOrderIsoAsModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieSubmodule R L M ≃o Submodule (UniversalEnvelopingAlgebra R L) M

The submodule dictionary for the canonical enveloping-algebra module structure Ado.UniversalEnvelopingAlgebra.asModule.

Equations

• Ado.UniversalEnvelopingAlgebra.lieSubmoduleOrderIsoAsModule R L M = Ado.UniversalEnvelopingAlgebra.lieSubmoduleOrderIso ⋯

theorem Ado.UniversalEnvelopingAlgebra.lieSubmoduleOrderIsoAsModule_def (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : lieSubmoduleOrderIsoAsModule R L M = lieSubmoduleOrderIso ⋯

Ado.UniversalEnvelopingAlgebra.lieSubmoduleOrderIsoAsModule is the general dictionary at the compatibility supplied by Ado.UniversalEnvelopingAlgebra.asModule_ι_smul, so all the lemmas about the former apply to it.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.mem_lieSubmoduleOrderIsoAsModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {P : LieSubmodule R L M} {m : M} : m ∈ (lieSubmoduleOrderIsoAsModule R L M) P ↔ m ∈ P

Membership in the canonical submodule dictionary is membership in the Lie submodule.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.mem_lieSubmoduleOrderIsoAsModule_symm (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {Q : Submodule (UniversalEnvelopingAlgebra R L) M} {m : M} : m ∈ (lieSubmoduleOrderIsoAsModule R L M).symm Q ↔ m ∈ Q

Membership in the inverse of the canonical submodule dictionary is membership in the U(L)-submodule.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.coe_asModule_smul_lieSubmodule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (P : LieSubmodule R L M) (u : UniversalEnvelopingAlgebra R L) (p : ↥P) : ↑(u • p) = u • ↑p

The canonical U(L)-action on a Lie submodule agrees, after inclusion, with the canonical action on the ambient Lie module.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.map_representation (R : Type u) (L : Type v) (M : Type w) (N : Type x) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [LieRingModule L M] [LieModule R L M] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L⁆ N) (u : UniversalEnvelopingAlgebra R L) (m : M) : f (((representation R L M) u) m) = ((representation R L N) u) (f m)

A homomorphism of Lie modules intertwines the enveloping-algebra actions. Equivariance for the canonical Lie generators is the defining property of such a homomorphism, and those generate U(L) as an algebra; this is Ado.UniversalEnvelopingAlgebra.map_smul_of_map_ι_smul at the canonical module structures.