# Documentation

Mathlib.Algebra.Lie.CartanMatrix

# Lie algebras from Cartan matrices #

Split semi-simple Lie algebras are uniquely determined by their Cartan matrix. Indeed, if A is an l × l Cartan matrix, the corresponding Lie algebra may be obtained as the Lie algebra on 3l generators: $H_1, H_2, \ldots H_l, E_1, E_2, \ldots, E_l, F_1, F_2, \ldots, F_l$ subject to the following relations: \begin{align} [H_i, H_j] &= 0\ [E_i, F_i] &= H_i\ [E_i, F_j] &= 0 \quad\text{if i \ne j}\ [H_i, E_j] &= A_{ij}E_j\ [H_i, F_j] &= -A_{ij}F_j\ ad(E_i)^{1 - A_{ij}}(E_j) &= 0 \quad\text{if i \ne j}\ ad(F_i)^{1 - A_{ij}}(F_j) &= 0 \quad\text{if i \ne j}\ \end{align}

In this file we provide the above construction. It is defined for any square matrix of integers but the results for non-Cartan matrices should be regarded as junk.

Recall that a Cartan matrix is a square matrix of integers A such that:

• For diagonal values we have: A i i = 2.
• For off-diagonal values (i ≠ j) we have: A i j ∈ {-3, -2, -1, 0}.
• A i j = 0 ↔ A j i = 0.
• There exists a diagonal matrix D over ℝ such that D * A * D⁻¹ is symmetric positive definite.

## Alternative construction #

This construction is sometimes performed within the free unital associative algebra FreeAlgebra R X, rather than within the free Lie algebra FreeLieAlgebra R X, as we do here. However the difference is illusory since the construction stays inside the Lie subalgebra of FreeAlgebra R X generated by X, and this is naturally isomorphic to FreeLieAlgebra R X (though the proof of this seems to require Poincaré–Birkhoff–Witt).

## Definitions of exceptional Lie algebras #

This file also contains the Cartan matrices of the exceptional Lie algebras. By using these in the above construction, it thus provides definitions of the exceptional Lie algebras. These definitions make sense over any commutative ring. When the ring is ℝ, these are the split real forms of the exceptional semisimple Lie algebras.

## Main definitions #

• Matrix.ToLieAlgebra
• CartanMatrix.E₆
• CartanMatrix.E₇
• CartanMatrix.E₈
• CartanMatrix.F₄
• CartanMatrix.G₂
• LieAlgebra.e₆
• LieAlgebra.e₇
• LieAlgebra.e₈
• LieAlgebra.f₄
• LieAlgebra.g₂

## Tags #

lie algebra, semi-simple, cartan matrix