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 #

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

      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

        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

          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

            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

              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

                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

                  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

                    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

                      The Coxeter matrix of type G₂.

                      The corresponding Coxeter-Dynkin diagram is:

                             6
                          o --- o
                      
                      Equations
                      Instances For

                        The Coxeter matrix of type H₃.

                        The corresponding Coxeter-Dynkin diagram is:

                               5
                            o --- o --- o
                        
                        Equations
                        Instances For

                          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