Enveloping algebras over domains have no zero divisors

The PBW filtration of U(L) is the word filtration generated by the canonical Lie map UniversalEnvelopingAlgebra.ι R, and it is exhaustive (TauCeti.UniversalEnvelopingAlgebra.iSup_pbwFiltration_eq_top), so the filtered-to-graded transfer of TauCeti/Algebra/WordFiltration/Domain.lean applies to it verbatim: if the PBW associated graded gr U(L) has no zero divisors, then neither does U(L).

Transferring the domain property downwards needs two mathematical inputs: exhaustivity of the filtration, and the domain property of the graded side. The first holds for the PBW filtration of any Lie algebra over any commutative ring. The second follows, when L is free, from the Poincaré--Birkhoff--Witt theorem: the canonical map TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap from the symmetric algebra Sym(L) to gr U(L) is surjective (TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_surjective) and, for a free L, injective, hence an isomorphism, so gr U(L) inherits the domain property of Sym(L) over a domain.

Main results

• TauCeti.UniversalEnvelopingAlgebra.noZeroDivisors_of_noZeroDivisors_pbwAssociatedGraded: U(L) has no zero divisors as soon as gr U(L) has none.
• TauCeti.UniversalEnvelopingAlgebra.isDomain_of_noZeroDivisors_pbwAssociatedGraded: over a nontrivial base ring, U(L) is then a domain.
• TauCeti.UniversalEnvelopingAlgebra.instNoZeroDivisors: U(L) has no zero divisors when L is free over a base ring with no zero divisors.
• TauCeti.UniversalEnvelopingAlgebra.instIsDomain: U(L) is a domain when L is free over a domain, in particular for every Lie algebra over a field.

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.noZeroDivisors_of_noZeroDivisors_pbwAssociatedGraded (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [NoZeroDivisors (PBWAssociatedGraded R L)] : NoZeroDivisors (UniversalEnvelopingAlgebra R L)

The enveloping algebra has no zero divisors as soon as its PBW associated graded has none.

theorem TauCeti.UniversalEnvelopingAlgebra.isDomain_of_noZeroDivisors_pbwAssociatedGraded (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Nontrivial R] [NoZeroDivisors (PBWAssociatedGraded R L)] : IsDomain (UniversalEnvelopingAlgebra R L)

The enveloping algebra of a Lie algebra over a nontrivial base ring is a domain as soon as its PBW associated graded has no zero divisors.

instance TauCeti.UniversalEnvelopingAlgebra.instNoZeroDivisorsPBWAssociatedGraded (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [NoZeroDivisors R] [Module.Free R L] : NoZeroDivisors (PBWAssociatedGraded R L)

The PBW associated graded of a Lie algebra free over a ring with no zero divisors has no zero divisors.

instance TauCeti.UniversalEnvelopingAlgebra.instNoZeroDivisors (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [NoZeroDivisors R] [Module.Free R L] : NoZeroDivisors (UniversalEnvelopingAlgebra R L)

The enveloping algebra of a Lie algebra free over a ring with no zero divisors has no zero divisors.

instance TauCeti.UniversalEnvelopingAlgebra.instIsDomain (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsDomain R] [Module.Free R L] : IsDomain (UniversalEnvelopingAlgebra R L)

The enveloping algebra of a Lie algebra free over a domain is a domain. In particular, this holds for every Lie algebra over a field.