The enveloping algebra of a finite Lie algebra over a Noetherian ring is Noetherian

A universal enveloping algebra need not be commutative -- it is when L is abelian, but not in general -- so the Hilbert basis theorem does not apply to it directly; what is always commutative is the associated graded of its PBW filtration. This file runs that comparison. The PBW filtration 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/Noetherian.lean applies to it verbatim: U(L) is left Noetherian as soon as gr U(L) is.

The graded side needs no Poincaré--Birkhoff--Witt theorem, only its easy half. The canonical map TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap from the symmetric algebra Sym(L) to gr U(L) is surjective for every Lie algebra over every commutative ring (TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_surjective) -- injectivity, the hard half, is what needs L free -- and Sym(L) is Noetherian whenever R is Noetherian and L is module-finite (TauCeti.SymmetricAlgebra.instIsNoetherianRing). So gr U(L) is a quotient of a Noetherian ring, hence Noetherian, and the transfer carries that down to U(L).

The hypotheses are therefore R Noetherian and L finite as an R-module, with no field, no freeness and no abelianness. Over a field this specializes to the Poincaré--Birkhoff--Witt corollary that the enveloping algebra of a finite-dimensional Lie algebra is Noetherian (TauCeti.UniversalEnvelopingAlgebra.isNoetherianRing_universalEnvelopingAlgebra). This file treats left ideals, matching Mathlib's IsNoetherianRing. The companion TauCeti/Algebra/Lie/UniversalEnveloping/PBW/Noetherian/Opposite.lean transfers this result through the antipode to obtain the right Noetherian statement.

Main results

• TauCeti.UniversalEnvelopingAlgebra.instIsNoetherianRingPBWAssociatedGraded: the PBW associated graded is Noetherian, being a quotient of the symmetric algebra.
• TauCeti.UniversalEnvelopingAlgebra.isNoetherianRing_of_isNoetherianRing_pbwAssociatedGraded: U(L) is Noetherian as soon as gr U(L) is.
• TauCeti.UniversalEnvelopingAlgebra.instIsNoetherianRing: the enveloping algebra of a Lie algebra finite over a Noetherian commutative ring is left Noetherian.
• TauCeti.UniversalEnvelopingAlgebra.isNoetherianRing_universalEnvelopingAlgebra: the same statement for a finite-dimensional Lie algebra over a field.

References

• J. Dixmier, Enveloping Algebras, AMS GSM 11 (1996), §2.3.
• J. C. McConnell and J. C. Robson, Noncommutative Noetherian Rings, Wiley (1987), §1.6.

instance TauCeti.UniversalEnvelopingAlgebra.instIsNoetherianRingPBWAssociatedGraded (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherianRing R] [Module.Finite R L] : IsNoetherianRing (PBWAssociatedGraded R L)

The PBW associated graded of a module-finite Lie algebra over a Noetherian ring is Noetherian: it is a quotient of the symmetric algebra Sym(L) by TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_surjective, and that symmetric algebra is Noetherian.

theorem TauCeti.UniversalEnvelopingAlgebra.isNoetherianRing_of_isNoetherianRing_pbwAssociatedGraded (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherianRing (PBWAssociatedGraded R L)] : IsNoetherianRing (UniversalEnvelopingAlgebra R L)

The enveloping algebra is left Noetherian as soon as its PBW associated graded is.

instance TauCeti.UniversalEnvelopingAlgebra.instIsNoetherianRing (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherianRing R] [Module.Finite R L] : IsNoetherianRing (UniversalEnvelopingAlgebra R L)

The enveloping algebra of a Lie algebra finite over a Noetherian commutative ring is left Noetherian.

theorem TauCeti.UniversalEnvelopingAlgebra.isNoetherianRing_universalEnvelopingAlgebra (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] : IsNoetherianRing (UniversalEnvelopingAlgebra K L)

The enveloping algebra of a finite-dimensional Lie algebra over a field is left Noetherian, the Poincaré--Birkhoff--Witt corollary. This is the classical form of TauCeti.UniversalEnvelopingAlgebra.instIsNoetherianRing; no freeness hypothesis appears, a finite-dimensional vector space being automatically free.