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), as well as the generalized Eₙ family obtained by continuing the E-type Dynkin diagram.

Main definitions

Exceptional types and the E family

• 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 (n : ℕ) : Matrix (Fin n) (Fin n) ℤ

The generalized Cartan matrix of type Eₙ, extending E₆, E₇, E₈ by the same Dynkin-diagram pattern.

Equations

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

theorem CartanMatrix.E_six_eq : E 6 = !![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]

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

@[reducible, inline, deprecated "Use `E 6` instead" (since := "2026-07-29")]

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

Deprecated alias for E 6.

Equations

• CartanMatrix.E₆ = CartanMatrix.E 6

theorem CartanMatrix.E_seven_eq : E 7 = !![2, 0, -1, 0, 0, 0, 0; 0, 2, 0, -1, 0, 0, 0; -1, 0, 2, -1, 0, 0, 0; 0, -1, -1, 2, -1, 0, 0; 0, 0, 0, -1, 2, -1, 0; 0, 0, 0, 0, -1, 2, -1; 0, 0, 0, 0, 0, -1, 2]

E 7 is the Cartan matrix of type E₇. See [bourbaki1968] plate VI, page 281.

@[reducible, inline, deprecated "Use `E 7` instead" (since := "2026-07-29")]

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

Deprecated alias for E 7.

Equations

• CartanMatrix.E₇ = CartanMatrix.E 7

theorem CartanMatrix.E_eight_eq : E 8 = !![2, 0, -1, 0, 0, 0, 0, 0; 0, 2, 0, -1, 0, 0, 0, 0; -1, 0, 2, -1, 0, 0, 0, 0; 0, -1, -1, 2, -1, 0, 0, 0; 0, 0, 0, -1, 2, -1, 0, 0; 0, 0, 0, 0, -1, 2, -1, 0; 0, 0, 0, 0, 0, -1, 2, -1; 0, 0, 0, 0, 0, 0, -1, 2]

E 8 is the Cartan matrix of type E₈. See [bourbaki1968] plate VII, page 285.

@[reducible, inline, deprecated "Use `E 8` instead" (since := "2026-07-29")]

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

Deprecated alias for E 8.

Equations

• CartanMatrix.E₈ = CartanMatrix.E 8

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

theorem CartanMatrix.A_isSymm (n : ℕ) : (A n).IsSymm

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

theorem CartanMatrix.D_isSymm (n : ℕ) : (D n).IsSymm

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 (n : ℕ) (i : Fin n) : E n i i = 2

@[deprecated "Use `E_diag` instead" (since := "2026-08-11")]

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

@[deprecated "Use `E_diag` instead" (since := "2026-08-11")]

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

@[deprecated "Use `E_diag` instead" (since := "2026-08-11")]

theorem CartanMatrix.E₈_diag (i : Fin 8) : E 8 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 (n : ℕ) (i j : Fin n) (h : i ≠ j) : E n i j ≤ 0

@[deprecated "Use `E_off_diag_nonpos` instead" (since := "2026-08-11")]

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

@[deprecated "Use `E_off_diag_nonpos` instead" (since := "2026-08-11")]

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

@[deprecated "Use `E_off_diag_nonpos` instead" (since := "2026-08-11")]

theorem CartanMatrix.E₈_off_diag_nonpos (i j : Fin 8) (h : i ≠ j) : E 8 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 (n : ℕ) : (E n).transpose = E n

theorem CartanMatrix.E_isSymm (n : ℕ) : (E n).IsSymm

@[deprecated "Use `E_transpose` instead" (since := "2026-08-11")]

theorem CartanMatrix.E₆_transpose : (E 6).transpose = E 6

@[deprecated "Use `E_transpose` instead" (since := "2026-08-11")]

theorem CartanMatrix.E₇_transpose : (E 7).transpose = E 7

@[deprecated "Use `E_transpose` instead" (since := "2026-08-11")]

theorem CartanMatrix.E₈_transpose : (E 8).transpose = E 8

@[deprecated "Use `E_isSymm` instead" (since := "2026-08-11")]

theorem CartanMatrix.E₆_isSymm : (E 6).IsSymm

@[deprecated "Use `E_isSymm` instead" (since := "2026-08-11")]

theorem CartanMatrix.E₇_isSymm : (E 7).IsSymm

@[deprecated "Use `E_isSymm` instead" (since := "2026-08-11")]

theorem CartanMatrix.E₈_isSymm : (E 8).IsSymm

Exceptional matrix determinants

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

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

theorem CartanMatrix.det_E_add_two (n : ℕ) (hn : 4 ≤ n) : (E (n + 2)).det = 2 * (E (n + 1)).det - (E n).det

theorem CartanMatrix.E_det {n : ℕ} (hn : 3 ≤ n) : (E n).det = 9 - ↑n

The determinant of E n is 9 - n for n ≥ 3.

The determinants of E₆, E₇, E₈ are 3, 2, 1 respectively.

theorem CartanMatrix.E₆_det : (E 6).det = 3

theorem CartanMatrix.E₇_det : (E 7).det = 2

theorem CartanMatrix.E₈_det : (E 8).det = 1

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_reducible]

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

Equations

• CartanMatrix.instDecidablePredMatrixIntIsSimplyLacedOfFintypeOfDecidableEq = CartanMatrix.instDecidablePredMatrixIntIsSimplyLacedOfFintypeOfDecidableEq._aux_1

theorem Matrix.isSimplyLaced_iff_of_linearOrder {ι : Type u_1} [LinearOrder ι] (A : Matrix ι ι ℤ) (hA : A.IsSymm) : A.IsSimplyLaced ↔ ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1

@[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 (n : ℕ) : (E n).IsSimplyLaced

@[deprecated "Use `isSimplyLaced_E` instead" (since := "2026-08-11")]

theorem CartanMatrix.isSimplyLaced_E₆ : (E 6).IsSimplyLaced

@[deprecated "Use `isSimplyLaced_E` instead" (since := "2026-08-11")]

theorem CartanMatrix.isSimplyLaced_E₇ : (E 7).IsSimplyLaced

@[deprecated "Use `isSimplyLaced_E` instead" (since := "2026-08-11")]

theorem CartanMatrix.isSimplyLaced_E₈ : (E 8).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