Coxeter Systems

This file defines Coxeter systems and Coxeter groups.

A Coxeter system is a pair (W, S) where W is a group generated by a set of reflections (involutions) S = {s₁,s₂,...,sₙ}, subject to relations determined by a Coxeter matrix M = (mᵢⱼ). The Coxeter matrix is a symmetric matrix with entries mᵢⱼ representing the order of the product sᵢsⱼ for i ≠ j and mᵢᵢ = 1.

When (W, S) is a Coxeter system, one also says, by abuse of language, that W is a Coxeter group. A Coxeter group W is determined by the presentation W = ⟨s₁,s₂,...,sₙ | ∀ i j, (sᵢsⱼ)^mᵢⱼ = 1⟩, where 1 is the identity element of W.

The finite Coxeter groups are classified (TODO) as the four infinite families:

• Aₙ, Bₙ, Dₙ, I₂ₘ

And the exceptional systems:

• E₆, E₇, E₈, F₄, G₂, H₃, H₄

Implementation details

In this file a Coxeter system, designated as CoxeterSystem M W, is implemented as a structure which effectively records the isomorphism between a group W and the corresponding group presentation derived from a Coxeter matrix M. From another perspective, it serves as a set of generators for W, tailored to the underlying type of M, while ensuring compliance with the relations specified by the Coxeter matrix M.

A type class IsCoxeterGroup is introduced, for groups that are isomorphic to a group presentation corresponding to a Coxeter matrix which is registered in a Coxeter system.

Main definitions

• Matrix.IsCoxeter : A matrix IsCoxeter if it is a symmetric matrix with diagonal entries equal to one and off-diagonal entries distinct from one.
• Matrix.CoxeterGroup : The group presentation corresponding to a Coxeter matrix.
• CoxeterSystem : A structure recording the isomorphism between a group W and the group presentation corresponding to a Coxeter matrix, i.e. Matrix.CoxeterGroup M.
• equivCoxeterGroup : Coxeter groups of isomorphic types are isomorphic.
• IsCoxeterGroup : A group is a Coxeter group if it is registered in a Coxeter system.
• 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

TODO

• The canonical map from the type to the Coxeter group W is an injection.
• A group W registered in a Coxeter system is a Coxeter group.
• A Coxeter group is an instance of IsCoxeterGroup.

Tags

coxeter system, coxeter group

structure Matrix.IsCoxeter {B : Type u_1} (M : Matrix B B ℕ) : Prop

A matrix IsCoxeter if it is a symmetric matrix with diagonal entries equal to one and off-diagonal entries distinct from one.

• symmetric : Matrix.IsSymm M
• diagonal : ∀ (b : B), M b b = 1
• off_diagonal : ∀ (b₁ b₂ : B), b₁ ≠ b₂ → M b₁ b₂ ≠ 1

def CoxeterGroup.Relations.ofMatrix {B : Type u_1} (M : Matrix B B ℕ) : B × B → FreeGroup B

The relations corresponding to a Coxeter matrix.

Equations

• CoxeterGroup.Relations.ofMatrix M = Function.uncurry fun (b₁ b₂ : B) => (FreeGroup.of b₁ * FreeGroup.of b₂) ^ M b₁ b₂

def CoxeterGroup.Relations.toSet {B : Type u_1} (M : Matrix B B ℕ) : Set (FreeGroup B)

The set of relations corresponding to a Coxeter matrix.

Equations

• CoxeterGroup.Relations.toSet M = Set.range (CoxeterGroup.Relations.ofMatrix M)

def Matrix.CoxeterGroup {B : Type u_1} (M : Matrix B B ℕ) : Type u_1

The group presentation corresponding to a Coxeter matrix.

Equations

• Matrix.CoxeterGroup M = PresentedGroup (CoxeterGroup.Relations.toSet M)

instance instGroupCoxeterGroup {B : Type u_1} (M : Matrix B B ℕ) : Group (Matrix.CoxeterGroup M)

Equations

• instGroupCoxeterGroup M = QuotientGroup.Quotient.group (Subgroup.normalClosure (CoxeterGroup.Relations.toSet M))

def CoxeterGroup.of {B : Type u_1} (M : Matrix B B ℕ) (b : B) : Matrix.CoxeterGroup M

The canonical map from B to the Coxeter group with generators b : B. The term b is mapped to the equivalence class of the image of b in CoxeterGroup M.

Equations

• CoxeterGroup.of M b = PresentedGroup.of b

@[simp]

theorem CoxeterGroup.of_apply {B : Type u_1} (M : Matrix B B ℕ) (b : B) : CoxeterGroup.of M b = PresentedGroup.of b

structure CoxeterSystem {B : Type u_1} (M : Matrix B B ℕ) (W : Type u_2) [Group W] : Type (max u_1 u_2)

A Coxeter system CoxeterSystem W is a structure recording the isomorphism between a group W and the group presentation corresponding to a Coxeter matrix. Equivalently, this can be seen as a list of generators of W parameterized by the underlying type of M, which satisfy the relations of the Coxeter matrix M.

• ofMulEquiv :: (
• mulEquiv : W ≃* Matrix.CoxeterGroup M

  mulEquiv is the isomorphism between the group W and the group presentation corresponding to a Coxeter matrix M.

• )

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 : Matrix B B ℕ), Matrix.IsCoxeter M ∧ Nonempty (CoxeterSystem M W)

instance CoxeterSystem.funLike {B : Type u_2} {W : Type u_4} [Group W] {M : Matrix B B ℕ} : FunLike (CoxeterSystem M W) B W

A Coxeter system for W with Coxeter matrix M indexed by B, is associated to a map B → W recording the images of the indices.

Equations

