Serre construction of Lie algebras from Cartan matrices

This file provides the Serre construction of Lie algebras from Cartan matrices. Given a Cartan matrix A, we construct a Lie algebra as a quotient of the free Lie algebra on generators {H_i, E_i, F_i} by the Serre 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} $$

Main definitions

• Matrix.ToLieAlgebra : The Lie algebra constructed from a Cartan matrix via Serre relations

Exceptional Lie algebras

• LieAlgebra.e₆, LieAlgebra.e₇, LieAlgebra.e₈, LieAlgebra.f₄, LieAlgebra.g₂

Classical Lie algebras

• CartanMatrix.aₙ, CartanMatrix.bₙ, CartanMatrix.cₙ, CartanMatrix.dₙ

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).

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 7--9 chapter VIII, §4.3
• J.P. Serre, Complex Semisimple Lie Algebras chapter VI, appendix

Tags

lie algebra, semi-simple, cartan matrix, serre relations

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 → Generators B
• E {B : Type v} : B → Generators B
• F {B : Type v} : B → Generators B

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

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

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

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

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

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

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

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

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

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

The terms corresponding to the ad E-relations.

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

The terms corresponding to the ad F-relations.

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

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

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

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

def Matrix.ToLieAlgebra (R : Type u) {B : Type v} [CommRing R] (CM : 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.

instance Matrix.instLieRingToLieAlgebra (R : Type u_1) {B : Type u_2} [CommRing R] (CM : Matrix B B ℤ) [DecidableEq B] : LieRing (ToLieAlgebra R CM)

instance Matrix.instInhabitedToLieAlgebra (R : Type u_1) {B : Type u_2} [CommRing R] (CM : Matrix B B ℤ) [DecidableEq B] : Inhabited (ToLieAlgebra R CM)

instance Matrix.instLieAlgebraToLieAlgebra (R : Type u_1) {B : Type u_2} [CommRing R] (CM : Matrix B B ℤ) [DecidableEq B] : LieAlgebra R (ToLieAlgebra R CM)

@[reducible, inline]

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

The exceptional split Lie algebra of type e₆.

@[reducible, inline]

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

The exceptional split Lie algebra of type e₇.

@[reducible, inline]

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

The exceptional split Lie algebra of type e₈.

@[reducible, inline]

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

The exceptional split Lie algebra of type f₄.

@[reducible, inline]

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

The exceptional split Lie algebra of type g₂.

@[reducible, inline]

noncomputable abbrev CartanMatrix.aₙ (R : Type u_1) [CommRing R] (n : ℕ) : Type u_1

The Lie algebra of type Aₙ₋₁, isomorphic to sl(n).

@[reducible, inline]

noncomputable abbrev CartanMatrix.bₙ (R : Type u_1) [CommRing R] (n : ℕ) : Type u_1

The Lie algebra of type Bₙ, isomorphic to so(2n+1).

@[reducible, inline]

noncomputable abbrev CartanMatrix.cₙ (R : Type u_1) [CommRing R] (n : ℕ) : Type u_1

The Lie algebra of type Cₙ, isomorphic to sp(2n).

@[reducible, inline]

noncomputable abbrev CartanMatrix.dₙ (R : Type u_1) [CommRing R] (n : ℕ) : Type u_1

The Lie algebra of type Dₙ, isomorphic to so(2n). Requires n ≥ 4 for non-degenerate behavior.