Documentation

Mathlib.GroupTheory.Coxeter.Matrix

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 Mi,i of a Coxeter matrix can be either a positive integer or . In our treatment of Coxeter matrices, we use the value 0 instead of . 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 #

References #

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
Instances For
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

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) :

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

Equations
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')

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 := }

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.

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.

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 := }

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.

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.

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.

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.

The Coxeter matrix of type G₂.

The corresponding Coxeter-Dynkin diagram is:

       6
    o --- o
Equations

The Coxeter matrix of type H₃.

The corresponding Coxeter-Dynkin diagram is:

       5
    o --- o --- o
Equations

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.