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 $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

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

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

Instances For

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

Instances For

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.

Instances For

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.

Instances For

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

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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 := Matrix.of ![![1, 6], ![6, 1]], isSymm := CoxeterMatrix.G₂.proof_1, diagonal := CoxeterMatrix.G₂.proof_2, off_diagonal := CoxeterMatrix.G₂.proof_3 }

Instances For

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 := Matrix.of ![![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 }

Instances For

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.

Instances For