Documentation

def CartanMatrix.E₆ :

Matrix (Fin 6) (Fin 6) ℤ

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

Equations

Instances For

def CartanMatrix.E₇ :

Matrix (Fin 7) (Fin 7) ℤ

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

Equations

Instances For

def CartanMatrix.E₈ :

Matrix (Fin 8) (Fin 8) ℤ

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

Equations

Instances For

def CartanMatrix.F₄ :

Matrix (Fin 4) (Fin 4) ℤ

The Cartan matrix of type F₄. See [bourbaki1968] plate VIII, page 288.

Equations

Instances For

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

Instances For

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

Instances For

def CartanMatrix.B (n : ℕ) :

Matrix (Fin n) (Fin n) ℤ

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

Equations

Instances For

def CartanMatrix.C (n : ℕ) :

Matrix (Fin n) (Fin n) ℤ

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

Equations

Instances For

def CartanMatrix.D (n : ℕ) :

Matrix (Fin n) (Fin n) ℤ

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

Equations

Instances For

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 (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₈

theorem CartanMatrix.E₆_isSymm :

E₆.IsSymm

theorem CartanMatrix.E₇_isSymm :

E₇.IsSymm

theorem CartanMatrix.E₈_isSymm :

E₈.IsSymm

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.