Nilpotence of representations on enveloping quotients

On a stable enveloping quotient that is Noetherian over the coefficient ring, the multiplication-plus-derivation action is nilpotent on an element (s, h) when every ideal element acts nilpotently by multiplication and the complementary quotient operator is nilpotent. Local nilpotence of ψ(h) suffices for the latter condition. The two summands need not commute: the ideal summand is normalized by the complementary summand, so the nilpotent-extension lemma applies.

For a nilpotent split Lie extension, nilpotence of its adjoint action supplies the condition on ψ(h). Consequently every element of the extension acts nilpotently on any Noetherian stable quotient where the images of the ideal's nilradical are nilpotent. When the ambient nilradical is contained in the embedded nilradical of the ideal, nilpotence control instead follows from the multiplication action alone, without a finiteness hypothesis on the quotient. When the quotient is finite dimensional over a field, these results give nilrepresentations of the extension.

The argument combines LieSubalgebra.isNilpotent_toEnd_of_mem_lieSpan_insert_of_forall with the descended-derivation nilpotence theorem used by Ado.isNilpotent_envelopingQuotientRep_inr.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Appendix E, §E.2, Proposition E.5, for nilpotence control in the split-extension construction.

theorem Ado.isNilpotent_envelopingQuotientRep (R : Type u) (S : Type v) {H : Type w} [CommRing R] [LieRing S] [LieAlgebra R S] [LieRing H] [LieAlgebra R H] (ψ : H →ₗ⁅R⁆ LieDerivation R S S) (J : Ideal (UniversalEnvelopingAlgebra R S)) [J.IsTwoSided] (hJ : ∀ (h : H), UniversalEnvelopingAlgebra.envelopingDerivation R S (ψ h) ∈ stableDerivations R (Submodule.restrictScalars R J)) [IsNoetherian R (UniversalEnvelopingAlgebra R S ⧸ J)] (hnil : ∀ (s : S), IsNilpotent ((Ideal.Quotient.mk J) ((UniversalEnvelopingAlgebra.ι R) s))) (x : S ⋊⁅ψ⁆ H) (hH : IsNilpotent ((envelopingQuotientRep R S ψ J hJ) ((LieAlgebra.SemiDirectSum.inr ψ) x.right))) : IsNilpotent ((envelopingQuotientRep R S ψ J hJ) x)

If all ideal generators have nilpotent images and the complementary quotient operator is nilpotent, the full multiplication-plus-derivation operator is nilpotent. The quotient need only be Noetherian over the coefficient ring; the two operators need not commute.

theorem Ado.isNilpotent_envelopingQuotientRep_of_locallyNilpotent (R : Type u) (S : Type v) {H : Type w} [CommRing R] [LieRing S] [LieAlgebra R S] [LieRing H] [LieAlgebra R H] (ψ : H →ₗ⁅R⁆ LieDerivation R S S) (J : Ideal (UniversalEnvelopingAlgebra R S)) [J.IsTwoSided] (hJ : ∀ (h : H), UniversalEnvelopingAlgebra.envelopingDerivation R S (ψ h) ∈ stableDerivations R (Submodule.restrictScalars R J)) [IsNoetherian R (UniversalEnvelopingAlgebra R S ⧸ J)] (hnil : ∀ (s : S), IsNilpotent ((Ideal.Quotient.mk J) ((UniversalEnvelopingAlgebra.ι R) s))) (x : S ⋊⁅ψ⁆ H) (hψ : ∀ (s : S), ∃ (n : ℕ), (↑(ψ x.right) ^ n) s = 0) : IsNilpotent ((envelopingQuotientRep R S ψ J hJ) x)

Local nilpotence of the complementary derivation and nilpotence of all ideal-generator images imply nilpotence of the full action on a Noetherian stable enveloping quotient.

theorem Ado.isNilpotent_envelopingQuotientRep_of_isNilpotent (R : Type u) (S : Type v) {H : Type w} [CommRing R] [LieRing S] [LieAlgebra R S] [LieRing H] [LieAlgebra R H] (ψ : H →ₗ⁅R⁆ LieDerivation R S S) (J : Ideal (UniversalEnvelopingAlgebra R S)) [J.IsTwoSided] (hJ : ∀ (h : H), UniversalEnvelopingAlgebra.envelopingDerivation R S (ψ h) ∈ stableDerivations R (Submodule.restrictScalars R J)) [IsNoetherian R (UniversalEnvelopingAlgebra R S ⧸ J)] [LieRing.IsNilpotent (S ⋊⁅ψ⁆ H)] (hnil : ∀ s ∈ LieAlgebra.nilradical R S, IsNilpotent ((Ideal.Quotient.mk J) ((UniversalEnvelopingAlgebra.ι R) s))) (x : S ⋊⁅ψ⁆ H) : IsNilpotent ((envelopingQuotientRep R S ψ J hJ) x)

On a nilpotent split extension, every element acts nilpotently on the stable enveloping quotient whenever the images of the ideal's nilradical are nilpotent.

theorem Ado.isNilpotent_envelopingQuotientRep_of_mem_nilradical (R : Type u) (S : Type v) {H : Type w} [CommRing R] [LieRing S] [LieAlgebra R S] [LieRing H] [LieAlgebra R H] (ψ : H →ₗ⁅R⁆ LieDerivation R S S) (J : Ideal (UniversalEnvelopingAlgebra R S)) [J.IsTwoSided] (hJ : ∀ (h : H), UniversalEnvelopingAlgebra.envelopingDerivation R S (ψ h) ∈ stableDerivations R (Submodule.restrictScalars R J)) (hnil : ∀ s ∈ LieAlgebra.nilradical R S, IsNilpotent ((Ideal.Quotient.mk J) ((UniversalEnvelopingAlgebra.ι R) s))) (hnr : ↑(LieAlgebra.nilradical R (S ⋊⁅ψ⁆ H)) ≤ Submodule.map ↑(LieAlgebra.SemiDirectSum.inl ψ) ↑(LieAlgebra.nilradical R S)) {x : S ⋊⁅ψ⁆ H} (hx : x ∈ LieAlgebra.nilradical R (S ⋊⁅ψ⁆ H)) : IsNilpotent ((envelopingQuotientRep R S ψ J hJ) x)

If the ambient nilradical lies in the embedded nilradical of the ideal and the images of the ideal's nilradical are nilpotent, every element of the ambient nilradical acts nilpotently. This includes equality of the two nilradicals and requires no finiteness of the quotient.