English
For Lie algebras L, the nilpotence of the ad-range of the adjoint action satisfies IsNilpotent((ad_R L).range) iff IsNilpotent L.
Русский
Для алгебр Ли L выполнено: нильпотентность диапазона ад-оператора эквивалентна нильпотентности самой L.
LaTeX
$$$\mathrm{IsNilpotent}\bigl((\operatorname{ad} R L).\mathrm{range}\bigr) \iff \mathrm{IsNilpotent} L$$$
Lean4
/-- Note that this result is not quite a special case of
`LieModule.isNilpotent_range_toEnd_iff` which concerns nilpotency of the
`(ad R L).range`-module `L`, whereas this result concerns nilpotency of the `(ad R L).range`-module
`(ad R L).range`. -/
@[simp]
theorem isNilpotent_range_ad_iff : IsNilpotent (ad R L).range ↔ IsNilpotent L :=
by
refine ⟨fun h => ?_, ?_⟩
· have : (ad R L).ker = center R L := by simp
exact
LieAlgebra.nilpotent_of_nilpotent_quotient (le_of_eq this)
((ad R L).quotKerEquivRange.nilpotent_iff_equiv_nilpotent.mpr h)
· intro h
exact (ad R L).isNilpotent_range
