Finite images of enveloping algebras from monic relations

If the images of a finite spanning family of a Lie algebra satisfy monic polynomial relations over central scalars, every surjective image of its enveloping algebra is module-finite over those scalars. The target algebra need not be commutative. Ordered PBW monomials group the powers of each generator together. Reducing each power by its monic relation and using multilinearity expresses every such product in terms of the bounded products.

This provides the finiteness argument both for enveloping algebras over central subalgebras and for two-sided quotients by noncentral monic relations.

References

• N. Jacobson, Lie Algebras, Chapter V (PBW).
• W. Fulton and J. Harris, Representation Theory: A First Course, Appendix E, §E.2.

theorem Ado.UniversalEnvelopingAlgebra.span_range_orderedPowerProducts_eq_top (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type x} [Ring A] [Algebra R A] (S : Type w) [CommRing S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] {n : ℕ} (e : Fin n → L) (he : Submodule.span R (Set.range e) = ⊤) (q : UniversalEnvelopingAlgebra R L →ₐ[R] A) (hq : Function.Surjective ⇑q) : Submodule.span S (Set.range fun (c : Fin n → ℕ) => (List.map (fun (i : Fin n) => q ((UniversalEnvelopingAlgebra.ι R) (e i)) ^ c i) (List.finRange n)).prod) = ⊤

Ordered products of generator powers span every surjective image of an enveloping algebra. Only a spanning family of the Lie algebra is required.

theorem Ado.UniversalEnvelopingAlgebra.span_range_bounded_orderedPowerProducts_eq_top (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type x} [Ring A] [Algebra R A] (S : Type w) [CommRing S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] {n : ℕ} (e : Fin n → L) (he : Submodule.span R (Set.range e) = ⊤) (q : UniversalEnvelopingAlgebra R L →ₐ[R] A) (hq : Function.Surjective ⇑q) (p : Fin n → Polynomial S) (hp : ∀ (i : Fin n), (p i).Monic) (hpx : ∀ (i : Fin n), (Polynomial.aeval (q ((UniversalEnvelopingAlgebra.ι R) (e i)))) (p i) = 0) : Submodule.span S (Set.range fun (c : (i : Fin n) → Fin (p i).natDegree) => (List.map (fun (i : Fin n) => q ((UniversalEnvelopingAlgebra.ι R) (e i)) ^ ↑(c i)) (List.finRange n)).prod) = ⊤

If the generator images satisfy monic relations p i, the ordered products with exponent of generator i strictly less than (p i).natDegree span the target. This is an explicit finite spanning family even when the target is noncommutative.

theorem Ado.UniversalEnvelopingAlgebra.moduleFinite_of_isIntegral_of_span_eq_top (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type x} [Ring A] [Algebra R A] (S : Type w) [CommRing S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] {n : ℕ} (e : Fin n → L) (he : Submodule.span R (Set.range e) = ⊤) (q : UniversalEnvelopingAlgebra R L →ₐ[R] A) (hq : Function.Surjective ⇑q) (h : ∀ (i : Fin n), IsIntegral S (q ((UniversalEnvelopingAlgebra.ι R) (e i)))) : Module.Finite S A

A surjective image of an enveloping algebra is module-finite over central scalars S if the images of a finite spanning family of the Lie algebra are integral over S. The target algebra may be noncommutative.