Documentation

Mathlib.GroupTheory.Coxeter.Basic

Coxeter groups and Coxeter systems #

This file defines Coxeter groups and Coxeter systems.

Let B be a (possibly infinite) type, and let $M = (M_{i,i'})_{i, i' \in B}$ be a matrix of natural numbers. Further assume that $M$ is a Coxeter matrix (CoxeterMatrix); that is, $M$ is symmetric and $M_{i,i'} = 1$ if and only if $i = i'$. The Coxeter group associated to $M$ (CoxeterMatrix.group) has the presentation $$\langle \{s_i\}_{i \in B} \vert \{(s_i s_{i'})^{M_{i, i'}}\}_{i, i' \in B} \rangle.$$ The elements $s_i$ are called the simple reflections (CoxeterMatrix.simple) of the Coxeter group. Note that every simple reflection is an involution.

A Coxeter system (CoxeterSystem) is a group $W$, together with an isomorphism between $W$ and the Coxeter group associated to some Coxeter matrix $M$. By abuse of language, we also say that $W$ is a Coxeter group (IsCoxeterGroup), and we may speak of the simple reflections $s_i \in W$ (CoxeterSystem.simple). We state all of our results about Coxeter groups in terms of Coxeter systems where possible.

Let $W$ be a group equipped with a Coxeter system. For all monoids $G$ and all functions $f \colon B \to G$ whose values satisfy the Coxeter relations, we may lift $f$ to a multiplicative homomorphism $W \to G$ (CoxeterSystem.lift) in a unique way.

A word is a sequence of elements of $B$. The word $(i_1, \ldots, i_\ell)$ has a corresponding product $s_{i_1} \cdots s_{i_\ell} \in W$ (CoxeterSystem.wordProd). Every element of $W$ is the product of some word (CoxeterSystem.wordProd_surjective). The words that alternate between two elements of $B$ (CoxeterSystem.alternatingWord) are particularly important.

Implementation details #

Much of the literature on Coxeter groups conflates the set $S = \{s_i : i \in B\} \subseteq W$ of simple reflections with the set $B$ that indexes the simple reflections. This is usually permissible because the simple reflections $s_i$ of any Coxeter group are all distinct (a nontrivial fact that we do not prove in this file). In contrast, we try not to refer to the set $S$ of simple reflections unless necessary; instead, we state our results in terms of $B$ wherever possible.

Main definitions #

References #

TODO #

Tags #

coxeter system, coxeter group

Coxeter groups #

def CoxeterMatrix.relation {B : Type u_1} (M : CoxeterMatrix B) (i : B) (i' : B) :

The Coxeter relation associated to a Coxeter matrix $M$ and two indices $i, i' \in B$. That is, the relation $(s_i s_{i'})^{M_{i, i'}}$, considered as an element of the free group on $\{s_i\}_{i \in B}$. If $M_{i, i'} = 0$, then this is the identity, indicating that there is no relation between $s_i$ and $s_{i'}$.

Equations
Instances For

    The set of all Coxeter relations associated to the Coxeter matrix $M$.

    Equations
    Instances For
      def CoxeterMatrix.Group {B : Type u_1} (M : CoxeterMatrix B) :
      Type u_1

      The Coxeter group associated to a Coxeter matrix $M$; that is, the group $$\langle \{s_i\}_{i \in B} \vert \{(s_i s_{i'})^{M_{i, i'}}\}_{i, i' \in B} \rangle.$$

      Equations
      Instances For
        instance CoxeterMatrix.instGroupGroup {B : Type u_1} (M : CoxeterMatrix B) :
        Group M.Group
        Equations
        def CoxeterMatrix.simple {B : Type u_1} (M : CoxeterMatrix B) (i : B) :
        M.Group

        The simple reflection of the Coxeter group M.group at the index i.

        Equations
        Instances For
          theorem CoxeterMatrix.reindex_relationsSet {B : Type u_1} {B' : Type u_2} (M : CoxeterMatrix B) (e : B B') :
          (CoxeterMatrix.reindex e M).relationsSet = (FreeGroup.freeGroupCongr e) '' M.relationsSet
          def CoxeterMatrix.reindexGroupEquiv {B : Type u_1} {B' : Type u_2} (M : CoxeterMatrix B) (e : B B') :
          (CoxeterMatrix.reindex e M).Group ≃* M.Group

          The isomorphism between the Coxeter group associated to the reindexed matrix M.reindex e and the Coxeter group associated to M.

          Equations
          Instances For
            theorem CoxeterMatrix.reindexGroupEquiv_apply_simple {B : Type u_1} {B' : Type u_2} (M : CoxeterMatrix B) (e : B B') (i : B') :
            (M.reindexGroupEquiv e) ((CoxeterMatrix.reindex e M).simple i) = M.simple (e.symm i)
            theorem CoxeterMatrix.reindexGroupEquiv_symm_apply_simple {B : Type u_1} {B' : Type u_2} (M : CoxeterMatrix B) (e : B B') (i : B) :
            (M.reindexGroupEquiv e).symm (M.simple i) = (CoxeterMatrix.reindex e M).simple (e i)

            Coxeter systems #

            theorem CoxeterSystem.ext_iff {B : Type u_1} {M : CoxeterMatrix B} {W : Type u_2} :
            ∀ {inst : Group W} (x y : CoxeterSystem M W), x = y x.mulEquiv = y.mulEquiv
            theorem CoxeterSystem.ext {B : Type u_1} {M : CoxeterMatrix B} {W : Type u_2} :
            ∀ {inst : Group W} (x y : CoxeterSystem M W), x.mulEquiv = y.mulEquivx = y
            structure CoxeterSystem {B : Type u_1} (M : CoxeterMatrix B) (W : Type u_2) [Group W] :
            Type (max u_1 u_2)

            A Coxeter system CoxeterSystem M W is a structure recording the isomorphism between a group W and the Coxeter group associated to a Coxeter matrix M.

            • mulEquiv : W ≃* M.Group

              The isomorphism between W and the Coxeter group associated to M.

            Instances For
              class IsCoxeterGroup (W : Type u) [Group W] :

              A group is a Coxeter group if it admits a Coxeter system for some Coxeter matrix M.

              Instances
                theorem IsCoxeterGroup.nonempty_system {W : Type u} [Group W] [self : IsCoxeterGroup W] :
                ∃ (B : Type u) (M : CoxeterMatrix B), Nonempty (CoxeterSystem M W)

                The canonical Coxeter system on the Coxeter group associated to M.

                Equations
                Instances For
                  @[simp]
                  theorem CoxeterSystem.reindex_mulEquiv {B : Type u_1} {B' : Type u_2} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (e : B B') :
                  (cs.reindex e).mulEquiv = cs.mulEquiv.trans (M.reindexGroupEquiv e).symm
                  def CoxeterSystem.reindex {B : Type u_1} {B' : Type u_2} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (e : B B') :

                  Reindex a Coxeter system through a bijection of the indexing sets.

                  Equations
                  • cs.reindex e = { mulEquiv := cs.mulEquiv.trans (M.reindexGroupEquiv e).symm }
                  Instances For
                    @[simp]
                    theorem CoxeterSystem.map_mulEquiv {B : Type u_1} {W : Type u_3} {H : Type u_4} [Group W] [Group H] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (e : W ≃* H) :
                    (cs.map e).mulEquiv = e.symm.trans cs.mulEquiv
                    def CoxeterSystem.map {B : Type u_1} {W : Type u_3} {H : Type u_4} [Group W] [Group H] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (e : W ≃* H) :

                    Push a Coxeter system through a group isomorphism.

                    Equations
                    • cs.map e = { mulEquiv := e.symm.trans cs.mulEquiv }
                    Instances For

                      Simple reflections #

                      def CoxeterSystem.simple {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) :
                      W

                      The simple reflection of W at the index i.

                      Equations
                      Instances For
                        @[simp]
                        theorem CoxeterMatrix.toCoxeterSystem_simple {B : Type u_1} (M : CoxeterMatrix B) :
                        M.toCoxeterSystem.simple = M.simple
                        @[simp]
                        theorem CoxeterSystem.reindex_simple {B : Type u_1} {B' : Type u_2} (e : B B') {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i' : B') :
                        (cs.reindex e).simple i' = cs.simple (e.symm i')
                        @[simp]
                        theorem CoxeterSystem.map_simple {B : Type u_1} {W : Type u_3} {H : Type u_4} [Group W] [Group H] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (e : W ≃* H) (i : B) :
                        (cs.map e).simple i = e (cs.simple i)
                        @[simp]
                        theorem CoxeterSystem.simple_mul_simple_self {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) :
                        cs.simple i * cs.simple i = 1
                        @[simp]
                        theorem CoxeterSystem.simple_mul_simple_cancel_right {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} (i : B) :
                        w * cs.simple i * cs.simple i = w
                        @[simp]
                        theorem CoxeterSystem.simple_mul_simple_cancel_left {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} (i : B) :
                        cs.simple i * (cs.simple i * w) = w
                        @[simp]
                        theorem CoxeterSystem.simple_sq {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) :
                        cs.simple i ^ 2 = 1
                        @[simp]
                        theorem CoxeterSystem.inv_simple {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) :
                        (cs.simple i)⁻¹ = cs.simple i
                        @[simp]
                        theorem CoxeterSystem.simple_mul_simple_pow {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (i' : B) :
                        (cs.simple i * cs.simple i') ^ M.M i i' = 1
                        @[simp]
                        theorem CoxeterSystem.simple_mul_simple_pow' {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (i' : B) :
                        (cs.simple i' * cs.simple i) ^ M.M i i' = 1

                        The simple reflections of W generate W as a group.

                        The simple reflections of W generate W as a monoid.

                        Induction principles for Coxeter systems #

                        theorem CoxeterSystem.simple_induction {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {p : WProp} (w : W) (simple : ∀ (i : B), p (cs.simple i)) (one : p 1) (mul : ∀ (w w' : W), p wp w'p (w * w')) :
                        p w

                        If p : W → Prop holds for all simple reflections, it holds for the identity, and it is preserved under multiplication, then it holds for all elements of W.

                        theorem CoxeterSystem.simple_induction_left {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {p : WProp} (w : W) (one : p 1) (mul_simple_left : ∀ (w : W) (i : B), p wp (cs.simple i * w)) :
                        p w

                        If p : W → Prop holds for the identity and it is preserved under multiplying on the left by a simple reflection, then it holds for all elements of W.

                        theorem CoxeterSystem.simple_induction_right {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {p : WProp} (w : W) (one : p 1) (mul_simple_right : ∀ (w : W) (i : B), p wp (w * cs.simple i)) :
                        p w

                        If p : W → Prop holds for the identity and it is preserved under multiplying on the right by a simple reflection, then it holds for all elements of W.

                        Homomorphisms from a Coxeter group #

                        theorem CoxeterSystem.ext_simple {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {G : Type u_5} [Monoid G] {φ₁ : W →* G} {φ₂ : W →* G} (h : ∀ (i : B), φ₁ (cs.simple i) = φ₂ (cs.simple i)) :
                        φ₁ = φ₂

                        If two homomorphisms with domain W agree on all simple reflections, then they are equal.

                        def CoxeterMatrix.IsLiftable {B : Type u_1} {G : Type u_5} [Monoid G] (M : CoxeterMatrix B) (f : BG) :

                        The proposition that the values of the function f : B → G satisfy the Coxeter relations corresponding to the matrix M.

                        Equations
                        • M.IsLiftable f = ∀ (i i' : B), (f i * f i') ^ M.M i i' = 1
                        Instances For
                          def CoxeterSystem.lift {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {G : Type u_5} [Monoid G] :
                          { f : BG // M.IsLiftable f } (W →* G)

                          The universal mapping property of Coxeter systems. For any monoid G, functions f : B → G whose values satisfy the Coxeter relations are equivalent to monoid homomorphisms f' : W → G.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem CoxeterSystem.lift_apply_simple {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {G : Type u_5} [Monoid G] {f : BG} (hf : M.IsLiftable f) (i : B) :
                            (cs.lift f, hf) (cs.simple i) = f i
                            theorem CoxeterSystem.simple_determines_coxeterSystem {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} :
                            Function.Injective CoxeterSystem.simple

                            If two Coxeter systems on the same group W have the same Coxeter matrix M : Matrix B B ℕ and the same simple reflection map B → W, then they are identical.

                            Words #

                            def CoxeterSystem.wordProd {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) :
                            W

                            The product of the simple reflections of W corresponding to the indices in ω.

                            Equations
                            • cs.wordProd ω = (List.map cs.simple ω).prod
                            Instances For
                              @[simp]
                              theorem CoxeterSystem.wordProd_nil {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) :
                              cs.wordProd [] = 1
                              theorem CoxeterSystem.wordProd_cons {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (ω : List B) :
                              cs.wordProd (i :: ω) = cs.simple i * cs.wordProd ω
                              @[simp]
                              theorem CoxeterSystem.wordProd_singleton {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) :
                              cs.wordProd [i] = cs.simple i
                              theorem CoxeterSystem.wordProd_concat {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (ω : List B) :
                              cs.wordProd (ω.concat i) = cs.wordProd ω * cs.simple i
                              theorem CoxeterSystem.wordProd_append {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (ω' : List B) :
                              cs.wordProd (ω ++ ω') = cs.wordProd ω * cs.wordProd ω'
                              @[simp]
                              theorem CoxeterSystem.wordProd_reverse {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) :
                              cs.wordProd ω.reverse = (cs.wordProd ω)⁻¹
                              theorem CoxeterSystem.wordProd_surjective {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) :
                              def CoxeterSystem.alternatingWord {B : Type u_1} (i : B) (i' : B) (m : ) :

                              The word of length m that alternates between i and i', ending with i'.

                              Equations
                              Instances For
                                @[reducible, inline]
                                abbrev CoxeterSystem.braidWord {B : Type u_1} (M : CoxeterMatrix B) (i : B) (i' : B) :

                                The word of length M i i' that alternates between i and i', ending with i'.

                                Equations
                                Instances For
                                  theorem CoxeterSystem.alternatingWord_succ {B : Type u_1} (i : B) (i' : B) (m : ) :
                                  theorem CoxeterSystem.alternatingWord_succ' {B : Type u_1} (i : B) (i' : B) (m : ) :
                                  CoxeterSystem.alternatingWord i i' (m + 1) = (if Even m then i' else i) :: CoxeterSystem.alternatingWord i i' m
                                  @[simp]
                                  theorem CoxeterSystem.length_alternatingWord {B : Type u_1} (i : B) (i' : B) (m : ) :
                                  theorem CoxeterSystem.prod_alternatingWord_eq_mul_pow {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (i' : B) (m : ) :
                                  cs.wordProd (CoxeterSystem.alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
                                  theorem CoxeterSystem.prod_alternatingWord_eq_prod_alternatingWord_sub {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (i' : B) (m : ) (hm : m M.M i i' * 2) :
                                  cs.wordProd (CoxeterSystem.alternatingWord i i' m) = cs.wordProd (CoxeterSystem.alternatingWord i' i (M.M i i' * 2 - m))
                                  theorem CoxeterSystem.wordProd_braidWord_eq {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (i' : B) :
                                  cs.wordProd (CoxeterSystem.braidWord M i i') = cs.wordProd (CoxeterSystem.braidWord M i' i)

                                  The two words of length M i i' that alternate between i and i' have the same product. This is known as the "braid relation" or "Artin-Tits relation".