Coexeter matrices

This file defines some standard Coxeter matrices.

Main definitions

• 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.

@[inline, reducible]

abbrev CoxeterMatrix.Aₙ (n : ℕ) : Matrix (Fin n) (Fin n) ℕ

The Coxeter matrix of family A(n).

The corresponding Coxeter-Dynkin diagram is:

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

Equations

• CoxeterMatrix.Aₙ n = Matrix.of fun (i j : Fin n) => if i = j then 1 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2

theorem CoxeterMatrix.AₙIsCoxeter (n : ℕ) : Matrix.IsCoxeter (CoxeterMatrix.Aₙ n)

@[inline, reducible]

abbrev CoxeterMatrix.Bₙ (n : ℕ) : Matrix (Fin n) (Fin n) ℕ

The Coxeter matrix of family Bₙ.

The corresponding Coxeter-Dynkin diagram is:

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

Equations

• CoxeterMatrix.Bₙ n = Matrix.of fun (i j : Fin n) => if i = j then 1 else if ↑i = n - 1 ∧ ↑j = n - 2 ∨ ↑j = n - 1 ∧ ↑i = n - 2 then 4 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2

theorem CoxeterMatrix.BₙIsCoxeter (n : ℕ) : Matrix.IsCoxeter (CoxeterMatrix.Bₙ n)

@[inline, reducible]

abbrev CoxeterMatrix.Dₙ (n : ℕ) : Matrix (Fin n) (Fin n) ℕ

The Coxeter matrix of family Dₙ.

The corresponding Coxeter-Dynkin diagram is:

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

Equations

• CoxeterMatrix.Dₙ n = Matrix.of fun (i j : Fin n) => if i = j then 1 else if ↑i = n - 1 ∧ ↑j = n - 3 ∨ ↑j = n - 1 ∧ ↑i = n - 3 then 3 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2

theorem CoxeterMatrix.DₙIsCoxeter (n : ℕ) : Matrix.IsCoxeter (CoxeterMatrix.Dₙ n)

@[inline, reducible]

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

The Coxeter matrix of m-indexed family I₂(m).

The corresponding Coxeter-Dynkin diagram is:

     m + 2
    o --- o

Equations

• CoxeterMatrix.I₂ₘ m = Matrix.of fun (i j : Fin 2) => if i = j then 1 else m + 2

theorem CoxeterMatrix.I₂ₘIsCoxeter (m : ℕ) : Matrix.IsCoxeter (CoxeterMatrix.I₂ₘ m)

def CoxeterMatrix.E₆ : Matrix (Fin 6) (Fin 6) ℕ

The Coxeter matrix of system E₆.

The corresponding Coxeter-Dynkin diagram is:

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

Equations

• CoxeterMatrix.E₆ = Matrix.of ![![1, 2, 3, 2, 2, 2], ![2, 1, 2, 3, 2, 2], ![3, 2, 1, 3, 2, 2], ![2, 3, 3, 1, 3, 2], ![2, 2, 2, 3, 1, 3], ![2, 2, 2, 2, 3, 1]]

theorem CoxeterMatrix.E₆IsCoxeter : Matrix.IsCoxeter CoxeterMatrix.E₆

def CoxeterMatrix.E₇ : Matrix (Fin 7) (Fin 7) ℕ

The Coxeter matrix of system 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.

theorem CoxeterMatrix.E₇IsCoxeter : Matrix.IsCoxeter CoxeterMatrix.E₇

def CoxeterMatrix.E₈ : Matrix (Fin 8) (Fin 8) ℕ

The Coxeter matrix of system 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.

theorem CoxeterMatrix.E₈IsCoxeter : Matrix.IsCoxeter CoxeterMatrix.E₈

def CoxeterMatrix.F₄ : Matrix (Fin 4) (Fin 4) ℕ

The Coxeter matrix of system F₄.

The corresponding Coxeter-Dynkin diagram is:

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

Equations

• CoxeterMatrix.F₄ = Matrix.of ![![1, 3, 2, 2], ![3, 1, 4, 2], ![2, 4, 1, 3], ![2, 2, 3, 1]]

theorem CoxeterMatrix.F₄IsCoxeter : Matrix.IsCoxeter CoxeterMatrix.F₄

def CoxeterMatrix.G₂ : Matrix (Fin 2) (Fin 2) ℕ

The Coxeter matrix of system G₂.

The corresponding Coxeter-Dynkin diagram is:

       6
    o --- o

Equations

• CoxeterMatrix.G₂ = Matrix.of ![![1, 6], ![6, 1]]

theorem CoxeterMatrix.G₂IsCoxeter : Matrix.IsCoxeter CoxeterMatrix.G₂

def CoxeterMatrix.H₃ : Matrix (Fin 3) (Fin 3) ℕ

The Coxeter matrix of system H₃.

The corresponding Coxeter-Dynkin diagram is:

       5
    o --- o --- o

Equations

• CoxeterMatrix.H₃ = Matrix.of ![![1, 3, 2], ![3, 1, 5], ![2, 5, 1]]

theorem CoxeterMatrix.H₃IsCoxeter : Matrix.IsCoxeter CoxeterMatrix.H₃

def CoxeterMatrix.H₄ : Matrix (Fin 4) (Fin 4) ℕ

The Coxeter matrix of system H₄.

The corresponding Coxeter-Dynkin diagram is:

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

Equations

• CoxeterMatrix.H₄ = Matrix.of ![![1, 3, 2, 2], ![3, 1, 3, 2], ![2, 3, 1, 5], ![2, 2, 5, 1]]

theorem CoxeterMatrix.H₄IsCoxeter : Matrix.IsCoxeter CoxeterMatrix.H₄