The canonical embedding into an enveloping algebra

A Lie algebra L that is free as a module over a commutative ring R embeds in its universal enveloping algebra. The degree-one map into the PBW associated graded is injective, since the Poincaré--Birkhoff--Witt isomorphism identifies it with the canonical embedding into the symmetric algebra. Consequently the canonical Lie map ι : L → U(L) is injective, and the images of any basis of L are linearly independent.

These results identify L with its canonical copy in U(L), so a quotient of U(L) separating that copy gives a faithful representation of L. Over a field freeness is automatic; neither finite-dimensionality nor a characteristic assumption is needed.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Chapter V, §17.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapter I, §2.7.

theorem TauCeti.UniversalEnvelopingAlgebra.pbwGradedGenerator_injective (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] : Function.Injective ⇑(pbwGradedGenerator R L)

The degree-one generators of the PBW associated graded embed a Lie algebra that is free as a module over the base ring.

theorem TauCeti.UniversalEnvelopingAlgebra.ι_injective (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] : Function.Injective ⇑(UniversalEnvelopingAlgebra.ι R)

A Lie algebra that is free as a module over a commutative ring embeds in its universal enveloping algebra. In particular, this holds for every Lie algebra over a field.

theorem TauCeti.UniversalEnvelopingAlgebra.linearIndependent_ι_basis (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {κ : Type w} (b : Module.Basis κ R L) : LinearIndependent R fun (i : κ) => (UniversalEnvelopingAlgebra.ι R) (b i)

The images of a basis of a Lie algebra are linearly independent in its enveloping algebra.