Adjoint-nilpotent elements in central-augmentation quotients

In positive characteristic, a power of the enveloping-algebra generator of an element whose adjoint action is nilpotent lies in every prescribed power of the central augmentation ideal. Consequently, any associative target killing such an ideal power sends that generator to a nilpotent element. Its left-regular representation also acts nilpotently.

These conclusions hold for the quotient by any power of the central augmentation ideal. They require neither a finite-dimensional separating quotient nor a nilpotent Lie algebra. When a quotient over a field is finite-dimensional and separates the Lie algebra, its left-regular action gives a faithful representation that preserves adjoint nilpotence.

The quotient-nilpotence argument follows G. Hochschild, An Addition to Ado's Theorem, Proceedings of the American Mathematical Society 17 (1966), 531–533.

theorem TauCeti.UniversalEnvelopingAlgebra.isNilpotent_map_ι_of_isNilpotent_ad (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type w} [Semiring A] (p : ℕ) [ExpChar R p] (hp : p ≠ 1) (q : UniversalEnvelopingAlgebra R L →+* A) (n : ℕ) (hq : ∀ z ∈ HopfIdeal.centralAugmentationIdeal R (UniversalEnvelopingAlgebra R L) ^ n, q z = 0) {x : L} (hx : IsNilpotent ((LieAlgebra.ad R L) x)) : IsNilpotent (q ((UniversalEnvelopingAlgebra.ι R) x))

In exponential characteristic p ≠ 1, if a ring homomorphism kills a power of the central augmentation ideal, then it sends every adjoint-nilpotent Lie element to a nilpotent element.

theorem TauCeti.UniversalEnvelopingAlgebra.isNilpotent_quotient_ι_of_isNilpotent_ad (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (p : ℕ) [ExpChar R p] (hp : p ≠ 1) (n : ℕ) {x : L} (hx : IsNilpotent ((LieAlgebra.ad R L) x)) : IsNilpotent ((Ideal.Quotient.mk (HopfIdeal.centralAugmentationIdeal R (UniversalEnvelopingAlgebra R L) ^ n)) ((UniversalEnvelopingAlgebra.ι R) x))

In exponential characteristic p ≠ 1, every adjoint-nilpotent Lie element has nilpotent image in the quotient by the n-th power of the central augmentation ideal.

theorem TauCeti.UniversalEnvelopingAlgebra.isNilpotent_leftRegularRep_of_isNilpotent_ad (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type w} [Ring A] [Algebra R A] (p : ℕ) [ExpChar R p] (hp : p ≠ 1) (q : UniversalEnvelopingAlgebra R L →ₐ[R] A) (n : ℕ) (hq : ∀ z ∈ HopfIdeal.centralAugmentationIdeal R (UniversalEnvelopingAlgebra R L) ^ n, q z = 0) {x : L} (hx : IsNilpotent ((LieAlgebra.ad R L) x)) : IsNilpotent ((q.toLieHom.comp (UniversalEnvelopingAlgebra.ι R)).leftRegularRep x)

In exponential characteristic p ≠ 1, the left-regular Lie representation of such a target acts nilpotently on every adjoint-nilpotent Lie element.

theorem TauCeti.UniversalEnvelopingAlgebra.isNilpotent_quotient_leftRegularRep_of_isNilpotent_ad (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (p : ℕ) [ExpChar R p] (hp : p ≠ 1) (n : ℕ) {x : L} (hx : IsNilpotent ((LieAlgebra.ad R L) x)) : IsNilpotent (((Ideal.Quotient.mkₐ R (HopfIdeal.centralAugmentationIdeal R (UniversalEnvelopingAlgebra R L) ^ n)).toLieHom.comp (UniversalEnvelopingAlgebra.ι R)).leftRegularRep x)

In exponential characteristic p ≠ 1, the left-regular representation on the quotient by the n-th power of the central augmentation ideal sends every adjoint-nilpotent Lie element to a nilpotent endomorphism.