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)

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 (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 (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] (CM : Matrix B B ℤ) : B × B → FreeLieAlgebra R (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] (CM : Matrix B B ℤ) : B × B → FreeLieAlgebra R (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] (CM : Matrix B B ℤ) : B × B → FreeLieAlgebra R (Generators B)

The terms corresponding to the ad E-relations.

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] (CM : Matrix B B ℤ) : B × B → FreeLieAlgebra R (Generators B)

The terms corresponding to the ad F-relations.

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] (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.

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] (CM : Matrix B B ℤ) [DecidableEq B] : LieIdeal R (FreeLieAlgebra R (Generators B))

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

Equations

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

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.

Equations

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

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

Equations

• Matrix.instLieRingToLieAlgebra R CM = LieSubmodule.Quotient.lieQuotientLieRing (CartanMatrix.Relations.toIdeal 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)

Equations

• Matrix.instInhabitedToLieAlgebra R CM = LieSubmodule.Quotient.inhabited

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

Equations

• Matrix.instLieAlgebraToLieAlgebra R CM = LieSubmodule.Quotient.lieQuotientLieAlgebra (CartanMatrix.Relations.toIdeal R CM)

@[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₂

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

Equations

• CartanMatrix.aₙ R n = Matrix.ToLieAlgebra R (CartanMatrix.A 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).

Equations

• CartanMatrix.bₙ R n = Matrix.ToLieAlgebra R (CartanMatrix.B n)

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

Equations

• CartanMatrix.cₙ R n = Matrix.ToLieAlgebra R (CartanMatrix.C n)

@[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.

Equations

• CartanMatrix.dₙ R n = Matrix.ToLieAlgebra R (CartanMatrix.D n)