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 [Bou02] 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 [Bou02] 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 [Bou02] 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 [Bou02] 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 [Bou02] 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

Exceptional matrix off-diagonal entries

theorem CartanMatrix.E₆_off_diag_nonpos (i j : Fin 6) (h : i ≠ j) : E₆ i j ≤ 0

theorem CartanMatrix.E₇_off_diag_nonpos (i j : Fin 7) (h : i ≠ j) : E₇ i j ≤ 0

theorem CartanMatrix.E₈_off_diag_nonpos (i j : Fin 8) (h : i ≠ j) : E₈ i j ≤ 0

theorem CartanMatrix.F₄_off_diag_nonpos (i j : Fin 4) (h : i ≠ j) : F₄ i j ≤ 0

theorem CartanMatrix.G₂_off_diag_nonpos (i j : Fin 2) (h : i ≠ j) : G₂ i j ≤ 0

Exceptional matrix transpose properties

@[simp]

theorem CartanMatrix.E₆_transpose : E₆.transpose = E₆

@[simp]

theorem CartanMatrix.E₇_transpose : E₇.transpose = E₇

@[simp]

theorem CartanMatrix.E₈_transpose : E₈.transpose = E₈

Exceptional matrix determinants

theorem CartanMatrix.G₂_det : G₂.det = 1

theorem CartanMatrix.F₄_det : F₄.det = 1

The determinants of E₆, E₇, E₈ are 3, 2, 1 respectively. decide fails for these larger matrices without increasing the max recursion depth. We could write manual proofs (e.g., expanding via det_succ_column_zero), but prefer to wait for a more principled determinant tactic.

def Matrix.IsSimplyLaced {ι : Type u_1} (A : Matrix ι ι ℤ) : Prop

A Cartan matrix is simply laced if its off-diagonal entries are all 0 or -1.

Equations

• A.IsSimplyLaced = Pairwise fun (i j : ι) => A i j = 0 ∨ A i j = -1

instance CartanMatrix.instDecidablePredMatrixIntIsSimplyLacedOfFintypeOfDecidableEq {ι : Type u_1} [Fintype ι] [DecidableEq ι] : DecidablePred Matrix.IsSimplyLaced

Equations

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

@[simp]

theorem Matrix.isSimplyLaced_transpose {ι : Type u_1} (A : Matrix ι ι ℤ) : A.transpose.IsSimplyLaced ↔ A.IsSimplyLaced

theorem CartanMatrix.isSimplyLaced_A (n : ℕ) : (A n).IsSimplyLaced

theorem CartanMatrix.isSimplyLaced_D (n : ℕ) : (D n).IsSimplyLaced

theorem CartanMatrix.isSimplyLaced_E₆ : E₆.IsSimplyLaced

theorem CartanMatrix.isSimplyLaced_E₇ : E₇.IsSimplyLaced

theorem CartanMatrix.isSimplyLaced_E₈ : E₈.IsSimplyLaced

The Cartan matrices F₄ and G₂ are not simply laced because they contain off-diagonal entries that are neither 0 nor -1.

theorem CartanMatrix.not_isSimplyLaced_F₄ : ¬F₄.IsSimplyLaced

theorem CartanMatrix.not_isSimplyLaced_G₂ : ¬G₂.IsSimplyLaced