Cartan matrices

This file defines Cartan matrices for simple Lie algebras, both the exceptional types (E₆, E₇, E₈, F₄, G₂) and the classical infinite families (A, B, C, D).

Main definitions

Exceptional types

• CartanMatrix.E₆ : The Cartan matrix of type E₆
• CartanMatrix.E₇ : The Cartan matrix of type E₇
• CartanMatrix.E₈ : The Cartan matrix of type E₈
• CartanMatrix.F₄ : The Cartan matrix of type F₄
• CartanMatrix.G₂ : The Cartan matrix of type G₂

Classical types

• CartanMatrix.A : The Cartan matrix of type Aₙ₋₁ (corresponding to sl(n))
• CartanMatrix.B : The Cartan matrix of type Bₙ (corresponding to so(2n+1))
• CartanMatrix.C : The Cartan matrix of type Cₙ (corresponding to sp(2n))
• CartanMatrix.D : The Cartan matrix of type Dₙ (corresponding to so(2n))

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6 plates I -- IX
• [J. Humphreys, Introduction to Lie Algebras and Representation Theory] Chapter 11

Tags

cartan matrix, lie algebra, dynkin diagram

Exceptional Cartan matrices

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

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

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.

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.

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.

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. We use the transpose of Bourbaki's matrix for consistency with F₄.

Equations

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

Classical Cartan matrices

def CartanMatrix.A (n : ℕ) : Matrix (Fin n) (Fin n) ℤ

The Cartan matrix of type Aₙ₋₁ (rank n-1, corresponding to sl(n)).

Equations

• CartanMatrix.A n = Matrix.of fun (i j : Fin n) => if i = j then 2 else if ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i then -1 else 0

def CartanMatrix.B (n : ℕ) : Matrix (Fin n) (Fin n) ℤ

The Cartan matrix of type Bₙ (rank n, corresponding to so(2n+1)).

Equations

• CartanMatrix.B n = Matrix.of fun (i j : Fin n) => if i = j then 2 else if ↑i + 1 = ↑j then if ↑j = n - 1 then -2 else -1 else if ↑j + 1 = ↑i then -1 else 0

def CartanMatrix.C (n : ℕ) : Matrix (Fin n) (Fin n) ℤ

The Cartan matrix of type Cₙ (rank n, corresponding to sp(2n)).

Equations

• CartanMatrix.C n = Matrix.of fun (i j : Fin n) => if i = j then 2 else if ↑i + 1 = ↑j then -1 else if ↑j + 1 = ↑i then if ↑i = n - 1 then -2 else -1 else 0

def CartanMatrix.D (n : ℕ) : Matrix (Fin n) (Fin n) ℤ

The Cartan matrix of type Dₙ (rank n, corresponding to so(2n)).

Equations

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

Properties

@[simp]

theorem CartanMatrix.A_diag (n : ℕ) : (A n).diag = 2

@[simp]

theorem CartanMatrix.B_diag (n : ℕ) (i : Fin n) : B n i i = 2

@[simp]

theorem CartanMatrix.C_diag (n : ℕ) (i : Fin n) : C n i i = 2

@[simp]

theorem CartanMatrix.D_diag (n : ℕ) (i : Fin n) : D n i i = 2

theorem CartanMatrix.A_apply_le_zero_of_ne (n : ℕ) (i j : Fin n) (h : i ≠ j) : A n i j ≤ 0

theorem CartanMatrix.B_off_diag_nonpos (n : ℕ) (i j : Fin n) (h : i ≠ j) : B n i j ≤ 0

theorem CartanMatrix.C_off_diag_nonpos (n : ℕ) (i j : Fin n) (h : i ≠ j) : C n i j ≤ 0

theorem CartanMatrix.D_off_diag_nonpos (n : ℕ) (i j : Fin n) (h : i ≠ j) : D n i j ≤ 0

Transpose properties

@[simp]

theorem CartanMatrix.A_transpose (n : ℕ) : (A n).transpose = A n

@[simp]

theorem CartanMatrix.B_transpose (n : ℕ) : (B n).transpose = C n

@[simp]

theorem CartanMatrix.C_transpose (n : ℕ) : (C n).transpose = B n

@[simp]

theorem CartanMatrix.D_transpose (n : ℕ) : (D n).transpose = D n

Small cases

theorem CartanMatrix.A_one : A 1 = !![2]

theorem CartanMatrix.A_two : A 2 = !![2, -1; -1, 2]

theorem CartanMatrix.A_three : A 3 = !![2, -1, 0; -1, 2, -1; 0, -1, 2]

theorem CartanMatrix.B_one : B 1 = A 1

theorem CartanMatrix.C_one : C 1 = A 1

theorem CartanMatrix.D_one : D 1 = A 1

theorem CartanMatrix.D_two : D 2 = !![2, 0; 0, 2]

theorem CartanMatrix.B_two : B 2 = !![2, -2; -1, 2]

theorem CartanMatrix.C_two : C 2 = !![2, -1; -2, 2]

theorem CartanMatrix.D_three : D 3 = !![2, -1, -1; -1, 2, 0; -1, 0, 2]

theorem CartanMatrix.D_three' : (Matrix.reindex ((↑[0, 1]).formPerm ⋯) ((↑[0, 1]).formPerm ⋯)) (D 3) = A 3

theorem CartanMatrix.D_four : D 4 = !![2, -1, 0, 0; -1, 2, -1, -1; 0, -1, 2, 0; 0, -1, 0, 2]

Exceptional matrix diagonal entries

@[simp]

theorem CartanMatrix.E₆_diag (i : Fin 6) : E₆ i i = 2

@[simp]

theorem CartanMatrix.E₇_diag (i : Fin 7) : E₇ i i = 2

@[simp]

theorem CartanMatrix.E₈_diag (i : Fin 8) : E₈ i i = 2

@[simp]

theorem CartanMatrix.F₄_diag (i : Fin 4) : F₄ i i = 2

@[simp]

theorem CartanMatrix.G₂_diag (i : Fin 2) : G₂ i i = 2