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) = ⊥