The filtration of a centralizer by powers of ad e

Let L be a Lie algebra and e ∈ L. The centralizer ker (ad e) of e carries the decreasing filtration 𝔲ₖ = ker (ad e) ⊓ range ((ad e) ^ k). Over a field of characteristic zero it is compatible with brackets, ⁅𝔲ᵢ, 𝔲ⱼ⁆ ⊆ 𝔲ᵢ₊ⱼ, by the Leibniz rule for powers of the derivation ad e: in the expansion of (ad e) ^ (i + j) ⁅a, b⁆ only the term ⁅(ad e) ^ i a, (ad e) ^ j b⁆ survives when (ad e) ^ (i + 1) kills a and (ad e) ^ (j + 1) kills b.

The first step 𝔲₁ = ker (ad e) ⊓ [e, L] consists of ad-nilpotent elements in finite dimension: this is Jacobson's lemma LinearMap.isNilpotent_lie_of_lie_lie_eq_zero for the adjoint representation.

Main results

• TauCeti.antitone_ker_inf_range_pow: the filtration is decreasing.
• TauCeti.lie_mem_ker_inf_range_pow_add: the filtration is compatible with brackets.
• TauCeti.isNilpotent_ad_lie_of_lie_lie_eq_zero: Jacobson's lemma for the adjoint representation.
• TauCeti.isNilpotent_ad_of_mem_ker_inf_range: every element of ker (ad e) ⊓ [e, L] is ad-nilpotent.

References

• N. Jacobson, Lie Algebras, Interscience, 1962, Chapter III, §11.

theorem TauCeti.antitone_ker_inf_range_pow {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (e : L) : Antitone fun (k : ℕ) => LinearMap.ker ((LieAlgebra.ad R L) e) ⊓ LinearMap.range ((LieAlgebra.ad R L) e ^ k)

The filtration ker (ad e) ⊓ range ((ad e) ^ k) of the centralizer of e is decreasing.

theorem TauCeti.lie_mem_ker_inf_range_pow_add {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] {e x y : L} {i j : ℕ} (hx : x ∈ LinearMap.ker ((LieAlgebra.ad K L) e) ⊓ LinearMap.range ((LieAlgebra.ad K L) e ^ i)) (hy : y ∈ LinearMap.ker ((LieAlgebra.ad K L) e) ⊓ LinearMap.range ((LieAlgebra.ad K L) e ^ j)) : ⁅x, y⁆ ∈ LinearMap.ker ((LieAlgebra.ad K L) e) ⊓ LinearMap.range ((LieAlgebra.ad K L) e ^ (i + j))

The filtration ker (ad e) ⊓ range ((ad e) ^ k) of the centralizer of e is compatible with brackets: a bracket of an element of the i-th step with an element of the j-th step lies in the (i + j)-th step.

theorem TauCeti.isNilpotent_ad_lie_of_lie_lie_eq_zero {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {e a : L} (h : ⁅e, ⁅e, a⁆⁆ = 0) : IsNilpotent ((LieAlgebra.ad K L) ⁅e, a⁆)

Jacobson's lemma for the adjoint representation. In a finite-dimensional Lie algebra over a field of characteristic zero, if ⁅e, ⁅e, a⁆⁆ = 0 then ad ⁅e, a⁆ is nilpotent. In particular every element of ker (ad e) ⊓ [e, L] is ad-nilpotent.

theorem TauCeti.isNilpotent_ad_of_mem_ker_inf_range {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {e y : L} (hy : y ∈ LinearMap.ker ((LieAlgebra.ad K L) e) ⊓ LinearMap.range ((LieAlgebra.ad K L) e)) : IsNilpotent ((LieAlgebra.ad K L) y)

Every element of ker (ad e) ⊓ [e, L] is ad-nilpotent.