Documentation

TauCeti.LinearAlgebra.Matrix.Cartan.Classical

The determinants of the classical Cartan matrices of types A, B and C #

Mathlib computes the determinant of CartanMatrix.E n, and hence of the three exceptional matrices E₆, E₇ and E₈, and evaluates F₄ and G₂ directly, but leaves the classical families untouched. This file computes

(CartanMatrix.A n).det = n + 1,   (CartanMatrix.B n).det = 2,   (CartanMatrix.C n).det = 2,

the last two for 0 < n. The remaining classical family is type D, whose determinant is CartanMatrix.D_det in TauCeti.LinearAlgebra.IntegralLattice.RootLattice.TypeD.SimpleRoots, where it is read off the checkerboard lattice.

No recursion in the rank is needed for any of the three. Weighting row k by k + 1 and summing over k ≤ i turns CartanMatrix.A n into an upper triangular matrix whose i-th diagonal entry is i + 2, while the weights themselves assemble into a lower triangular matrix whose i-th diagonal entry is i + 1. Comparing the two triangular determinants across that product gives n ! * det = (n + 1)!, and n ! cancels.

The same weights triangularize CartanMatrix.B n, which differs from CartanMatrix.A n in the single entry carrying the double bond at the end of the diagram. That entry contributes only to the last column, where it cuts the final diagonal entry n + 1 down to 2, so the weighted determinant is 2 * n ! instead of (n + 1)!. Type C is the transpose of type B.

Main declarations #

References #

Weighted row combinations #

Type A #

source
@[simp]
theorem CartanMatrix.A_det (n : ℕ) :
(A n).det = ↑n + 1

The determinant of the type A Cartan matrix of rank n is n + 1.

Types B and C #

source
theorem CartanMatrix.B_det {n : ℕ} (hn : 0 < n) :
(B n).det = 2

The determinant of the type B Cartan matrix of rank n is 2. The double bond at the end of the diagram cuts the last weighted diagonal entry down from n + 1 to 2.

source
theorem CartanMatrix.C_det {n : ℕ} (hn : 0 < n) :
(C n).det = 2

The determinant of the type C Cartan matrix of rank n is 2. It is the transpose of the type B Cartan matrix of the same rank.