Finite generation over central subalgebras

Let L be a Lie algebra over a commutative ring R and let S be a commutative ring acting on U(L) by central scalars. If the canonical images in U(L) of a finite family spanning L are integral over S, then U(L) is finite as an S-module.

For a finite-dimensional Lie algebra over a field of prime characteristic p the central p-polynomials of TauCeti.Algebra.Lie.UniversalEnveloping.PCenter supply such an S: one p-polynomial for each member of a basis. The subalgebra of the center that they generate is Noetherian, U(L) is finite over it, and each generator lies in the augmentation ideal. The finiteness argument uses the monic-relation theorem of TauCeti.Algebra.Lie.UniversalEnveloping.PBW.Finite.

Those three conclusions are exactly the input to the Krull-intersection step of the positive-characteristic proof of Ado--Iwasawa: Noetherianity and module-finiteness let the generalized Krull intersection theorem apply, and augmentation membership makes the quotient of U(L) by the ideal the generators span finite dimensional.

Main results

• TauCeti.UniversalEnvelopingAlgebra.exists_pCentralGenerators_moduleFinite: in prime characteristic, finitely many central p-polynomials generate a Noetherian coefficient algebra over which the enveloping algebra is module-finite.

References

• N. Jacobson, Lie Algebras, Chapter VI, section 2.

theorem TauCeti.UniversalEnvelopingAlgebra.exists_pCentralGenerators_moduleFinite (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] [FiniteDimensional K L] : ∃ (e : Fin (Module.finrank K L) → ℕ) (a : (i : Fin (Module.finrank K L)) → Fin (e i) → K) (c : Fin (Module.finrank K L) → ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))), (∀ (i : Fin (Module.finrank K L)), ↑(c i) = (UniversalEnvelopingAlgebra.ι K) ((Module.finBasis K L) i) ^ p ^ e i + ∑ j : Fin (e i), a i j • (UniversalEnvelopingAlgebra.ι K) ((Module.finBasis K L) i) ^ p ^ ↑j) ∧ (∀ (i : Fin (Module.finrank K L)), ↑(c i) ∈ (HopfIdeal.augmentation K (UniversalEnvelopingAlgebra K L)).toIdeal) ∧ let S := Algebra.adjoin K (Set.range c); have x := S.centralSubalgebraAlgebra; IsNoetherianRing ↥S ∧ Module.Finite (↥S) (UniversalEnvelopingAlgebra K L)

The enveloping algebra is module-finite over a Noetherian algebra generated by central p-polynomials. For a finite-dimensional Lie algebra L over a field of prime characteristic p, there is one central p-polynomial for each member of a finite basis. These elements lie in the augmentation ideal. Their algebra S in the center of U(L) is Noetherian, and U(L) is a finite S-module.

The generators are returned together with the exponent e i and the coefficients a i that exhibit c i as a p-polynomial in the i-th member of Module.finBasis K L, and with their augmentation-ideal membership, both of which are needed when passing to a finite-dimensional quotient.