Cofinite refinements stable under lifted derivations

Let L be a module-finite Lie algebra, I a two-sided ideal of U(L) with Noetherian quotient over the coefficient ring, and N a Lie ideal whose canonical images are nilpotent modulo I. A power of B = I ⊔ N.envelopingIdeal lies inside I, has module-finite quotient, and is stable under every lifted derivation whose values on L lie in N. Moreover, every element nilpotent modulo I remains nilpotent modulo the refinement, and conversely.

For a finite-dimensional solvable Lie algebra in characteristic zero, every derivation takes values in its nilradical. Ideal.exists_cofinite_refinement_stableDerivations_of_isSolvable therefore supplies a refinement stable under all lifted derivations, when the nilradical acts nilpotently modulo the original ideal. The general refinement also works over commutative coefficient rings when the original quotient is Noetherian, and does not require a free Lie algebra.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Appendix E, §E.2, the cofinite-ideal refinement in the proof of Proposition E.5.

theorem LieIdeal.exists_cofinite_refinement_stableDerivations {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] (N : LieIdeal R L) (I : Ideal (UniversalEnvelopingAlgebra R L)) [I.IsTwoSided] [IsNoetherian R (UniversalEnvelopingAlgebra R L ⧸ I)] (hnil : ∀ x ∈ N, IsNilpotent ((Ideal.Quotient.mk I) ((UniversalEnvelopingAlgebra.ι R) x))) : ∃ (n : ℕ), (I ⊔ N.envelopingIdeal) ^ n ≤ I ∧ Module.Finite R (UniversalEnvelopingAlgebra R L ⧸ (I ⊔ N.envelopingIdeal) ^ n) ∧ (∀ (D : LieDerivation R L L), (∀ (x : L), D x ∈ N) → Ado.UniversalEnvelopingAlgebra.envelopingDerivation R L D ∈ Ado.stableDerivations R (Submodule.restrictScalars R ((I ⊔ N.envelopingIdeal) ^ n))) ∧ ∀ (a : UniversalEnvelopingAlgebra R L), IsNilpotent ((Ideal.Quotient.mk ((I ⊔ N.envelopingIdeal) ^ n)) a) ↔ IsNilpotent ((Ideal.Quotient.mk I) a)

A two-sided ideal whose quotient is Noetherian over the coefficient ring admits a cofinite refinement stable under every lifted derivation taking values in a Lie ideal N that acts nilpotently modulo the original ideal. The refinement is a power of I ⊔ N.envelopingIdeal, and it has exactly the same nilpotent elements in its quotient as the original ideal. No stability of I is assumed.

theorem Ideal.exists_cofinite_refinement_stableDerivations_of_isSolvable {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsSolvable L] (I : Ideal (UniversalEnvelopingAlgebra K L)) [I.IsTwoSided] [Module.Finite K (UniversalEnvelopingAlgebra K L ⧸ I)] (hnil : ∀ x ∈ Ado.LieAlgebra.nilradical K L, IsNilpotent ((Quotient.mk I) ((UniversalEnvelopingAlgebra.ι K) x))) : ∃ (n : ℕ), (I ⊔ (Ado.LieAlgebra.nilradical K L).envelopingIdeal) ^ n ≤ I ∧ Module.Finite K (UniversalEnvelopingAlgebra K L ⧸ (I ⊔ (Ado.LieAlgebra.nilradical K L).envelopingIdeal) ^ n) ∧ (∀ (D : LieDerivation K L L), Ado.UniversalEnvelopingAlgebra.envelopingDerivation K L D ∈ Ado.stableDerivations K (Submodule.restrictScalars K ((I ⊔ (Ado.LieAlgebra.nilradical K L).envelopingIdeal) ^ n))) ∧ ∀ (a : UniversalEnvelopingAlgebra K L), IsNilpotent ((Quotient.mk ((I ⊔ (Ado.LieAlgebra.nilradical K L).envelopingIdeal) ^ n)) a) ↔ IsNilpotent ((Quotient.mk I) a)

A cofinite two-sided enveloping ideal I of a finite-dimensional solvable Lie algebra in characteristic zero, on whose quotient the nilradical acts nilpotently, admits a cofinite refinement stable under every lifted derivation. The refinement is a power of I ⊔ (nilradical K L).envelopingIdeal lying inside I, and it has exactly the same nilpotent elements modulo it as I.