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.

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)