• CoxeterSystem.funLike = { coe := fun (cs : CoxeterSystem M W) (b : B) => (MulEquiv.symm cs.mulEquiv) (PresentedGroup.of b), coe_injective' := ⋯ }

@[simp]

theorem CoxeterSystem.mulEquiv_apply_coe {B : Type u_2} {W : Type u_4} [Group W] {M : Matrix B B ℕ} (cs : CoxeterSystem M W) (b : B) : cs.mulEquiv (cs b) = PresentedGroup.of b

theorem CoxeterSystem.ext' {B : Type u_2} {W : Type u_4} [Group W] {M : Matrix B B ℕ} {cs₁ : CoxeterSystem M W} {cs₂ : CoxeterSystem M W} (H : ⇑cs₁ = ⇑cs₂) : cs₁ = cs₂

The map sending a Coxeter system to its associated map B → W is injective.

theorem CoxeterSystem.ext {B : Type u_2} {W : Type u_4} [Group W] {M : Matrix B B ℕ} {cs₁ : CoxeterSystem M W} {cs₂ : CoxeterSystem M W} (H : ∀ (b : B), cs₁ b = cs₂ b) : cs₁ = cs₂

Extensionality rule for Coxeter systems.

def CoxeterSystem.ofCoxeterGroup (X : Type u_6) (D : Matrix X X ℕ) : CoxeterSystem D (Matrix.CoxeterGroup D)

The canonical Coxeter system of the Coxeter group over X.

Equations

• CoxeterSystem.ofCoxeterGroup X D = { mulEquiv := MulEquiv.refl (Matrix.CoxeterGroup D) }

@[simp]

theorem CoxeterSystem.ofCoxeterGroup_apply {X : Type u_6} (D : Matrix X X ℕ) (x : X) : (CoxeterSystem.ofCoxeterGroup X D) x = CoxeterGroup.of D x

theorem CoxeterSystem.map_relations_eq_reindex_relations {B : Type u_2} {B' : Type u_3} {M : Matrix B B ℕ} (e : B ≃ B') : ⇑(MulEquiv.toMonoidHom (FreeGroup.freeGroupCongr e)) '' CoxeterGroup.Relations.toSet M = CoxeterGroup.Relations.toSet ((Matrix.reindex e e) M)

def CoxeterSystem.equivCoxeterGroup {B : Type u_2} {B' : Type u_3} {M : Matrix B B ℕ} (e : B ≃ B') : Matrix.CoxeterGroup M ≃* Matrix.CoxeterGroup ((Matrix.reindex e e) M)

Coxeter groups of isomorphic types are isomorphic.

Equations

• One or more equations did not get rendered due to their size.

theorem CoxeterSystem.equivCoxeterGroup_apply_of {B : Type u_2} {B' : Type u_3} (b : B) (M : Matrix B B ℕ) (e : B ≃ B') : (CoxeterSystem.equivCoxeterGroup e) (CoxeterGroup.of M b) = CoxeterGroup.of ((Matrix.reindex e e) M) (e b)

theorem CoxeterSystem.equivCoxeterGroup_symm_apply_of {B : Type u_2} {B' : Type u_3} (b' : B') (M : Matrix B B ℕ) (e : B ≃ B') : (MulEquiv.symm (CoxeterSystem.equivCoxeterGroup e)) (CoxeterGroup.of ((Matrix.reindex e e) M) b') = CoxeterGroup.of M (e.symm b')

@[simp]

theorem CoxeterSystem.reindex_mulEquiv {B : Type u_2} {B' : Type u_3} {W : Type u_4} [Group W] {M : Matrix B B ℕ} (cs : CoxeterSystem M W) (e : B ≃ B') : (CoxeterSystem.reindex cs e).mulEquiv = MulEquiv.trans cs.mulEquiv (CoxeterSystem.equivCoxeterGroup e)

def CoxeterSystem.reindex {B : Type u_2} {B' : Type u_3} {W : Type u_4} [Group W] {M : Matrix B B ℕ} (cs : CoxeterSystem M W) (e : B ≃ B') : CoxeterSystem ((Matrix.reindex e e) M) W

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

Equations

• CoxeterSystem.reindex cs e = { mulEquiv := MulEquiv.trans cs.mulEquiv (CoxeterSystem.equivCoxeterGroup e) }

@[simp]

theorem CoxeterSystem.reindex_apply {B : Type u_2} {B' : Type u_3} {W : Type u_4} [Group W] {M : Matrix B B ℕ} (cs : CoxeterSystem M W) (e : B ≃ B') (b' : B') : (CoxeterSystem.reindex cs e) b' = cs (e.symm b')

@[simp]

theorem CoxeterSystem.map_mulEquiv {B : Type u_2} {W : Type u_4} {H : Type u_5} [Group W] [Group H] {M : Matrix B B ℕ} (cs : CoxeterSystem M W) (e : W ≃* H) : (CoxeterSystem.map cs e).mulEquiv = MulEquiv.trans (MulEquiv.symm e) cs.mulEquiv

def CoxeterSystem.map {B : Type u_2} {W : Type u_4} {H : Type u_5} [Group W] [Group H] {M : Matrix B B ℕ} (cs : CoxeterSystem M W) (e : W ≃* H) : CoxeterSystem M H

Pushing a Coxeter system through a group isomorphism.

Equations

• CoxeterSystem.map cs e = { mulEquiv := MulEquiv.trans (MulEquiv.symm e) cs.mulEquiv }

@[simp]

theorem CoxeterSystem.map_apply {B : Type u_2} {W : Type u_4} {H : Type u_5} [Group W] [Group H] {M : Matrix B B ℕ} (cs : CoxeterSystem M W) (e : W ≃* H) (b : B) : (CoxeterSystem.map cs e) b = e (cs b)

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