Coxeter Groups

Stream: mathlib4

[Newell Jensen]

After spending some time working on personal lean coding projects in relative obscurity, I would like to contribute to mathlib. Specifically, I'm interested in incorporating Coxeter Groups. Before diving in, I'm hoping to seek advice from the maintainers on the most efficient approach to ensure smooth integration with mathlib, given that Coxeter/Weyl/Reflection groups have many connections to various areas of mathematics. Do any maintainers have implementation suggestions for this endeavor?

For example, would classifying the finite Coxeter groups: $A_n, B_n, D_n, I_2(p), E_6, E_7, E_8, F_4, H_3$ and $H_4$ be a good starting point?

[Scott Morrison]

Even giving the definitions of some of them would be a good start!

[Newell Jensen]

Currently refreshing my memory with The Geometry and Topology of Coxeter Groups by Michael W. Davis, but that sounds like a good first PR, the definitions, and then work up from there.

[Johan Commelin]

Be sure to look at the Lie theory formalized by @Oliver Nash. In particular, mathlib already has the Cartan matrices for most of the Dynkin types that you list.

[Oliver Nash]

I have often thought that Coxeter groups would make a great project, and I'd love to see someone do this. Actually I recently decided to add a bit more Lie theory to Mathlib and if all goes well I'll probably add the definition the root systems (and data) in the next month or so (together with the proof that the collection of non-zero vectors satisfying docs#LieAlgebra.IsRoot form a root system, subject suitable hypotheses). So then we'd have Weyl groups and it would be really nice if some abstract theory of Coxeter groups was starting to take shape in parallel!

[Oliver Nash]

I should add that @Deepro Choudhury did some nice work on root systems in Lean, though it's in a private repository.

[Newell Jensen]

@Oliver Nash I have the time to put into this but some guidance might be necessary. Today I will try and wrap my head around Bourbaki/Davis and associated mathlib code that might serve as an indication of how to formulate the definition properly and will post my initial attempts here in order to get some feedback.

[Oliver Nash]

@Newell Jensen that sounds great! I'm happy to help however I can.

[Newell Jensen]

@Oliver Nash As you may already know...

I am thinking I would define CoxeterGroup abstractly via FreeGroup α similar to what you did in CartanMatrix but instead I plan usingPresentedGroup which creates the quotient group modulo the relations you pass it. On top of this I would need to define a CoxeterSystem. However, before getting into the details and specifics of that, and as a first step to acquaint myself with mathlib's group API, I have started creating the presentation for the Dihedral group using PresentedGroup. Once the PresentedGroup for a CoxeterGroup or CoxeterSystem is defined appropriately, I could then show that for $n=2$ that the Coxeter group is equivalent to the presentation of the Dihedral group.

Below is the code I have so far (I still have some proofs to finish). However, some questions/comments I have before making PR(s):

• The property that the normalClosure is equal to the kernel of the lifted homomorphism depends on textbook. Dummit and Foote (3ed, pg. 218) assumes this in the definition of a presentation group. Other textbooks do not, see example 2, pg. 448 of Gallian 8ed. My take on it is that this should be proved (rather than updating the current definition of PresentedGroup) and that is what I am currently working on. Thoughts?

• If the aforementioned is to be added to PresentedGroup.lean, then I will need to refactor what I am currently still working on to make it more abstract. Instead of using 2 * n I would need to make it so that it was some constant. Thoughts?

• The code below still needs some cleaning up with naming conventions and such but if you (or anyone else) has comments/suggestions please advise. Thanks!

import Mathlib.GroupTheory.PresentedGroup
import Mathlib.GroupTheory.SpecificGroups.Dihedral

-- The code here in the PresentedGroup namespace would got inside of PresentedGroup in a separate PR
namespace PresentedGroup

variable {α : Type*}

variable {G : Type*} [Group G] {f : α → G} {rels : Set (FreeGroup α)}

-- mathport name: exprF
local notation "F" => FreeGroup.lift f

variable (h' : ∀ r ∈ rels, FreeGroup.lift f r = 1)

theorem thirdIsoThm : (FreeGroup α ⧸ Subgroup.normalClosure rels) ⧸
    Subgroup.map (QuotientGroup.mk' (Subgroup.normalClosure rels)) (MonoidHom.ker (FreeGroup.lift f)) ≃*
    FreeGroup α ⧸ MonoidHom.ker (FreeGroup.lift f) :=
  QuotientGroup.quotientQuotientEquivQuotient (Subgroup.normalClosure rels) (MonoidHom.ker F) (closure_rels_subset_ker h')

-- This theorem is an axiom of the definitons for Presentation of a Group in Dummit and Foote (3ed, pg. 218).
-- However, it seems that we should be proving this rather than adding it to the definition axioms.
theorem closure_rels_eq_ker : Subgroup.normalClosure rels = MonoidHom.ker F := by
  sorry

/-- Noether's first isomorphism theorem states G ⧸ ker φ ≃* range φ, i.e. FreeGroup α ⧸ ker F ≃* range F -/
theorem presented_group_eq_range_lift : PresentedGroup rels ≃* (FreeGroup α ⧸ MonoidHom.ker F) := by
  refine MulEquiv.symm (QuotientGroup.quotientMulEquivOfEq ?h)
  rw [← closure_rels_eq_ker]

end PresentedGroup


open DihedralGroup

namespace DihedralPresentedGroup

inductive generator (n : ℕ)
  | a : ZMod n → generator n
  | b : ZMod n → generator n
  deriving DecidableEq

def genMap : generator n → DihedralGroup n
  | generator.a i => sr i
  | generator.b i => sr i * r i

/-- The presentation of the Dihedral group which makes it a Coxeter group is
⟨a, b | a^2 = 1, b^2 = 1, (a * b)^n = 1⟩ -/
def Rels {i : ZMod n} : Set (FreeGroup (generator n)) :=
  {FreeGroup.of (generator.a i) * FreeGroup.of (generator.a i)} ∪
  {FreeGroup.of (generator.b i) * FreeGroup.of (generator.b i)} ∪
  {(FreeGroup.of (generator.a i) * FreeGroup.of (generator.b i)) ^ n}

@[simp] abbrev DihedralPresentedGroup {i : ZMod n} := PresentedGroup <| @Rels n i
@[simp] abbrev KerQuotClosure {i : ZMod n} := Subgroup.map (QuotientGroup.mk'
  (Subgroup.normalClosure (@Rels n i))) (MonoidHom.ker (FreeGroup.lift (@genMap n)))
@[simp] abbrev FreeGroupQuotLift (n : ℕ) :=
  FreeGroup (generator n) ⧸ MonoidHom.ker (FreeGroup.lift (@genMap n))

theorem factor_group_closure_ker : @DihedralPresentedGroup n i ≃* FreeGroupQuotLift n := by
  simp only [DihedralPresentedGroup, FreeGroupQuotLift]
  exact PresentedGroup.presented_group_eq_range_lift

theorem genHom : FreeGroupQuotLift n →* DihedralGroup n :=
  QuotientGroup.kerLift <| FreeGroup.lift (@genMap n)

theorem injective_genHom : Function.Injective <| @genHom n := by
  unfold genHom
  exact QuotientGroup.kerLift_injective <| FreeGroup.lift (@genMap n)

theorem surjective_genHom : Function.Surjective <| @genHom n := by
  intro g
  rcases g with i | i
  · use (FreeGroup.of (generator.a i) * FreeGroup.of (generator.b i))
    unfold genHom genMap
    simp only [sr_mul_r, map_mul, QuotientGroup.kerLift_mk, FreeGroup.lift.of,
      sr_mul_sr, add_sub_cancel]
  · use FreeGroup.of (generator.a i)
    unfold genHom genMap
    simp only [sr_mul_r, QuotientGroup.kerLift_mk, FreeGroup.lift.of]

theorem bijective_genHom : Function.Bijective <| @genHom n :=
  ⟨injective_genHom, surjective_genHom⟩

theorem RangeLift_eq_DihedralGroup : FreeGroupQuotLift n ≃* DihedralGroup n :=
  MulEquiv.ofBijective (@genHom n) (bijective_genHom)

-- | F / K | = | Dn |
theorem RangeLift_eq_DihedralGroup_card
    : Nat.card (FreeGroupQuotLift n) = Nat.card (DihedralGroup n) := by
  refine Nat.card_congr ?f
  exact (@RangeLift_eq_DihedralGroup n).toEquiv

-- | F / K | = 2n
theorem RangeLift_eq_2n_card : Nat.card (FreeGroupQuotLift n) = 2 * n := by
  rw [← nat_card]
  exact RangeLift_eq_DihedralGroup_card

@[simp]
lemma r_i_pow_n {i : ZMod n} [NeZero n] : r i ^ n = 1 := by
  have h1 : r 1 ^ i.val = r i := by
    simp only [r_one_pow, r.injEq]
    exact ZMod.nat_cast_zmod_val i
  have h2 : (r 1 ^ i.val) ^ n = r 1 ^ (i.val * n) := by
    exact Eq.symm (pow_mul (r 1 : DihedralGroup n) i.val n)
  have h3 : (r 1) ^ (i.val * n) = (1 : DihedralGroup n) := by
    simp only [r_one_pow, Nat.cast_mul, ZMod.nat_cast_val, ZMod.cast_id',
      id_eq, CharP.cast_eq_zero, mul_zero]; rfl
  rw [← h1, h2, h3]

lemma a_relsGenMap : (@genMap n (generator.a i)) * (@genMap n (generator.a i)) = (1 : DihedralGroup n) := by
  rw [genMap]; split
  · simp only [sr_mul_sr, sub_self]; rfl
  · simp only [sr_mul_r, sr_mul_sr, sub_self]; rfl

lemma b_relsGenMap : (@genMap n (generator.b i)) * (@genMap n (generator.b i)) = (1 : DihedralGroup n) := by
  rw [genMap]; split
  · simp only [sr_mul_sr, sub_self]; rfl
  · simp only [sr_mul_r, sr_mul_sr, sub_self]; rfl

lemma a_b_relsGenMap
    : ((@genMap n (generator.a i)) * (@genMap n (generator.b i))) ^ n = (1 : DihedralGroup n) := by
  simp_rw [genMap]
  simp only [sr_mul_r, sr_mul_sr, add_sub_cancel]
  cases n with
  | zero => simp only [Nat.zero_eq, pow_zero]
  | succ n => simp only [r_i_pow_n]

theorem one_of_Rels {i : ZMod n} : ∀ r ∈ (@Rels n i), FreeGroup.lift (@genMap n) r = 1 := by
  intro r hr
  simp only [Rels] at hr
  simp only [Set.union_singleton, Set.mem_singleton_iff, Set.mem_insert_iff] at hr
  rcases hr with hr₁ | hr₂ | hr₃
  · rw [hr₁]
    simp only [map_pow, map_mul, FreeGroup.lift.of, a_b_relsGenMap]
  · rw [hr₂]
    simp only [map_mul, FreeGroup.lift.of, b_relsGenMap]
  · rw [hr₃]
    simp only [map_mul, FreeGroup.lift.of, a_relsGenMap]

-- | F / N / K / N | = | F / K |
theorem thirdIsoThm_eq_RangeLift_card : Nat.card (@DihedralPresentedGroup n i ⧸ KerQuotClosure) =
    Nat.card (FreeGroupQuotLift n) := by
  simp only [FreeGroupQuotLift]
  refine Nat.card_congr ?f
  exact (PresentedGroup.thirdIsoThm (@one_of_Rels n i)).toEquiv

-- | F / N / K / N | = 2n
theorem thirdIsoThm_card_eq_2n
    : Nat.card (@DihedralPresentedGroup n i ⧸ KerQuotClosure) = 2 * n := by
  rw [← nat_card, ← RangeLift_eq_DihedralGroup_card]
  exact thirdIsoThm_eq_RangeLift_card

-- | F / N | = | K / N | * 2 * n
theorem dihedral_presented_group_eq_mul_2n_card : Nat.card (@DihedralPresentedGroup n i) =
    Nat.card (@KerQuotClosure n i) * (2 * n) := by
  sorry

-- 1 ≤ | K / N |
theorem ker_quot_closure_ge_one : 1 ≤ Nat.card (@KerQuotClosure n i) := by
  sorry

-- | F / N | ≤  2 * n
theorem dihedral_presented_group_le_2n_card
    : Nat.card (@DihedralPresentedGroup n i) ≤ 2 * n := by
  have h1 := @dihedral_presented_group_eq_mul_2n_card n i
  sorry

-- | F / K | ≤ | F / N |
theorem RangeLift_le_dihedral_presented_group_card : Nat.card (FreeGroupQuotLift n) ≤
    Nat.card (@DihedralPresentedGroup n i) := by
  -- Since N ≤ K then | F / K | ≤ | F / N |
  sorry

-- | F / N | ≥ 2 * n
theorem dihedral_presented_group_ge_2n_card : 2 * n ≤ Nat.card (@DihedralPresentedGroup n i) := by
  have h1 := @RangeLift_le_dihedral_presented_group_card n i
  rw [← RangeLift_eq_2n_card]
  linarith

-- | F / N | = 2 * n
theorem dihedral_presented_group_eq_2n_card : Nat.card (@DihedralPresentedGroup n i) = 2 * n := by
  have h1 := @dihedral_presented_group_ge_2n_card n i
  have h2 := @dihedral_presented_group_le_2n_card n i
  linarith

-- | F / K | = | F / N |
theorem RangeLift_eq_dihedral_presented_group_card
    : Nat.card (FreeGroupQuotLift n) = Nat.card (@DihedralPresentedGroup n i) := by
  rw [dihedral_presented_group_eq_2n_card, RangeLift_eq_2n_card]

-- | N | = | K |
theorem normalClosure_eq_kernel_card : Nat.card (Subgroup.normalClosure (@Rels n i)) =
    Nat.card (MonoidHom.ker (FreeGroup.lift (@genMap n))) := by
  have h1 := @RangeLift_eq_dihedral_presented_group_card n i
  simp only [FreeGroupQuotLift, DihedralPresentedGroup, PresentedGroup] at h1
  sorry

-- N = K
theorem normalClosure_eq_kernel
    : Subgroup.normalClosure (@Rels n i) = MonoidHom.ker (FreeGroup.lift (@genMap n)) := by
  -- Since N ≤ K and their orders are equal they are equal (finite groups)
  sorry

theorem DihedralPresentedGroup_eq_DihedralGroup : @DihedralPresentedGroup n i ≃* DihedralGroup n :=
  MulEquiv.trans (@factor_group_closure_ker n i) (RangeLift_eq_DihedralGroup)

end DihedralPresentedGroup

[Newell Jensen]

Also, I feel like I might need to show that the quotient groups I am dealing with are Fintype so that I can show that if N \leq K and their orders are equal that they therefore must be equal.

[Kyle Miller]

I think I'm not saying anything you're not already contemplating, but it would be nice to have an interface where you can give a Coxeter matrix to get a Coxeter group, vs doing a construction for each family individually.

There's a related family of groups, Artin-Tits groups, where the relation is that if you add in the relations that each generator's square is the identity you get Coxeter groups. Here's some old Lean 3 code for Artin-Tits groups: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/knot.20theory/near/280767378

For Artin-Tits groups, the $A_n$ family gives the braid groups, and for Coxeter groups it gives the symmetric groups, and the homomorphism from a braid group to a symmetric group you get by adding in these extra relations is a useful one.

[Kyle Miller]

What's the role of the ZMod n element in each generator? It looks like the set of relations only ever refers to the generators for a specific i, and I can't figure out what the function is of the other 2 * (n - i) generators is.

[Newell Jensen]

I originally had the definition without it but ran into problems trying to prove surjectivity/injectivity as the mapping to DihedralGroups generators ZMod argument wasn't lining up. This was something that was bugging me quite a bit actually. Maybe there is a way to do it without ZMod in the definition and still make everything work correctly but I wasn't seeing it.

[Oliver Nash]

I agree with @Kyle Miller that the there should be only two generators rather than a family (for fixed n). With only small modifications your code works for just two generators:

import Mathlib.GroupTheory.PresentedGroup
import Mathlib.GroupTheory.SpecificGroups.Dihedral

namespace DihedralGroup

@[simp] lemma r_one_zpow (n : ℕ) (i : ℤ) :
    r (1 : ZMod n) ^ i = r i := by
  obtain ⟨j, hj⟩ := i.eq_nat_or_neg
  rcases hj with rfl | rfl
  · simp
  · simp only [zpow_neg, zpow_coe_nat, r_one_pow, Int.cast_neg, Int.cast_ofNat]
    rfl -- Should probably be a `simp` lemma to avoid this `rfl` proof

end DihedralGroup

set_option autoImplicit true -- TODO Bump to latest Mathlib, remove this, and fix the errors

-- The code here in the PresentedGroup namespace would got inside of PresentedGroup in a separate PR
namespace PresentedGroup

variable {α : Type*}

variable {G : Type*} [Group G] {f : α → G} {rels : Set (FreeGroup α)}

-- mathport name: exprF
local notation "F" => FreeGroup.lift f

variable (h' : ∀ r ∈ rels, FreeGroup.lift f r = 1)

theorem thirdIsoThm : (FreeGroup α ⧸ Subgroup.normalClosure rels) ⧸
    Subgroup.map (QuotientGroup.mk' (Subgroup.normalClosure rels)) (MonoidHom.ker (FreeGroup.lift f)) ≃*
    FreeGroup α ⧸ MonoidHom.ker (FreeGroup.lift f) :=
  QuotientGroup.quotientQuotientEquivQuotient (Subgroup.normalClosure rels) (MonoidHom.ker F) (closure_rels_subset_ker h')

-- This theorem is an axiom of the definitons for Presentation of a Group in Dummit and Foote (3ed, pg. 218).
-- However, it seems that we should be proving this rather than adding it to the definition axioms.
theorem closure_rels_eq_ker : Subgroup.normalClosure rels = MonoidHom.ker F := by
  sorry

/-- Noether's first isomorphism theorem states G ⧸ ker φ ≃* range φ, i.e. FreeGroup α ⧸ ker F ≃* range F -/
theorem presented_group_eq_range_lift : PresentedGroup rels ≃* (FreeGroup α ⧸ MonoidHom.ker F) := by
  refine MulEquiv.symm (QuotientGroup.quotientMulEquivOfEq ?h)
  rw [← closure_rels_eq_ker]

end PresentedGroup


open DihedralGroup

namespace DihedralPresentedGroup

inductive generator (n : ℕ)
  | a : generator n
  | b : generator n
  deriving DecidableEq

def genMap : generator n → DihedralGroup n
  | generator.a => sr 1
  | generator.b => sr 1 * r 1

/-- The presentation of the Dihedral group which makes it a Coxeter group is
⟨a, b | a^2 = 1, b^2 = 1, (a * b)^n = 1⟩ -/
def Rels : Set (FreeGroup (generator n)) :=
  {FreeGroup.of generator.a * FreeGroup.of generator.a} ∪
  {FreeGroup.of generator.b * FreeGroup.of generator.b} ∪
  {(FreeGroup.of generator.a * FreeGroup.of generator.b) ^ n}

@[simp] abbrev DihedralPresentedGroup {n : ℕ} := PresentedGroup <| @Rels n
@[simp] abbrev KerQuotClosure {n : ℕ} := Subgroup.map (QuotientGroup.mk'
  (Subgroup.normalClosure (@Rels n))) (MonoidHom.ker (FreeGroup.lift (@genMap n)))
@[simp] abbrev FreeGroupQuotLift (n : ℕ) :=
  FreeGroup (generator n) ⧸ MonoidHom.ker (FreeGroup.lift (@genMap n))

noncomputable
def factor_group_closure_ker : @DihedralPresentedGroup n ≃* FreeGroupQuotLift n :=
  PresentedGroup.presented_group_eq_range_lift

def genHom : FreeGroupQuotLift n →* DihedralGroup n :=
  QuotientGroup.kerLift <| FreeGroup.lift (@genMap n)

theorem injective_genHom : Function.Injective <| @genHom n :=
  QuotientGroup.kerLift_injective <| FreeGroup.lift (@genMap n)

theorem surjective_genHom : Function.Surjective <| @genHom n := by
  let a : FreeGroup (generator n) := FreeGroup.of generator.a
  let b : FreeGroup (generator n) := FreeGroup.of generator.b
  intro g
  rcases g with i | i
  · use (a * b) ^ (i : ℤ)
    simp [genHom, genMap]
  · use a * (a * b) ^ (i - 1 : ℤ)
    simp only [genHom, genMap, sr_mul_r, QuotientGroup.kerLift_mk, FreeGroup.lift.of]
    simp

theorem bijective_genHom : Function.Bijective <| @genHom n :=
  ⟨injective_genHom, surjective_genHom⟩

noncomputable
def RangeLift_eq_DihedralGroup : FreeGroupQuotLift n ≃* DihedralGroup n :=
  MulEquiv.ofBijective (@genHom n) (bijective_genHom)

noncomputable
def DihedralPresentedGroup_eq_DihedralGroup : @DihedralPresentedGroup n ≃* DihedralGroup n :=
  (@factor_group_closure_ker n).trans (RangeLift_eq_DihedralGroup)

[Kyle Miller]

I've been puzzled about how the original version managed to prove that the cardinality is 2 * n even though DihedralPresentedGroup was an infinite group. @Floris van Doorn and I were discussing it, and he noticed that the first sorry'd theorem is not true:

theorem closure_rels_eq_ker : Subgroup.normalClosure rels = MonoidHom.ker F := by
  sorry

What if f maps everything to the identity? The h' hypothesis allows this, but then MonoidHom.ker F is the top subgroup. The fix seems to be that Subgroup.normalClosure rels is a subgroup of MonoidHom.ker F.

[Newell Jensen]

Yea, when I originally had defined the generators I wasn't passing it n, and not doing that was driving me crazy! More evidence that getting the definitions correct is very important. Thanks for the help. I have updated my code with your changes @Oliver Nash . Now, in regards to:

theorem closure_rels_eq_ker : Subgroup.normalClosure rels = MonoidHom.ker F := by
  sorry

from my understanding this is a true statement (if we have the hypothesis that Subgroup.normalClosure rels is a subgroup of MonoidHom.ker F). Is this what you meant @Kyle Miller ?

[Kyle Miller]

I think h' is equivalent to Subgroup.normalClosure rels being a subgroup of MonoidHom.ker F

[Newell Jensen]

After getting distracted in a rabbit hole of trying to prove that the Dihedral group is isomorphic to its presentation group I have finally come around back to Coxeter groups. This is what I have cooked up so far for definitions. Thoughts @Oliver Nash?:

import Mathlib.Data.Matrix.Notation
import Mathlib.GroupTheory.PresentedGroup

/-!
# Coxeter Systems

This file develops Coxeter Systems.  The pair `(W, S)` where `W` is a Coxeter group with
generators `S = {r₁, r₂, ... , rₙ}` is called a Coxeter System.
-/

universe u

variable {n : ℕ} {B : Type u} [Fintype B]

variable (M : Matrix (Fin n) (Fin n) ℕ)

namespace CoxeterSystem

inductive Generators (n : ℕ) : Type
  | r : Fin n → Generators n

namespace Relations

/-- The relation terms corresponding to a Coxeter matrix. -/
def ofMatrix : (Fin n) × (Fin n) → FreeGroup (Generators n) :=
  Function.uncurry fun i j =>
    (FreeGroup.of (Generators.r i) * FreeGroup.of (Generators.r j)) ^ M i j

/-- The relations of the Coxeter System. -/
def toSet : Set (FreeGroup (Generators n)) :=
  Set.range <| ofMatrix M

end Relations

/-- The Presentation Coxeter group corresponding to a Coxeter matrix.

Note that it is defined for any matrix of natural numbers.
Its value for non-Coxetermatrices should be regarded as junk. -/
abbrev CoxeterGroup := PresentedGroup <| @Relations.toSet n M

structure CoxeterSystem : Type where
  /-- `W` is a CoxeterGroup. -/
  W : @CoxeterGroup n M
  /-- `S` are the generators of `W`. -/
  S : Generators n

end CoxeterSystem

namespace CoxeterMatrix

/-- The Coxeter matrix of type A₂.

The corresponding Coxeter diagram is:

o --- o

-/
def A₂ : Matrix (Fin 2) (Fin 2) ℕ :=
  !![1, 3; 3, 1]

/-- The Coxeter matrix of type Aₙ.

The corresponding Coxeter diagram is:

o --- o --- o ⬝ ⬝ ⬝ ⬝ o --- o

-/
def Aₙ : Matrix (Fin n) (Fin n) ℕ :=
  Matrix.of (fun i j => if i == j then 1 else 3)

end CoxeterMatrix

namespace CoxeterSystem

/-- Example: Finite Coxeter group A₂. -/
abbrev A₂ := CoxeterGroup CoxeterMatrix.A₂

/-- Finite Coxeter System for Aₙ. -/
abbrev Aₙ := CoxeterSystem (@CoxeterMatrix.Aₙ n)

end CoxeterSystem

[Newell Jensen]

(deleted)

[Joël Riou]

I would think you could replace Fin n by any type S such that [Finite S]. Also, I am confused with your definition of CoxeterSystem. The CoxeterGroup M you define is already the type of elements of a group (defined by generators and relations). Then, W : CoxeterGroup M is an element in this group; presumably, it is not what you intented. I am not expert in Coxeter groups, but some references allow matrices with \inftyentries (using 0 instead should be fine though).
(There might be some typo in your definition of Aₙ because I understand that generators should commute if their indices are further enough).

[Newell Jensen]

Ah yes, looks like I was half way inbetween doing that with B.

[Newell Jensen]

Let me update that.

[Newell Jensen]

import Mathlib.Data.Matrix.Notation
import Mathlib.GroupTheory.PresentedGroup

/-!
# Coxeter Systems

This file develops Coxeter Systems.  The pair `(W, S)` where `W` is a Coxeter group with
generators `S = {r₁, r₂, ... , rₙ}` is called a Coxeter System.
-/


universe u

variable {n : ℕ} {B : Type u} [DecidableEq B] [Fintype B]

variable (M : Matrix B B ℕ)

namespace CoxeterGroup

variable (B)

inductive Generators
  | r : B → Generators

instance [Inhabited B] : Inhabited (Generators B) :=
  ⟨Generators.r default⟩

variable {B}

namespace Relations

/-- The relation terms corresponding to a Coxeter matrix. -/
def ofMatrix : B × B → FreeGroup (Generators B) :=
  Function.uncurry fun i j =>
    (FreeGroup.of (Generators.r i) * FreeGroup.of (Generators.r j)) ^ M i j

/-- The relations of the Coxeter group. -/
def toSet : Set (FreeGroup (Generators B)) :=
  Set.range <| ofMatrix M

end Relations

end CoxeterGroup

/-- The Presentation Coxeter group corresponding to a Coxeter matrix.

Note that it is defined for any matrix of natural numbers.
Its value for non-Coxeter matrices should be regarded as junk. -/
def Matrix.ToCoxeterGroup := PresentedGroup <| @CoxeterGroup.Relations.toSet B M

structure CoxeterSystem where
  /-- `W` is a CoxeterGroup. -/
  W : Matrix.ToCoxeterGroup M
  /-- `S` are the generators of `W`. -/
  S : CoxeterGroup.Generators B

namespace CoxeterMatrix

/-- The Coxeter matrix of type A₂.

The corresponding Coxeter diagram is:

o --- o

-/
def A₂ : Matrix (Fin 2) (Fin 2) ℕ :=
  !![1, 3; 3, 1]

/-- The Coxeter matrix of type Aₙ.

The corresponding Coxeter diagram is:

o --- o --- o ⬝ ⬝ ⬝ ⬝ o --- o

-/
def Aₙ : Matrix (Fin n) (Fin n) ℕ :=
  Matrix.of (fun i j => if i == j then 1 else 3)

end CoxeterMatrix

namespace CoxeterSystem

/-- Example: Finite Coxeter group A₂. -/
abbrev A₂ := CoxeterSystem <| CoxeterMatrix.A₂

/-- Finite Coxeter System for Aₙ. -/
abbrev Aₙ := CoxeterSystem <| @CoxeterMatrix.Aₙ n

end CoxeterSystem

[Newell Jensen]

@Joël Riou when I spoke with @Oliver Nash about this a bit he mentioned defining CoxeterSystem as a structure that will have the Coxeter group and also the generators of that group. I could be doing it totally wrong here, or maybe it just seems odd with how the definitions are setup since I am using PresentedGroup for generating the Coxeter group. I am not sure.

[Joël Riou]

As I said, what you have formalized is not what you intended to formalize. What makes sense is, given a matrix M with some index set S, a group W and a map S → W, a condition IsCoxeterGroup which would assert that the given elements in W satisfies the relations and that the morphism M.toCoxeterGroup → W from the constructed presented group is an isomorphism. In other words, for each matrix M, there is an "abstract" group defined by generators and relations (as a quotient of the free group), and we may also have particular "models" of it. For example, it would be interesting to show that the symmetric group in n+1 letters equipped with the transpositions (i i+1) satisfies the property IsCoxeterGroup for An.

[Oliver Nash]

I'm also no expert on Coxeter groups but two things strike me after comparing the above code with Bourbaki:

1. In Bourbaki a Coxeter system is the data of a group W and a subset S of W subject to hypotheses.
2. In Bourbaki, the subset S is not required to be finite.

My null hypothesis would be that following Bourbaki is the right approach. Have you considered doing this?

I don't know if 2 matters, but I would check the wider literature to see (my guess is yes).

[Sebastien Gouezel]

Instead of a subset as in Bourbaki, we should probably use a map from another type, as we do for bases in linear algebra: this design has proved to be more flexible than the set-based one.

[Oliver Nash]

Good point, agreed!

I still want to emphasise that the data that forms part of a Coxeter system should (I think) be a group (as in Bourbaki) and not the data of a presentation (as in code snippet above).

[Sebastien Gouezel]

I think we should have three kind of objects:

• CoxeterGroup M, as the concrete Coxeter group associated to a matrix M subject to some conditions
• CoxeterBasis M G: given a group G, this would record an isomorphism between CoxeterGroup M and G. Equivalently, this can be seen as a list of generators of G parameterized by the underlying type of M, together with the fact that they satisfy exactly the relations we want.
• IsCoxeterGroup G would be a Prop-valued typeclass registering the existence of a Coxeter basis of G, for some M.

We already do that for free groups, or for localizations, or for any construction that has concrete instances which are not definitionally the preferred construction.

[Newell Jensen]

Awesome, thanks for the guidance everyone. :)

[Newell Jensen]

Hello again. I wanted to get feedback to make sure I am on the right track. Here is what I have come up with so far:

import Mathlib.Data.Matrix.Notation
import Mathlib.GroupTheory.PresentedGroup
import Mathlib.GroupTheory.SpecificGroups.Dihedral
import Mathlib.LinearAlgebra.Matrix.Symmetric


noncomputable section

variable {B : Type*} [DecidableEq B] [Fintype B]

variable (M : Matrix B B ℕ)

variable (B)

inductive Generators
  | r : B → Generators

instance [Inhabited B] : Inhabited (Generators B) :=
  ⟨Generators.r default⟩

/-- A Coxeter matrix is a B × B symmetric matrix with ones on the diagonal
  and off-diagonal elements greater than or equal to 2. -/
def Matrix.IsCoxeter (M : Matrix B B ℕ) : Prop :=
    (∀ i j : B, (i = j → M i j = 1) ∧ (i ≠ j → 2 ≤ M i j)) ∧ M.IsSymm

namespace CoxeterGroup

variable {B}

namespace Relations

/-- The relation terms corresponding to a Coxeter matrix. -/
def ofMatrix : B × B → FreeGroup (Generators B) :=
  Function.uncurry fun i j =>
    (FreeGroup.of (Generators.r i) * FreeGroup.of (Generators.r j)) ^ M i j

/-- The relations corresponding to a Coxeter matrix. -/
def toSet : Set (FreeGroup (Generators B)) :=
  Set.range <| ofMatrix M

end Relations

end CoxeterGroup

/-- The group presentation corresponding to a Coxeter matrix.

Note that it is defined for any matrix of natural numbers. Its value for non-Coxeter
matrices should be regarded as junk. `IsCoxeterGroup` checks that the matrix `IsCoxeter`. -/
abbrev Matrix.ToCoxeterPresentation := PresentedGroup <| CoxeterGroup.Relations.toSet M

structure CoxeterGroupBasis (W : Type*) [Group W] where
  /-- `CoxeterGroupBasis.ofRepr` constructs a basis given an equivalence with the group
  presentation corresponding to a Coxeter matrix `M`. -/
  ofRepr ::
    /-- `repr` is the isomorphism between the group `W` and the group presentation
    corresponding to a Coxeter matrix `M`. -/
    repr : W ≃* Matrix.ToCoxeterPresentation B M

class IsCoxeterGroup (W : Type*) [Group W] : Prop where
  nonempty_basis : ∃ (M : Matrix B B ℕ), M.IsCoxeter ∧ Nonempty (CoxeterGroupBasis B M W)

namespace CoxeterMatrix

variable {n : ℕ}

/-- The Coxeter matrix of type A₂.

The corresponding Coxeter diagram is:

o --- o

-/
def A₂ : Matrix (Fin 2) (Fin 2) ℕ :=
  !![1, 3; 3, 1]

theorem A₂IsCoxeter : A₂.IsCoxeter := by
  simp [Matrix.IsCoxeter, Matrix.IsSymm]

end CoxeterMatrix

open CoxeterMatrix

-- EXAMPLE: DihedralGroup 3 equivalant to the group presentation corresponding to
-- Coxeter matrix `A₂`.
def DihedralGroup3EquivCoxeterGroup :
    DihedralGroup 3 ≃* Matrix.ToCoxeterPresentation _ A₂ :=
  sorry -- Suppose we have a proof

def DihedralGroup3HasCoxeterGroupBasis :
    CoxeterGroupBasis (Fin 2) A₂ (DihedralGroup 3) :=
  CoxeterGroupBasis.ofRepr DihedralGroup3EquivCoxeterGroup

theorem DihedralGroup3IsCoxeterGroup : IsCoxeterGroup (Fin 2) (DihedralGroup 3) :=
  ⟨A₂, ⟨A₂IsCoxeter, Nonempty.intro DihedralGroup3HasCoxeterGroupBasis⟩⟩

[Kevin Buzzard]

The sorried theorem should be a def because it's data, it's not a proof of the statement "these groups are isomorphic", it's the claim that a given map is an isomorphism. Same for the "theorem" after. But this looks good to me -- try filling in the sorry!

[Newell Jensen]

The example was just to make sure I was getting the definitions right. First I would like to nail down the definitions before working on proofs. If no objections, yeah, time to start working on proofs :upside_down:

[Kevin Buzzard]

Well that sorry is still hiding two more definitions :-)

[Kevin Buzzard]

docs#MulEquiv

Looks to me like the thing you have to prove is a group homomorphism is the left-to-right function, so I suggest you flip the two sides of DihedralGroup3EquivCoxeterGroup because you'll get that the map from the presentation to D_3 is a group hom for free.

I think that before you start on this it might be easier to establish a presentation (any presentation will do, I should imagine) of D_3. Otherwise your proofs will be a case bash hell. It should be pretty easy to prove that a map between presentations is an isomorphism, but the defniition of D_3 in mathlib is a case bash.

docs#DihedralGroup

[Newell Jensen]

Kevin Buzzard said:

docs#MulEquiv

Looks to me like the thing you have to prove is a group homomorphism is the left-to-right function, so I suggest you flip the two sides of DihedralGroup3EquivCoxeterGroup because you'll get that the map from the presentation to D_3 is a group hom for free.

Interesting... I wasn't aware that switching sides would have this effect. Still trying to see what you are talking about here.

[Kevin Buzzard]

If you figure out a presentation of D_3 then you won't need to flip. What I'm envisaging here (with any presentation, not just the one you're using here) is that it's easy to write down a group hom from <Gens|Rels> to D_3 as defined by mathlib, and to prove it's a surjection, but to prove it's a bijection you will have to do something like write down a map from D_3 back to the presentation and prove that this is a two-sided inverse. Perhaps the easiest way to do this would be by proving that the map back is also a group hom (by a case split, so this would be 4 checks) and then showing that it sends each generator back to itself. And my gut feeling is that the calculations are going to be much easier if you use the usual generators of order n and 2, rather than generators of order 2, for this argument (which I think you're not going to be able to get away from).

My instinct is that it will be less painful to present D_n in the usual way and then finish the job from there, than by launching straight into the sorry, but maybe it ends up being the same amount of work either way.

I guess another advantage of giving the presentation for D_n is that it's useful for other people.

[Newell Jensen]

Ah I think I understand what you were referring to above in terms of one direction free. The lifting of the hom between the free group to D_n, which becomes the presentation to D_n is given to us.

I don't know how to prove there is a bijection. The issue I had when trying to prove this is that the map from D_n to the presentation is easy to prove cause you can just match on the constructors of D_n, but going in the opposite direction what do you match on? The presentation is a quotient group and therefore you are dealing with cosets. I at least didn't see an easy way of doing this.

[Newell Jensen]

I tried unfolding the layers on the definitions to get towards the map that underlies the presentation but that didn't help.

[Kevin Buzzard]

To prove that D_n = <a,b|a^n=b^2=1,bab=a^{-1}> I would first write down a group hom from the presented group to D_n (easy), then write down a set-theoretic map from D_n to <a,b> (two cases), then prove that the set-theoretic map is a group hom (4 cases), then prove that the composite in both directions is the identity. If you choose your maps wisely then showing that D_n -> <a,b> -> D_n is the identity should basically be rfl in both cases. To go the other way, just check that a goes to a and b to b.

[Newell Jensen]

In so many words this is the two-sided inverse no? I was able to prove one direction but not the other.

[Newell Jensen]

I don't know how to deconstruct the terms of the presentation and not sure there is a good way of doing this. However, I didn't try with the presentation you mentioned and I only tried with <a,b | a^2 = 1, b^2 = 1, (ab)^n=1>

[Newell Jensen]

From the proofs I have found in the literature they do a counting argument by showing the multiplicative closure of the set of the left cosets of the normal closure of the relations, but this is something I haven't tried to formalize yet. Additionally, I they are doing it on D_4 and this would need to be extrapolated to D_n which seems cumbersome.

[Kevin Buzzard]

I mean I guess you can use that presentation, it will just make the algebra a bit messier. You don't need any counting as my argument shows.

[Newell Jensen]

Kevin Buzzard said:

To prove that D_n = <a,b|a^n=b^2=1,bab=a^{-1}> I would first write down a group hom from the presented group to D_n (easy), then write down a set-theoretic map from D_n to <a,b> (two cases), then prove that the set-theoretic map is a group hom (4 cases), then prove that the composite in both directions is the identity. If you choose your maps wisely then showing that D_n -> <a,b> -> D_n is the identity should basically be rfl in both cases. To go the other way, just check that a goes to a and b to b.

This last sentence, I don't see how you can do that. Maybe you can you show me what you are talking about. How do you get the generators a and b isolated from <a, b>?

[Junyan Xu]

That would be docs#PresentedGroup.of.

[Newell Jensen]

I just threw up a WIP PR #8195 of what I have in regards to the recent conversation (not Coxeter groups) and I haven't tried getting past where I currently am for several weeks now but any suggestions welcome @Kevin Buzzard (or anyone else) in regards to what you were mentioning above . I still haven't figured out the map you mention in regards to <a, b> -> D_n -> <a, b> as you see in what I am currently calling leftInverseHoms (don't mind the WIP names).

[Kevin Buzzard]

To prove that two group homomorphisms from a presented group to some other group are equal, it suffices to prove that the generators get mapped to the same things. Hence to prove that a group homomorphism from a presented group to itself is the identity, it suffices to check that the generators get mapped to themselves.

[Joël Riou]

Newell Jensen said:

inductive Generators
  | r : B → Generators

I do not think that this definition is necessary. You may just use FreeGroup B below, right?
(Otherwise, the code looks much better!)

[Newell Jensen]

Thanks!

AFAIK we need a way to index the $n$ different generators $\{r_1, \dots, r_n\}$ and I don't see how to do that with FreeGroup B by itself.

[Joël Riou]

I do not think that you need a bijection between Fin n and B and I do not understand why creating an auxiliary type equivalent to B would be relevant here. If you just replace FreeGroup (Generators B) by FreeGroup B, and remove Generators.r everywhere, your code still compiles.

[Newell Jensen]

Yes, you are right, when I had tried to make the changes before commenting above I had made a mistake. It does compile. Thanks for your persistence with me!

[Newell Jensen]

Here is #8223 if anyone is up for a review.