Right Noetherian universal enveloping algebras

The antipode identifies a universal enveloping algebra with its opposite algebra, so left Noetherianity implies right Noetherianity. Mathlib expresses the latter as IsNoetherianRing (UniversalEnvelopingAlgebra R L)ᵐᵒᵖ.

In particular, the enveloping algebra of a Lie algebra finite as a module over a commutative Noetherian ring is Noetherian on both sides. The left Noetherian result in TauCeti.Algebra.Lie.UniversalEnveloping.PBW.Noetherian.Basic uses the surjection from the symmetric algebra to the PBW associated graded and the filtered-to-graded transfer. The instance here obtains its right counterpart through the existing TauCeti.UniversalEnvelopingAlgebra.antipodeEquiv, without freeness, characteristic, or algebraic-closure assumptions. This supplies the ascending chain condition on right ideals used in the structure theory of enveloping algebras.

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.instIsNoetherianRingMulOpposite (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherianRing (UniversalEnvelopingAlgebra R L)] : IsNoetherianRing (UniversalEnvelopingAlgebra R L)ᵐᵒᵖ

A left Noetherian universal enveloping algebra is also right Noetherian. In particular, this applies to every module-finite Lie algebra over a commutative Noetherian ring.