13.1. Lie algebras and their representations🔗

Mathlib contains a theory of Lie algebras and their representations.

The following adds a Lie algebra to the Lean environment

variable {R L : Type*} [CommRing R]
  [LieRing L] [LieAlgebra R L]

Lie algebras use a bracket notation: the product of x and y is written ⁅x, y⁆. Thus the Jacobi identity appears as:

example (x y z : L) :
    ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0 :=
  lie_jacobi x y z

The following adds a representation of a Lie algebra L on a module M to the Lean environment

variable {M : Type*}
  [AddCommGroup M] [Module R M]
  [LieRingModule L M] [LieModule R L M]

This data determines a morphism of Lie algebras L → End(M). In Mathlib this morphism appears as LieModule.toEnd. More generally morphisms and isomorphisms between any Lie algebras may be added to the environment using a special notation as follows

variable {L' : Type*}
  [LieRing L'] [LieAlgebra R L']
  (φ : L →ₗ⁅R⁆ L') (e : L ≃ₗ⁅R⁆ L')