The inner automorphisms exp (ad x)

If x is an element of a Lie algebra L whose adjoint action ad x is nilpotent, then over a base in which the factorials are invertible the finite sum exp (ad x) = ∑ (i !)⁻¹ • (ad x)ⁱ is an automorphism of L. These are the generators of the group Int L of inner automorphisms, and they are the Lie-algebra shadow of the root subgroups of a Chevalley group: for a root vector e of a split semisimple Lie algebra, exp (ad e) is the adjoint action of x_α(1).

For an element x of an associative ℚ-algebra, this shadow is identified with the actual conjugation action of the nilpotent exponential:

exp (ad x) y = exp(x) y exp(-x).

As an application, if [x, y] = z and z commutes with both x and y, then

exp(x) exp(y) = exp(y) exp(z) exp(x).

This is the central-commutator case of the Chevalley commutator formula. It is the relation for an A₂ pair of root vectors and is also a building block for the longer rank-two formulas.

Mathlib already exponentiates a nilpotent derivation (LieDerivation.exp) and knows that a root vector is ad-nilpotent (LieAlgebra.isNilpotent_ad_of_mem_rootSpace). This file specialises the first to the inner derivations LieAlgebra.ad K L x and records the truncations of the exponential series that a hand computation needs: TauCeti.expAd_apply_of_lie_eq_zero, TauCeti.expAd_apply_of_lie_lie_eq_zero and TauCeti.expAd_apply_of_lie_lie_lie_eq_zero evaluate exp (ad x) on a vector killed by one, two or three brackets with x, which is every case that occurs inside an sl₂ triple.

The ℚ-structure hypothesis

The exponential needs to divide by factorials, so L must be a ℚ-module. Following LieDerivation.exp, this is carried by an unbundled [LieAlgebra ℚ L] hypothesis alongside the base ring K. No compatibility between the two actions is assumed, and none is needed: an additive group carries at most one ℚ-module structure, so the hypothesis names a structure rather than choosing one (Subsingleton (LieAlgebra ℚ L), in Mathlib/Algebra/Lie/Basic.lean). Where a computation does mix the two scalar actions it goes through the ℕ-action that both refine, using Nat.cast_smul_eq_nsmul. Whenever K is itself a ℚ-algebra — in particular whenever it is a field of characteristic zero — such a structure exists: TauCeti.ratLieAlgebra builds it by restricting scalars along algebraMap ℚ K.

Main definitions

• TauCeti.ratLieAlgebra: the ℚ-Lie-algebra structure on a Lie algebra over a ℚ-algebra.
• TauCeti.expAd: the inner automorphism exp (ad x) of an ad-nilpotent element x.

Main results

• TauCeti.expAd_apply_eq_sum: exp (ad x) is the truncated exponential series, truncated at any length that already annihilates the vector it is applied to.
• TauCeti.expAd_apply_of_lie_eq_zero, TauCeti.expAd_apply_of_lie_lie_eq_zero, TauCeti.expAd_apply_of_lie_lie_lie_eq_zero: the resulting one-, two- and three-term formulas.
• TauCeti.expAd_apply_self: exp (ad x) fixes x.
• TauCeti.expAd_apply_eq_exp_mul_exp_neg: on an associative algebra, exp (ad x) is conjugation by exp x.
• TauCeti.exp_mul_exp_eq_exp_mul_exp_mul_of_lie_eq_of_commute: the exponential relation for a central commutator.

References

• J. Humphreys, Introduction to Lie Algebras and Representation Theory, §2.3, where Int L is introduced.
• R. W. Carter, Simple Groups of Lie Type, §4.1.

@[instance_reducible]

noncomputable def TauCeti.ratLieAlgebra (K : Type u_1) (L : Type u_2) [CommRing K] [Algebra ℚ K] [LieRing L] [LieAlgebra K L] : LieAlgebra ℚ L

The ℚ-Lie-algebra structure on a Lie algebra L over a ℚ-algebra K, obtained by restricting scalars along algebraMap ℚ K. A field of characteristic zero is such a K.

This is deliberately a def and not an instance: K cannot be recovered from the goal LieAlgebra ℚ L, so instance search could never use it. It is what a consumer supplies with letI := TauCeti.ratLieAlgebra K L in order to apply TauCeti.expAd and everything built on it, and because LieAlgebra ℚ L is a subsingleton the choice is harmless.

