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.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6 plates V -- IX, pages 275--290

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 7--9 chapter VIII, §4.3

• J.P. Serre, Complex Semisimple Lie Algebras chapter VI, appendix

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

inductive CartanMatrix.Generators (B : Type v) : Type v

The generators of the free Lie algebra from which we construct the Lie algebra of a Cartan matrix as a quotient.

• H: {B : Type v} → B → CartanMatrix.Generators B
• E: {B : Type v} → B → CartanMatrix.Generators B
• F: {B : Type v} → B → CartanMatrix.Generators B

instance CartanMatrix.instInhabitedGenerators (B : Type v) [Inhabited B] : Inhabited (CartanMatrix.Generators B)

Equations

• CartanMatrix.instInhabitedGenerators B = { default := CartanMatrix.Generators.H default }

def CartanMatrix.Relations.HH (R : Type u) {B : Type v} [CommRing R] : B × B → FreeLieAlgebra R (CartanMatrix.Generators B)

The terms corresponding to the ⁅H, H⁆-relations.

Equations

• CartanMatrix.Relations.HH R = Function.uncurry fun (i j : B) => ⁅(FreeLieAlgebra.of R ∘ CartanMatrix.Generators.H) i, (FreeLieAlgebra.of R ∘ CartanMatrix.Generators.H) j⁆

def CartanMatrix.Relations.EF (R : Type u) {B : Type v} [CommRing R] [DecidableEq B] : B × B → FreeLieAlgebra R (CartanMatrix.Generators B)

The terms corresponding to the ⁅E, F⁆-relations.

Equations

• One or more equations did not get rendered due to their size.

def CartanMatrix.Relations.HE (R : Type u) {B : Type v} [CommRing R] (A : Matrix B B ℤ) : B × B → FreeLieAlgebra R (CartanMatrix.Generators B)

The terms corresponding to the ⁅H, E⁆-relations.

Equations

• One or more equations did not get rendered due to their size.

def CartanMatrix.Relations.HF (R : Type u) {B : Type v} [CommRing R] (A : Matrix B B ℤ) : B × B → FreeLieAlgebra R (CartanMatrix.Generators B)

The terms corresponding to the ⁅H, F⁆-relations.

Equations

• One or more equations did not get rendered due to their size.

def CartanMatrix.Relations.adE (R : Type u) {B : Type v} [CommRing R] (A : Matrix B B ℤ) : B × B → FreeLieAlgebra R (CartanMatrix.Generators B)

The terms corresponding to the ad E-relations.

Note that we use Int.toNat so that we can take the power and that we do not bother restricting to the case i ≠ j since these relations are zero anyway. We also defensively ensure this with adE_of_eq_eq_zero.

Equations

• One or more equations did not get rendered due to their size.

def CartanMatrix.Relations.adF (R : Type u) {B : Type v} [CommRing R] (A : Matrix B B ℤ) : B × B → FreeLieAlgebra R (CartanMatrix.Generators B)

The terms corresponding to the ad F-relations.

See also adE docstring.

Equations

• One or more equations did not get rendered due to their size.

def CartanMatrix.Relations.toSet (R : Type u) {B : Type v} [CommRing R] (A : Matrix B B ℤ) [DecidableEq B] : Set (FreeLieAlgebra R (CartanMatrix.Generators B))

The union of all the relations as a subset of the free Lie algebra.

Equations

• One or more equations did not get rendered due to their size.

def CartanMatrix.Relations.toIdeal (R : Type u) {B : Type v} [CommRing R] (A : Matrix B B ℤ) [DecidableEq B] : LieIdeal R (FreeLieAlgebra R (CartanMatrix.Generators B))

The ideal of the free Lie algebra generated by the relations.

Equations

• CartanMatrix.Relations.toIdeal R A = LieSubmodule.lieSpan R (FreeLieAlgebra R (CartanMatrix.Generators B)) (CartanMatrix.Relations.toSet R A)

def Matrix.ToLieAlgebra (R : Type u) {B : Type v} [CommRing R] (A : Matrix B B ℤ) [DecidableEq B] : Type (max (max v u) u v)

The Lie algebra corresponding to a Cartan matrix.

Note that it is defined for any matrix of integers. Its value for non-Cartan matrices should be regarded as junk.

Equations

• Matrix.ToLieAlgebra R A = (FreeLieAlgebra R (CartanMatrix.Generators B) ⧸ CartanMatrix.Relations.toIdeal R A)

instance Matrix.ToLieAlgebra.instLieRing (R : Type u) {B : Type v} [CommRing R] (A : Matrix B B ℤ) [DecidableEq B] : LieRing (Matrix.ToLieAlgebra R A)

Equations

