Coxeter matrices

Let us say that a matrix (possibly an infinite matrix) is a Coxeter matrix (CoxeterMatrix) if its entries are natural numbers, it is symmetric, its diagonal entries are equal to 1, and its off-diagonal entries are not equal to 1. In this file, we define Coxeter matrices and provide some ways of constructing them.

We also define the Coxeter matrices CoxeterMatrix.Aₙ (n : ℕ), CoxeterMatrix.Bₙ (n : ℕ), CoxeterMatrix.Dₙ (n : ℕ), CoxeterMatrix.I₂ₘ (m : ℕ), CoxeterMatrix.E₆, CoxeterMatrix.E₇, CoxeterMatrix.E₈, CoxeterMatrix.F₄, CoxeterMatrix.G₂, CoxeterMatrix.H₃, and CoxeterMatrix.H₄. Up to reindexing, these are exactly the Coxeter matrices whose corresponding Coxeter group (CoxeterMatrix.coxeterGroup) is finite and irreducible, although we do not prove that in this file.

Implementation details

In some texts on Coxeter groups, each entry $M_{i,i'}$ of a Coxeter matrix can be either a positive integer or $\infty$. In our treatment of Coxeter matrices, we use the value $0$ instead of $\infty$. This will turn out to have some fortunate consequences when defining the Coxeter group of a Coxeter matrix and the standard geometric representation of a Coxeter group.

Main definitions

• CoxeterMatrix : The type of symmetric matrices of natural numbers, with rows and columns indexed by a type B, whose diagonal entries are equal to 1 and whose off-diagonal entries are not equal to 1.
• CoxeterMatrix.reindex : Reindexes a Coxeter matrix by a bijection on the index type.
• CoxeterMatrix.Aₙ : Coxeter matrix for the symmetry group of the regular n-simplex.
• CoxeterMatrix.Bₙ : Coxeter matrix for the symmetry group of the regular n-hypercube and its dual, the regular n-orthoplex (or n-cross-polytope).
• CoxeterMatrix.Dₙ : Coxeter matrix for the symmetry group of the n-demicube.
• CoxeterMatrix.I₂ₘ : Coxeter matrix for the symmetry group of the regular (m + 2)-gon.
• CoxeterMatrix.E₆ : Coxeter matrix for the symmetry group of the E₆ root polytope.
• CoxeterMatrix.E₇ : Coxeter matrix for the symmetry group of the E₇ root polytope.
• CoxeterMatrix.E₈ : Coxeter matrix for the symmetry group of the E₈ root polytope.
• CoxeterMatrix.F₄ : Coxeter matrix for the symmetry group of the regular 4-polytope, the 24-cell.
• CoxeterMatrix.G₂ : Coxeter matrix for the symmetry group of the regular hexagon.
• CoxeterMatrix.H₃ : Coxeter matrix for the symmetry group of the regular dodecahedron and icosahedron.
• CoxeterMatrix.H₄ : Coxeter matrix for the symmetry group of the regular 4-polytopes, the 120-cell and 600-cell.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6 chapter IV pages 4--5, 13--15

• J. Baez, Coxeter and Dynkin Diagrams

theorem CoxeterMatrix.ext {B : Type u_1} {x : CoxeterMatrix B} {y : CoxeterMatrix B} (M : x.M = y.M) : x = y

theorem CoxeterMatrix.ext_iff {B : Type u_1} {x : CoxeterMatrix B} {y : CoxeterMatrix B} : x = y ↔ x.M = y.M

structure CoxeterMatrix (B : Type u_1) : Type u_1

A Coxeter matrix is a symmetric matrix of natural numbers whose diagonal entries are equal to 1 and whose off-diagonal entries are not equal to 1.

• M : Matrix B B ℕ

  The underlying matrix of the Coxeter matrix.

• isSymm : self.M.IsSymm
• diagonal : ∀ (i : B), self.M i i = 1
• off_diagonal : ∀ (i i' : B), i ≠ i' → self.M i i' ≠ 1

theorem CoxeterMatrix.isSymm {B : Type u_1} (self : CoxeterMatrix B) : self.M.IsSymm

@[simp]

theorem CoxeterMatrix.diagonal {B : Type u_1} (self : CoxeterMatrix B) (i : B) : self.M i i = 1

theorem CoxeterMatrix.off_diagonal {B : Type u_1} (self : CoxeterMatrix B) (i : B) (i' : B) : i ≠ i' → self.M i i' ≠ 1

instance CoxeterMatrix.instCoeFunMatrixNat {B : Type u_1} : CoeFun (CoxeterMatrix B) fun (x : CoxeterMatrix B) => Matrix B B ℕ

A Coxeter matrix can be coerced to a matrix.

Equations

• CoxeterMatrix.instCoeFunMatrixNat = { coe := CoxeterMatrix.M }

theorem CoxeterMatrix.symmetric {B : Type u_1} (M : CoxeterMatrix B) (i : B) (i' : B) : M.M i i' = M.M i' i

def CoxeterMatrix.reindex {B : Type u_1} {B' : Type u_2} (e : B ≃ B') (M : CoxeterMatrix B) : CoxeterMatrix B'

The Coxeter matrix formed by reindexing via the bijection e : B ≃ B'.

Equations

• CoxeterMatrix.reindex e M = { M := (Matrix.reindex e e) M.M, isSymm := ⋯, diagonal := ⋯, off_diagonal := ⋯ }

theorem CoxeterMatrix.reindex_apply {B : Type u_1} {B' : Type u_2} (e : B ≃ B') (M : CoxeterMatrix B) (i : B') (i' : B') : (CoxeterMatrix.reindex e M).M i i' = M.M (e.symm i) (e.symm i')

def CoxeterMatrix.Aₙ (n : ℕ) : CoxeterMatrix (Fin n)

The Coxeter matrix of type Aₙ.

The corresponding Coxeter-Dynkin diagram is:

    o --- o --- o ⬝ ⬝ ⬝ ⬝ o --- o

Equations

• CoxeterMatrix.Aₙ n = { M := Matrix.of fun (i j : Fin n) => if i = j then 1 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2, isSymm := ⋯, diagonal := ⋯, off_diagonal := ⋯ }

def CoxeterMatrix.Bₙ (n : ℕ) : CoxeterMatrix (Fin n)

The Coxeter matrix of type Bₙ.

The corresponding Coxeter-Dynkin diagram is:

       4
    o --- o --- o ⬝ ⬝ ⬝ ⬝ o --- o

Equations

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

def CoxeterMatrix.Dₙ (n : ℕ) : CoxeterMatrix (Fin n)

The Coxeter matrix of type Dₙ.

The corresponding Coxeter-Dynkin diagram is:

    o
     \
      o --- o ⬝ ⬝ ⬝ ⬝ o --- o
     /
    o

Equations

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

def CoxeterMatrix.I₂ₘ (m : ℕ) : CoxeterMatrix (Fin 2)

The Coxeter matrix of type I₂(m).

The corresponding Coxeter-Dynkin diagram is:

     m + 2
    o --- o

Equations

• CoxeterMatrix.I₂ₘ m = { M := Matrix.of fun (i j : Fin 2) => if i = j then 1 else m + 2, isSymm := ⋯, diagonal := ⋯, off_diagonal := ⋯ }

def CoxeterMatrix.E₆ : CoxeterMatrix (Fin 6)

The Coxeter matrix of type E₆.

The corresponding Coxeter-Dynkin diagram is:

                o
                |
    o --- o --- o --- o --- o

Equations

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

def CoxeterMatrix.E₇ : CoxeterMatrix (Fin 7)

The Coxeter matrix of type E₇.

The corresponding Coxeter-Dynkin diagram is:

                o
                |
    o --- o --- o --- o --- o --- o

Equations

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

def CoxeterMatrix.E₈ : CoxeterMatrix (Fin 8)

The Coxeter matrix of type E₈.

The corresponding Coxeter-Dynkin diagram is:

                o
                |
    o --- o --- o --- o --- o --- o --- o

Equations

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

def CoxeterMatrix.F₄ : CoxeterMatrix (Fin 4)

The Coxeter matrix of type F₄.

The corresponding Coxeter-Dynkin diagram is:

             4
    o --- o --- o --- o

Equations

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

def CoxeterMatrix.G₂ : CoxeterMatrix (Fin 2)

The Coxeter matrix of type G₂.

The corresponding Coxeter-Dynkin diagram is:

       6
    o --- o

Equations

• CoxeterMatrix.G₂ = { M := !![1, 6; 6, 1], isSymm := CoxeterMatrix.G₂.proof_1, diagonal := CoxeterMatrix.G₂.proof_2, off_diagonal := CoxeterMatrix.G₂.proof_3 }

def CoxeterMatrix.H₃ : CoxeterMatrix (Fin 3)

The Coxeter matrix of type H₃.

The corresponding Coxeter-Dynkin diagram is:

       5
    o --- o --- o

Equations

• CoxeterMatrix.H₃ = { M := !![1, 3, 2; 3, 1, 5; 2, 5, 1], isSymm := CoxeterMatrix.H₃.proof_1, diagonal := CoxeterMatrix.H₃.proof_2, off_diagonal := CoxeterMatrix.H₃.proof_3 }

def CoxeterMatrix.H₄ : CoxeterMatrix (Fin 4)

The Coxeter matrix of type H₄.

The corresponding Coxeter-Dynkin diagram is:

       5
    o --- o --- o --- o

Equations

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