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

• CoxeterMatrix.Group
• CoxeterSystem
• IsCoxeterGroup
• CoxeterSystem.simple : If cs is a Coxeter system on the group W, then cs.simple i is the simple reflection of W at the index i.
• CoxeterSystem.lift : Extend a function f : B → G to a monoid homomorphism f' : W → G satisfying f' (cs.simple i) = f i for all i.
• CoxeterSystem.wordProd
• CoxeterSystem.alternatingWord

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6 chapter IV pages 4--5, 13--15

• J. Baez, Coxeter and Dynkin Diagrams

TODO

• The simple reflections of a Coxeter system are distinct.
• Introduce some ways to actually construct some Coxeter groups. For example, given a Coxeter matrix $M : B \times B \to \mathbb{N}$, a real vector space $V$, a basis $\{\alpha_i : i \in B\}$ and a bilinear form $\langle \cdot, \cdot \rangle \colon V \times V \to \mathbb{R}$ satisfying $$\langle \alpha_i, \alpha_{i'}\rangle = - \cos(\pi / M_{i,i'}),$$ one can form the subgroup of $GL(V)$ generated by the reflections in the $\alpha_i$, and it is a Coxeter group. We can use this to combinatorially describe the Coxeter groups of type $A$, $B$, $D$, and $I$.
• State and prove Matsumoto's theorem.
• Classify the finite Coxeter groups.

Tags

coxeter system, coxeter group

Coxeter groups

def CoxeterMatrix.relation {B : Type u_1} (M : CoxeterMatrix B) (i i' : B) : FreeGroup 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

• M.relation i i' = (FreeGroup.of i * FreeGroup.of i') ^ M.M i i'

def CoxeterMatrix.relationsSet {B : Type u_1} (M : CoxeterMatrix B) : Set (FreeGroup B)

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

Equations

• M.relationsSet = Set.range (Function.uncurry M.relation)

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

• M.Group = PresentedGroup M.relationsSet

instance CoxeterMatrix.instGroupGroup {B : Type u_1} (M : CoxeterMatrix B) : Group M.Group

Equations

• M.instGroupGroup = QuotientGroup.Quotient.group (Subgroup.normalClosure M.relationsSet)

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

• M.simple i = PresentedGroup.of i

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

• M.reindexGroupEquiv e = (QuotientGroup.congr (Subgroup.normalClosure M.relationsSet) (Subgroup.normalClosure (CoxeterMatrix.reindex e M).relationsSet) (FreeGroup.freeGroupCongr e) ⋯).symm

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

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.

theorem CoxeterSystem.ext {B : Type u_1} {M : CoxeterMatrix B} {W : Type u_2} {inst✝ : Group W} {x y : CoxeterSystem M W} (mulEquiv : x.mulEquiv = y.mulEquiv) : x = y

class IsCoxeterGroup (W : Type u) [Group W] : Prop

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

• nonempty_system : ∃ (B : Type u) (M : CoxeterMatrix B), Nonempty (CoxeterSystem M W)

def CoxeterMatrix.toCoxeterSystem {B : Type u_1} (M : CoxeterMatrix B) : CoxeterSystem M M.Group

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

Equations

• M.toCoxeterSystem = { mulEquiv := MulEquiv.refl M.Group }

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') : CoxeterSystem (CoxeterMatrix.reindex e M) W

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

Equations

• cs.reindex e = { mulEquiv := cs.mulEquiv.trans (M.reindexGroupEquiv e).symm }

@[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.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) : CoxeterSystem M H

Push a Coxeter system through a group isomorphism.

Equations

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

@[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

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

• cs.simple i = cs.mulEquiv.symm (PresentedGroup.of i)

@[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 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 i' : B) : (cs.simple i' * cs.simple i) ^ M.M i i' = 1

theorem CoxeterSystem.subgroup_closure_range_simple {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Subgroup.closure (Set.range cs.simple) = ⊤

The simple reflections of W generate W as a group.

theorem CoxeterSystem.submonoid_closure_range_simple {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Submonoid.closure (Set.range cs.simple) = ⊤

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 : W → Prop} (w : W) (simple : ∀ (i : B), p (cs.simple i)) (one : p 1) (mul : ∀ (w w' : W), p w → p 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 : W → Prop} (w : W) (one : p 1) (mul_simple_left : ∀ (w : W) (i : B), p w → p (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 : W → Prop} (w : W) (one : p 1) (mul_simple_right : ∀ (w : W) (i : B), p w → p (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} (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 : B → G) : Prop

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

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 : B → G // 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.

@[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 : B → G} (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

@[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) : 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) : Function.Surjective cs.wordProd

def CoxeterSystem.alternatingWord {B : Type u_1} (i i' : B) (m : ℕ) : List B

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

Equations

• CoxeterSystem.alternatingWord i i' 0 = []
• CoxeterSystem.alternatingWord i i' m_2.succ = (CoxeterSystem.alternatingWord i' i m_2).concat i'

@[reducible, inline]

abbrev CoxeterSystem.braidWord {B : Type u_1} (M : CoxeterMatrix B) (i i' : B) : List B

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

Equations

• CoxeterSystem.braidWord M i i' = CoxeterSystem.alternatingWord i i' (M.M i i')

theorem CoxeterSystem.alternatingWord_succ {B : Type u_1} (i i' : B) (m : ℕ) : CoxeterSystem.alternatingWord i i' (m + 1) = (CoxeterSystem.alternatingWord i' i m).concat i'

theorem CoxeterSystem.alternatingWord_succ' {B : Type u_1} (i 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 i' : B) (m : ℕ) : (CoxeterSystem.alternatingWord i i' m).length = m

theorem CoxeterSystem.getElem_alternatingWord {B : Type u_1} (i j : B) (p k : ℕ) (hk : k < p) : (CoxeterSystem.alternatingWord i j p)[k] = if Even (p + k) then i else j

theorem CoxeterSystem.getElem_alternatingWord_swapIndices {B : Type u_1} (i j : B) (p k : ℕ) (h : k + 1 < p) : (CoxeterSystem.alternatingWord i j p)[k + 1] = (CoxeterSystem.alternatingWord j i p)[k]

theorem CoxeterSystem.listTake_alternatingWord {B : Type u_1} (i j : B) (p k : ℕ) (h : k < 2 * p) : List.take k (CoxeterSystem.alternatingWord i j (2 * p)) = if Even k then CoxeterSystem.alternatingWord i j k else CoxeterSystem.alternatingWord j i k

theorem CoxeterSystem.listTake_succ_alternatingWord {B : Type u_1} (i j : B) (p k : ℕ) (h : k + 1 < 2 * p) : List.take (k + 1) (CoxeterSystem.alternatingWord i j (2 * p)) = i :: List.take k (CoxeterSystem.alternatingWord j i (2 * p))

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