The iterated adjoint action of an associative algebra

Let A be an associative R-algebra, bracketed by its ring commutator, and let ad R A a : Module.End R A be the inner derivation b ↦ ⁅a, b⁆. Two powers are in play and they must not be confused: a ^ n is a power in the ring A, while ad R A a ^ n is a power in the endomorphism ring Module.End R A, that is, the n-fold iterated commutator with a.

This file expands the second kind over an arbitrary commutative ring R. Since ad R A a is the difference of the commuting endomorphisms LinearMap.mulLeft R a and LinearMap.mulRight R a, the n-fold iterated commutator is their binomial expansion: a sum of the products a ^ m * b * (-a) ^ (n - m), with the sign absorbed into (-a) ^ (n - m) rather than carried as a separate (-1) ^ k. Alongside it, ad_eq_zero_iff_mem_center records that the adjoint action of a vanishes exactly when a is central.

Over an algebra of exponential characteristic p the expansion collapses at n = p ^ e, which is the subject of TauCeti.Algebra.Lie.AdjointAction.Frobenius.

Main statements

• TauCeti.LieAlgebra.ad_pow_eq_sum and TauCeti.LieAlgebra.ad_pow_apply: the iterated-commutator expansion of ad R A a ^ n, at operator level and evaluated.
• TauCeti.LieAlgebra.ad_eq_zero_iff_mem_center: ad R A a vanishes exactly on the centre.

References

• N. Jacobson, Lie Algebras, Interscience (1962), Chapter V.

theorem TauCeti.LieAlgebra.ad_pow_eq_sum {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (a : A) (n : ℕ) : (LieAlgebra.ad R A) a ^ n = ∑ m ∈ Finset.range (n + 1), n.choose m • (LinearMap.mulLeft R (a ^ m) * LinearMap.mulRight R ((-a) ^ (n - m)))

The iterated-commutator expansion, at operator level. Left and right multiplication by a commute by associativity, so the n-fold commutator with a is their binomial expansion. The sign that usually accompanies such an expansion is absorbed into (-a) ^ (n - m).

theorem TauCeti.LieAlgebra.ad_pow_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (a b : A) (n : ℕ) : ((LieAlgebra.ad R A) a ^ n) b = ∑ m ∈ Finset.range (n + 1), n.choose m • (a ^ m * b * (-a) ^ (n - m))

The iterated-commutator expansion, evaluated. This is ad_pow_eq_sum applied to an element: the n-fold commutator of a with b is the binomial sum of the products a ^ m * b * (-a) ^ (n - m).

@[simp]

theorem TauCeti.LieAlgebra.ad_eq_zero_iff_mem_center {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (a : A) : (LieAlgebra.ad R A) a = 0 ↔ a ∈ Subalgebra.center R A

The adjoint action of a vanishes exactly when a is central.