Adjoint action of a Lie algebra on itself

This file defines the adjoint action of a Lie algebra on itself, and establishes basic properties.

Main definitions

• LieDerivation.ad: The adjoint action of a Lie algebra L on itself, seen as a morphism of Lie algebras from L to the Lie algebra of its derivations. The adjoint action is also defined in the Mathlib.Algebra.Lie.OfAssociative.lean file, under the name LieAlgebra.ad, as the morphism with values in the endormophisms of L.

Main statements

• LieDerivation.coe_ad_apply_eq_ad_apply: when seen as endomorphisms, both definitions coincide,
• LieDerivation.ad_ker_eq_center: the kernel of the adjoint action is the center of L,
• LieDerivation.lie_der_ad_eq_ad_der: the commutator of a derivation D and ad x is ad (D x),
• LieDerivation.ad_isIdealMorphism: the range of the adjoint action is an ideal of the derivations.

def LieDerivation.ad (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : L →ₗ⁅R⁆ LieDerivation R L L

The adjoint action of a Lie algebra L on itself, seen as a morphism of Lie algebras from L to its derivations. Note the minus sign: this is chosen to so that ad ⁅x, y⁆ = ⁅ad x, ad y⁆.

Equations

• LieDerivation.ad R L = { toLinearMap := -LieDerivation.inner R L L, map_lie' := ⋯ }

@[simp]

theorem LieDerivation.ad_apply_apply (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (a a✝ : L) : ((ad R L) a) a✝ = ⁅a, a✝⁆

@[simp]

theorem LieDerivation.coe_ad_apply_eq_ad_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : ↑((ad R L) x) = (LieAlgebra.ad R L) x

The definitions LieDerivation.ad and LieAlgebra.ad agree.

theorem LieDerivation.ad_apply_lieDerivation {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (D : LieDerivation R L L) : (ad R L) (D x) = -⁅x, D⁆

theorem LieDerivation.lie_ad {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (D : LieDerivation R L L) : ⁅(ad R L) x, D⁆ = ⁅x, D⁆

theorem LieDerivation.ad_ker_eq_center (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : (ad R L).ker = LieAlgebra.center R L

The kernel of the adjoint action on a Lie algebra is equal to its center.

theorem LieDerivation.injective_ad_of_center_eq_bot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (h : LieAlgebra.center R L = ⊥) : Function.Injective ⇑(ad R L)

If the center of a Lie algebra is trivial, then the adjoint action is injective.

theorem LieDerivation.lie_der_ad_eq_ad_der {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (x : L) : ⁅D, (ad R L) x⁆ = (ad R L) (D x)

The commutator of a derivation D and a derivation of the form ad x is ad (D x).

theorem LieDerivation.ad_isIdealMorphism (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : (ad R L).IsIdealMorphism

The range of the adjoint action homomorphism from a Lie algebra L to the Lie algebra of its derivations is an ideal of the latter.

theorem LieDerivation.mem_ad_idealRange_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {D : LieDerivation R L L} : D ∈ (ad R L).idealRange ↔ ∃ (x : L), (ad R L) x = D

A derivation D belongs to the ideal range of the adjoint action iff it is of the form ad x for some x in the Lie algebra L.

theorem LieDerivation.maxTrivSubmodule_eq_bot_of_center_eq_bot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (h : LieAlgebra.center R L = ⊥) : LieModule.maxTrivSubmodule R L (LieDerivation R L L) = ⊥