Powers of cofinite enveloping-algebra ideals

If a two-sided quotient of U(L) is module-finite over the coefficient ring and L is module-finite, quotients by all powers of the ideal are module-finite as well. Each Lie generator satisfies a monic relation in the original finite quotient. Raising that polynomial gives a monic relation modulo the ideal's power, and ordered PBW spanning then gives module-finiteness.

Over a field this says that every power of a cofinite two-sided ideal is cofinite. It is useful when refining a representation kernel to an ideal stable under derivations, while retaining a finite-dimensional quotient on which to represent the Lie algebra.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Appendix E, §E.2.

theorem Ado.UniversalEnvelopingAlgebra.span_range_quotient_pow_orderedPowerProducts_eq_top (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {d : ℕ} (e : Fin d → L) (he : Submodule.span R (Set.range e) = ⊤) (I : Ideal (UniversalEnvelopingAlgebra R L)) [I.IsTwoSided] (p : Fin d → Polynomial R) (hp : ∀ (i : Fin d), (p i).Monic) (hI : ∀ (i : Fin d), (Polynomial.aeval ((UniversalEnvelopingAlgebra.ι R) (e i))) (p i) ∈ I) (n : ℕ) : Submodule.span R (Set.range fun (c : (i : Fin d) → Fin (p i ^ n).natDegree) => (List.map (fun (i : Fin d) => (Ideal.Quotient.mk (I ^ n)) ((UniversalEnvelopingAlgebra.ι R) (e i)) ^ ↑(c i)) (List.finRange d)).prod) = ⊤

If monic polynomials p i evaluated at a spanning family of Lie generators lie in I, then modulo I^n the ordered products with exponents below the degrees of p i ^ n span. These bounds give an explicit finite spanning family for the quotient.

theorem Ado.UniversalEnvelopingAlgebra.moduleFinite_quotient_pow_of_isIntegral (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {d : ℕ} (e : Fin d → L) (he : Submodule.span R (Set.range e) = ⊤) (I : Ideal (UniversalEnvelopingAlgebra R L)) [I.IsTwoSided] (hI : ∀ (i : Fin d), IsIntegral R ((Ideal.Quotient.mk I) ((UniversalEnvelopingAlgebra.ι R) (e i)))) (n : ℕ) : Module.Finite R (UniversalEnvelopingAlgebra R L ⧸ I ^ n)

Monic relations modulo a two-sided ideal for a finite spanning family of L imply that quotients by every power of the ideal are module-finite.

theorem Ado.UniversalEnvelopingAlgebra.moduleFinite_quotient_pow (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] (I : Ideal (UniversalEnvelopingAlgebra R L)) [I.IsTwoSided] [Module.Finite R (UniversalEnvelopingAlgebra R L ⧸ I)] (n : ℕ) : Module.Finite R (UniversalEnvelopingAlgebra R L ⧸ I ^ n)

Every power of a two-sided ideal with module-finite quotient has module-finite quotient, provided the Lie algebra is module-finite. The coefficient ring need not be a field or Noetherian.