Equations

• TauCeti.ratLieAlgebra K L = { toModule := Module.compHom L (algebraMap ℚ K), lie_smul := ⋯ }

noncomputable def TauCeti.expAd {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (x : L) (hx : IsNilpotent ((LieAlgebra.ad K L) x)) : L ≃ₗ⁅K⁆ L

The inner automorphism exp (ad x) attached to an element x with nilpotent adjoint action. It is LieDerivation.exp applied to the inner derivation ad x.

Equations

• TauCeti.expAd x hx = ((LieDerivation.ad K L) x).exp ⋯

theorem TauCeti.expAd_apply {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (x : L) (hx : IsNilpotent ((LieAlgebra.ad K L) x)) (y : L) : (expAd x hx) y = (IsNilpotent.exp ((LieAlgebra.ad K L) x)) y

TauCeti.expAd is the exponential of LieAlgebra.ad x.

theorem TauCeti.expAd_apply_eq_sum {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] {x : L} (hx : IsNilpotent ((LieAlgebra.ad K L) x)) {k : ℕ} {y : L} (hy : ((LieAlgebra.ad K L) x ^ k) y = 0) : (expAd x hx) y = ∑ i ∈ Finset.range k, (↑i.factorial)⁻¹ • ((LieAlgebra.ad K L) x ^ i) y

The exponential series for exp (ad x), truncated at any length k for which (ad x) ^ k already annihilates the vector y.

theorem TauCeti.expAd_apply_of_lie_eq_zero {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] {x y : L} (hx : IsNilpotent ((LieAlgebra.ad K L) x)) (hy : ⁅x, y⁆ = 0) : (expAd x hx) y = y

An element centralised by x is fixed by exp (ad x).

@[simp]

theorem TauCeti.expAd_apply_self {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (x : L) (hx : IsNilpotent ((LieAlgebra.ad K L) x)) : (expAd x hx) x = x

exp (ad x) fixes x.

theorem TauCeti.expAd_apply_of_lie_lie_eq_zero {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] {x y : L} (hx : IsNilpotent ((LieAlgebra.ad K L) x)) (hy : ⁅x, ⁅x, y⁆⁆ = 0) : (expAd x hx) y = y + ⁅x, y⁆

The two-term truncation of exp (ad x), valid on a vector killed by two brackets with x.

theorem TauCeti.expAd_apply_of_lie_lie_lie_eq_zero {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] {x y : L} (hx : IsNilpotent ((LieAlgebra.ad K L) x)) (hy : ⁅x, ⁅x, ⁅x, y⁆⁆⁆ = 0) : (expAd x hx) y = y + ⁅x, y⁆ + 2⁻¹ • ⁅x, ⁅x, y⁆⁆

The three-term truncation of exp (ad x), valid on a vector killed by three brackets with x.

Conjugation by nilpotent exponentials

@[simp]

theorem TauCeti.expAd_apply_eq_exp_mul_exp_neg {A : Type u_3} [Ring A] [Algebra ℚ A] {x y : A} (hx : IsNilpotent x) : (expAd x ⋯) y = IsNilpotent.exp x * y * IsNilpotent.exp (-x)

In an associative ℚ-algebra, the inner automorphism exp (ad x) is conjugation by the nilpotent exponential exp x.

The inverse of exp x is written explicitly as exp (-x). This form is the bridge between the Lie-algebra automorphisms above and root subgroup elements in a Chevalley group.

theorem TauCeti.exp_mul_exp_eq_exp_mul_exp_mul_of_lie_eq_of_commute {A : Type u_3} [Ring A] [Algebra ℚ A] {x y z : A} (hxy : ⁅x, y⁆ = z) (hxz : Commute x z) (hyz : Commute y z) (hx : IsNilpotent x) (hy : IsNilpotent y) : IsNilpotent.exp x * IsNilpotent.exp y = IsNilpotent.exp y * IsNilpotent.exp z * IsNilpotent.exp x

The central-commutator exponential relation. If [x, y] = z, the element z commutes with x and y, and x and y are nilpotent, then exp(x) exp(y) = exp(y) exp(z) exp(x).

For root vectors whose roots form an A₂ pair, this is the Chevalley commutator relation. The hypotheses are stated for arbitrary elements of an associative ℚ-algebra so the result also applies directly to their images in finite-dimensional representations.