Finite-dimensional quotients of an enveloping algebra in prime characteristic

Write UC = TauCeti.HopfIdeal.centralAugmentationIdeal K (U(L)) for the two-sided ideal of the universal enveloping algebra generated by the central elements of augmentation zero.

Let L be a finite-dimensional Lie algebra over a field K of prime characteristic p. Each element of a basis of L has a central p-polynomial in U(L), and those finitely many central elements generate a commutative subalgebra S of the centre over which U(L) is a finite module (TauCeti.UniversalEnvelopingAlgebra.exists_pCentralGenerators_moduleFinite). They also have augmentation zero, so they belong to UC. Together those two facts make every power of UC contain the extension to U(L) of a power of the ideal of S that the generators span, whose quotient is finite dimensional, and TauCeti.finite_quotient_pow_of_algebraMap_mem turns that into the theorem of this file: U(L) ⧸ UC ^ n is finite dimensional over K, for every n. It is nonzero for n ≠ 0, by TauCeti.HopfIdeal.nontrivial_quotient_centralAugmentationIdeal_pow, so the quotient is a nonzero finite-dimensional associative algebra.

Such a quotient is the target of Hochschild's proof of the Ado--Iwasawa theorem in prime characteristic: the left-regular action of L on U(L) ⧸ UC ^ n is a finite-dimensional representation, it is faithful as soon as the composite of the canonical map L → U(L) with the quotient map is injective, and it carries every adjoint-nilpotent element of L to a nilpotent endomorphism for every n, by TauCeti.UniversalEnvelopingAlgebra.isNilpotent_quotient_leftRegularRep_of_isNilpotent_ad.

Main results

• TauCeti.UniversalEnvelopingAlgebra.finiteDimensional_quotient_centralAugmentationIdeal_pow: the quotient of U(L) by a power of the central augmentation ideal is finite dimensional.

References

• G. Hochschild, An Addition to Ado's Theorem, Proceedings of the American Mathematical Society 17 (1966), 531--533.
• N. Jacobson, Lie Algebras, Chapter VI, section 2.

theorem TauCeti.UniversalEnvelopingAlgebra.finiteDimensional_quotient_centralAugmentationIdeal_pow (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] [FiniteDimensional K L] (n : ℕ) : FiniteDimensional K (UniversalEnvelopingAlgebra K L ⧸ HopfIdeal.centralAugmentationIdeal K (UniversalEnvelopingAlgebra K L) ^ n)

The quotient of an enveloping algebra by a power of the central augmentation ideal is finite dimensional. For a finite-dimensional Lie algebra over a field of prime characteristic, the central p-polynomials of a basis lie in the central augmentation ideal and make U(L) a finite module over the commutative subalgebra they generate, which is exactly the input that bounds the dimension of the quotient.