The adjoint action of an associative algebra and the Frobenius

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.

The main theorem of this file is that the two agree along the Frobenius: in exponential characteristic p,

ad R A (a ^ p ^ n) = ad R A a ^ p ^ n.

The reason is that ad R A a is the difference of the commuting endomorphisms LinearMap.mulLeft R a and LinearMap.mulRight R a, so the Frobenius of Module.End R A is additive on it, and each of the two factors is a multiplication operator by a power of a. The identity is characteristic-free in the exponential sense: for p = 1 it is a tautology, and its content is the prime case.

Two consequences follow at once. Iterating the commutator p ^ n times collapses to a single commutator with a ^ p ^ n (ad_pow_expChar_pow_apply), and, when p is a genuine prime, ad R A a is nilpotent exactly when some Frobenius power a ^ p ^ n is central (isNilpotent_ad_iff_exists_pow_expChar_pow_mem_center). The forward direction of that equivalence is the passage from adjoint nilpotence to a central p-th power that the positive-characteristic half of Ado--Iwasawa runs on.

The characteristic-free iterated-commutator expansion that this identity collapses, ad_pow_apply, is in TauCeti.Algebra.Lie.AdjointAction.Basic.

Main statements

• TauCeti.LieAlgebra.ad_pow_expChar_pow: the Frobenius commutator identity.
• TauCeti.LieAlgebra.ad_pow_expChar_pow_eq_zero_iff: the p ^ n-th power of ad R A a vanishes exactly when a ^ p ^ n is central.
• TauCeti.LieAlgebra.isNilpotent_ad_iff_exists_pow_expChar_pow_mem_center: in characteristic p, adjoint nilpotence is centrality of a Frobenius power.

References

The formal source is Mathlib/FieldTheory/JacobsonNoether.lean, whose JacobsonNoether.exist_pow_eq_zero_of_le carries out this Frobenius calculation inline, for a division algebra purely inseparable over its centre and phrased with Function.iterate, from the same four ingredients used here: sub_pow_expChar_pow_of_commute, LinearMap.commute_mulLeft_right, LinearMap.pow_mulLeft and LinearMap.pow_mulRight. This file generalizes that calculation to an arbitrary associative algebra and states it as a theorem about powers in Module.End R A.

• G. Hochschild, An Addition to Ado's Theorem, Proc. Amer. Math. Soc. 17 (1966), 531--533.
• N. Jacobson, Lie Algebras, Interscience (1962), Chapter V.

@[simp]

theorem TauCeti.LieAlgebra.ad_pow_expChar_pow {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (p : ℕ) [ExpChar A p] (a : A) (n : ℕ) : (LieAlgebra.ad R A) (a ^ p ^ n) = (LieAlgebra.ad R A) a ^ p ^ n

The Frobenius commutator identity. In exponential characteristic p, taking the p ^ n-th power in the algebra A and iterating the commutator p ^ n times in Module.End R A give the same endomorphism.

@[simp]

theorem TauCeti.LieAlgebra.ad_pow_expChar_pow_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (p : ℕ) [ExpChar A p] (a b : A) (n : ℕ) : ((LieAlgebra.ad R A) a ^ p ^ n) b = a ^ p ^ n * b - b * a ^ p ^ n

Iterating the commutator with a exactly p ^ n times collapses to a single commutator with a ^ p ^ n. This is the concrete reading of ad_pow_expChar_pow, and the reason the expansion ad_pow_apply degenerates in characteristic p.

@[simp]

theorem TauCeti.LieAlgebra.ad_pow_expChar_pow_eq_zero_iff {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (p : ℕ) [ExpChar A p] (a : A) (n : ℕ) : (LieAlgebra.ad R A) a ^ p ^ n = 0 ↔ a ^ p ^ n ∈ Subalgebra.center R A

The quantitative form of the Frobenius commutator identity. The p ^ n-fold commutator with a vanishes exactly when the Frobenius power a ^ p ^ n is central. Both nilpotence statements below are this equivalence with the exponent quantified.

theorem TauCeti.LieAlgebra.isNilpotent_ad_of_pow_expChar_pow_mem_center {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (p : ℕ) [ExpChar A p] {a : A} {n : ℕ} (h : a ^ p ^ n ∈ Subalgebra.center R A) : IsNilpotent ((LieAlgebra.ad R A) a)

If some Frobenius power a ^ p ^ n is central, then ad R A a is nilpotent.

theorem TauCeti.LieAlgebra.exists_pow_expChar_pow_mem_center_of_isNilpotent_ad {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (p : ℕ) [ExpChar A p] (hp : p ≠ 1) {a : A} (h : IsNilpotent ((LieAlgebra.ad R A) a)) : ∃ (n : ℕ), a ^ p ^ n ∈ Subalgebra.center R A

If ad R A a is nilpotent and p is a genuine prime characteristic, then some Frobenius power a ^ p ^ n is central.

theorem TauCeti.LieAlgebra.isNilpotent_ad_iff_exists_pow_expChar_pow_mem_center {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (p : ℕ) [ExpChar A p] (hp : p ≠ 1) (a : A) : IsNilpotent ((LieAlgebra.ad R A) a) ↔ ∃ (n : ℕ), a ^ p ^ n ∈ Subalgebra.center R A

Adjoint nilpotence is centrality of a Frobenius power. Over an algebra of prime characteristic p, the inner derivation attached to a is nilpotent exactly when one of the elements a ^ p ^ n is central. The forward direction is the step that, inside a universal enveloping algebra, produces the central p-polynomial attached to an ad-nilpotent element.