The center of an enveloping algebra in positive characteristic #
In prime characteristic the enveloping algebra of a finite-dimensional Lie algebra is
finite over the Noetherian algebra generated by central p-polynomials. Consequently it
is finite over its whole center, and that center is Noetherian. These facts supply the
hypotheses for applying the generalized Krull intersection theorem to the central
augmentation ideal.
This is the commutative-algebra step in G. Hochschild, An Addition to Ado's Theorem, Proc. Amer. Math. Soc. 17 (1966), 531–533.
theorem
TauCeti.UniversalEnvelopingAlgebra.isNoetherianRing_center
(K : Type u)
(L : Type v)
[Field K]
[LieRing L]
[LieAlgebra K L]
(p : ℕ)
[Fact (Nat.Prime p)]
[CharP K p]
[FiniteDimensional K L]
:
In positive characteristic, the center of U(L) is Noetherian.
theorem
TauCeti.UniversalEnvelopingAlgebra.moduleFinite_over_center
(K : Type u)
(L : Type v)
[Field K]
[LieRing L]
[LieAlgebra K L]
(p : ℕ)
[Fact (Nat.Prime p)]
[CharP K p]
[FiniteDimensional K L]
:
Module.Finite (↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))) (UniversalEnvelopingAlgebra K L)
In positive characteristic, U(L) is finite over its center.