• Matrix.ToLieAlgebra.instLieRing R A = inferInstanceAs (LieRing (FreeLieAlgebra R (CartanMatrix.Generators B) ⧸ CartanMatrix.Relations.toIdeal R A))

instance Matrix.ToLieAlgebra.instInhabited (R : Type u) {B : Type v} [CommRing R] (A : Matrix B B ℤ) [DecidableEq B] : Inhabited (Matrix.ToLieAlgebra R A)

Equations

• Matrix.ToLieAlgebra.instInhabited R A = inferInstanceAs (Inhabited (FreeLieAlgebra R (CartanMatrix.Generators B) ⧸ CartanMatrix.Relations.toIdeal R A))

instance Matrix.ToLieAlgebra.instLieAlgebra (R : Type u) {B : Type v} [CommRing R] (A : Matrix B B ℤ) [DecidableEq B] : LieAlgebra R (Matrix.ToLieAlgebra R A)

Equations

• Matrix.ToLieAlgebra.instLieAlgebra R A = inferInstanceAs (LieAlgebra R (FreeLieAlgebra R (CartanMatrix.Generators B) ⧸ CartanMatrix.Relations.toIdeal R A))

def CartanMatrix.E₆ : Matrix (Fin 6) (Fin 6) ℤ

The Cartan matrix of type e₆. See [bourbaki1968] plate V, page 277.

The corresponding Dynkin diagram is:

            o
            |
o --- o --- o --- o --- o

Equations

• CartanMatrix.E₆ = !![2, 0, -1, 0, 0, 0; 0, 2, 0, -1, 0, 0; -1, 0, 2, -1, 0, 0; 0, -1, -1, 2, -1, 0; 0, 0, 0, -1, 2, -1; 0, 0, 0, 0, -1, 2]

def CartanMatrix.E₇ : Matrix (Fin 7) (Fin 7) ℤ

The Cartan matrix of type e₇. See [bourbaki1968] plate VI, page 281.

The corresponding Dynkin diagram is:

            o
            |
o --- o --- o --- o --- o --- o

Equations

• One or more equations did not get rendered due to their size.

def CartanMatrix.E₈ : Matrix (Fin 8) (Fin 8) ℤ

The Cartan matrix of type e₈. See [bourbaki1968] plate VII, page 285.

The corresponding Dynkin diagram is:

            o
            |
o --- o --- o --- o --- o --- o --- o

Equations

• One or more equations did not get rendered due to their size.

def CartanMatrix.F₄ : Matrix (Fin 4) (Fin 4) ℤ

The Cartan matrix of type f₄. See [bourbaki1968] plate VIII, page 288.

The corresponding Dynkin diagram is:

o --- o =>= o --- o

Equations

• CartanMatrix.F₄ = !![2, -1, 0, 0; -1, 2, -2, 0; 0, -1, 2, -1; 0, 0, -1, 2]

def CartanMatrix.G₂ : Matrix (Fin 2) (Fin 2) ℤ

The Cartan matrix of type g₂. See [bourbaki1968] plate IX, page 290.

The corresponding Dynkin diagram is:

o ≡>≡ o

Actually we are using the transpose of Bourbaki's matrix. This is to make this matrix consistent with CartanMatrix.F₄, in the sense that all non-zero values below the diagonal are -1.

Equations

• CartanMatrix.G₂ = !![2, -3; -1, 2]

@[reducible, inline]

abbrev LieAlgebra.e₆ (R : Type u) [CommRing R] : Type u

The exceptional split Lie algebra of type e₆.

Equations

• LieAlgebra.e₆ R = Matrix.ToLieAlgebra R CartanMatrix.E₆

@[reducible, inline]

abbrev LieAlgebra.e₇ (R : Type u) [CommRing R] : Type u

The exceptional split Lie algebra of type e₇.

Equations

• LieAlgebra.e₇ R = Matrix.ToLieAlgebra R CartanMatrix.E₇

@[reducible, inline]

abbrev LieAlgebra.e₈ (R : Type u) [CommRing R] : Type u

The exceptional split Lie algebra of type e₈.

Equations

• LieAlgebra.e₈ R = Matrix.ToLieAlgebra R CartanMatrix.E₈

@[reducible, inline]

abbrev LieAlgebra.f₄ (R : Type u) [CommRing R] : Type u

The exceptional split Lie algebra of type f₄.

Equations

• LieAlgebra.f₄ R = Matrix.ToLieAlgebra R CartanMatrix.F₄

@[reducible, inline]

abbrev LieAlgebra.g₂ (R : Type u) [CommRing R] : Type u

The exceptional split Lie algebra of type g₂.

Equations

• LieAlgebra.g₂ R = Matrix.ToLieAlgebra R CartanMatrix.G₂