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.

[Newell Jensen]

(deleted)

[Newell Jensen]

(deleted)

[Newell Jensen]

Hello all.

Except from some minor nits that I need to fix and one last proof, AFAICT #8223 seems to be close to being done (at least for the first PR). However, the last proof (the only sorry left) is turning out to to be rather difficult to prove, at least for me, with the current PresentedGroup API. See here for the code of the PR

I have been thinking that I will need to develop the API of PresentedGroup similar to how FreeGroup is developed by using word reductions using the relations to then prove the associated equivalent of FreeGroup.of_injective.

What I had in mind was to:

1. Define an inductive type such as:
   inductive PresentedGroup.Red.Step : FreeGroup B → FreeGroup B → Prop | not {F₁ F₂} : ∀ g, ∀ r ∈ rels, PresentedGroup.Red.Step (F₁ * g * r * g⁻¹ * F₂) (F₁ * F₂)
   [or would it be better to go a level lower to the Lists that underlie the FreeGroup type? Would doing so make the reduction lemmas/proofs easier than dealing with terms of FreeGroup??]

The reason I have the definition as above is that PresentedGroup is the quotient of the free group by the normal closure of the relations and the set of the normal closure of the relations is the conjugation of the elements of the relations by the elements of the free group.

2. After creating the appropriate inductive type above I would then proceed by proving any needed lemmas so that I can define the associated equivalent of FreeGroup, which would be the quotient of the reductive step (1).
3. I would then proceed to prove that the definition in (2) is a Group and that it is isomorphic to the PresentedGroup using the same relations (this is why I am using conjugation in the inductive definition (1)).
4. Define the of definition for the new group we have constructed in (3) and prove that it is injective.

If this is a viable approach the next big question is the []-concern above, on whether going to one level lower in the definition, i.e. to List, will make everything easier for myself?

Hopefully what I am brainstorming above seems plausible. Any and all suggestions are welcome. I am trying to get feedback on whether my idea seems viable, or if there is a better way to prove this last sorry'd theorem. I am all ears so please let me know what you think!

[Kim Morrison]

What exactly is the sorry? That different Coxeter matrices give different groups?

[Kim Morrison]

Maybe I'm misunderstanding, as that doesn't seem useful?

[Newell Jensen]

In the PR the sorry is for:

theorem of_injective : Function.Injective (CoxeterGroup.of M) :=
    sorry

which I am thinking should be analogous to how FreeGroup.of_injective is injective when taking into account the word reductions from the conjugations of the relations. Or that is the idea at least. Am I making sense?

[Kim Morrison]

In informal maths what do these two statements say?

[Junyan Xu]

I think it says the generators are distinct in the Coxeter group they generate.

[Kim Morrison]

If so, that's both an excellent statement to have, but also probably not actually necessary in the first PR.

[Joël Riou]

Newell Jensen said:

Except from some minor nits that I need to fix and one last proof, AFAICT #8223 seems to be close to being done (at least for the first PR). However, the last proof (the only sorry left) is turning out to to be rather difficult to prove, at least for me, with the current PresentedGroup API. See here for the code of the PR

There is no immediate need to prove this sorry. The first PR is already long enough!

For this sorry, there are different approaches. Certainly, some properties cannot be proven easily for any CoxeterSystem (i.e. a group G equipped with generators satisfying a certain presentation), and it may not be easy even for the constructed PresentedGroup. If you see general improvements that can be made to the PresentedGroup API: like a criteria on "words" which would be an equivalence relation defined by induction, that would be nice. For the case of Coxeter groups, you may even have to use a more specially designed "model" using words involving the elements in s : B (as the generators are of order 2, we do not need the inverses): some lemmas and definitions in Bourbaki involve such words. Then, it would be useful to have a definition, given a Coxeter matrix M and two Coxeter systems for the same M, of an isomorphism between the corresponding groups: this would help translating results obtained for a model to any another.

[Newell Jensen]

Thanks for the responses everyone. I removed the theorems that relied open this sorry and for a first PR think that #8223 is ready for another review.

[Johan Commelin]

CI is unhappy...

[Newell Jensen]

Johan Commelin said:

CI is unhappy...

Fixed lint

[Johan Commelin]

@Newell Jensen I left a review. I really like the fact that Coxeter groups are converging to mathlib!

[Newell Jensen]

Johan Commelin said:

Newell Jensen I left a review. I really like the fact that Coxeter groups are converging to mathlib!

@Johan Commelin thanks for the review (I updated the branch yesterday with your review suggestions)!

[Newell Jensen]

bors is failing for #8223

Locally I tried to remedy the situation:

$ rm -rf .lake/
$ lake exe cache get
info: std: cloning https://github.com/leanprover/std4 to './.lake/packages/std'
info: Qq: cloning https://github.com/leanprover-community/quote4 to './.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to './.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to './.lake/packages/proofwidgets'
info: Cli: cloning https://github.com/leanprover/lean4-cli to './.lake/packages/Cli'
info: importGraph: cloning https://github.com/leanprover-community/import-graph.git to './.lake/packages/importGraph'
info: [0/9] Downloading proofwidgets cloud release
info: [0/9] Unpacking proofwidgets cloud release
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [6/9] Compiling Cache.Main
info: [9/9] Linking cache
installing leantar 0.1.11
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
100 1906k  100 1906k    0     0  1329k      0  0:00:01  0:00:01 --:--:-- 5959k

Attempting to download 4209 file(s)
Downloaded: 4204 file(s) [attempted 4209/4209 = 100%] (99% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
Decompressing 4204 file(s)
/home/newell/.cache/mathlib/ab5318f242094577.ltar: removing corrupted file
unpacked in 1980 ms
$ lake build
[5/12] Building Mathlib.Mathport.Rename
[2403/4207] Building Mathlib.GroupTheory.SpecificGroups.Coxeter
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/importGraph/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/build/lib /home/newell/.elan/toolchains/leanprover--lean4---v4.6.0-rc1/bin/lean -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false ./././Mathlib/GroupTheory/SpecificGroups/Coxeter.lean -R ././. -o ./.lake/build/lib/Mathlib/GroupTheory/SpecificGroups/Coxeter.olean -i ./.lake/build/lib/Mathlib/GroupTheory/SpecificGroups/Coxeter.ilean -c ./.lake/build/ir/Mathlib/GroupTheory/SpecificGroups/Coxeter.c
error: stdout:
./././Mathlib/GroupTheory/SpecificGroups/Coxeter.lean:163:49: error: application type mismatch
  FunLike (CoxeterSystem M W) B fun x ↦ W
argument
  fun x ↦ W
has type
  ?m.2568 → Type u_4 : Sort (max (u_4 + 2) ?u.2567)
but is expected to have type
  Sort ?u.2548 : Type ?u.2548
./././Mathlib/GroupTheory/SpecificGroups/Coxeter.lean:170:49: error: unknown constant 'FunLike.congr_fun'
./././Mathlib/GroupTheory/SpecificGroups/Coxeter.lean:174:8: warning: declaration uses 'sorry'
./././Mathlib/GroupTheory/SpecificGroups/Coxeter.lean:178:76: error: unknown constant 'FunLike.coe_injective'
./././Mathlib/GroupTheory/SpecificGroups/Coxeter.lean:181:8: warning: declaration uses 'sorry'
./././Mathlib/GroupTheory/SpecificGroups/Coxeter.lean:189:8: warning: declaration uses 'sorry'
./././Mathlib/GroupTheory/SpecificGroups/Coxeter.lean:235:8: warning: declaration uses 'sorry'
./././Mathlib/GroupTheory/SpecificGroups/Coxeter.lean:245:8: warning: declaration uses 'sorry'
./././Mathlib/GroupTheory/SpecificGroups/Coxeter.lean:268:39: error: tactic 'aesop' failed, made no progress
B : Type u_1
inst✝ : DecidableEq B
M : Matrix B B ℕ
n : ℕ
⊢ Matrix.IsSymm (Aₙ n)
./././Mathlib/GroupTheory/SpecificGroups/Coxeter.lean:284:39: error: tactic 'aesop' failed, made no progress
B : Type u_1
inst✝ : DecidableEq B
M : Matrix B B ℕ
n : ℕ
⊢ Matrix.IsSymm (Bₙ n)
./././Mathlib/GroupTheory/SpecificGroups/Coxeter.lean:303:39: error: tactic 'aesop' failed, made no progress
B : Type u_1
inst✝ : DecidableEq B
M : Matrix B B ℕ
n : ℕ
⊢ Matrix.IsSymm (Dₙ n)
./././Mathlib/GroupTheory/SpecificGroups/Coxeter.lean:316:49: error: tactic 'aesop' failed, made no progress
B : Type u_1
inst✝ : DecidableEq B
M : Matrix B B ℕ
n m : ℕ
⊢ Matrix.IsSymm (I₂ₘ m)
error: external command `/home/newell/.elan/toolchains/leanprover--lean4---v4.6.0-rc1/bin/lean` exited with code 1

Any ideas on what to do?

[Newell Jensen]

My local branch is up to date with upstream as well so not really sure what to do to fix the corruption.

[Newell Jensen]

Ah, maybe delete the .cache? ...

[Oliver Nash]

I doubt this is an issue with local state (cache etc) on your machine. If you have merged master then push your branch up to GitHub and I'll see if I can quickly fix the errors.

[Newell Jensen]

@Oliver Nash the last commit was with git merge origin/master so go ahead and have a go.

[Oliver Nash]

I pushed a commit which turns the errors into sorrys.

[Newell Jensen]

But why are there errors? Is this just the build state that is erroring for some reason?

[Newell Jensen]

I wasn't having any issues before with CI etc., so not sure what is going on.

[Oliver Nash]

I don't understand your second question but the answer to the first is that your branch was incompatible with changes that had been made to master since you created it.

[Newell Jensen]

oh yeah, duh. :stuck_out_tongue_closed_eyes: I was confused because I thought I was up to date and the CI had passed but that was before I merged master. It must have been a very recent change because CI passed yesterday I believe with what I had.

[Oliver Nash]

I am surprised that the (autoparameter) by aesop were previously succeeding but no longer are.

[Matthew Ballard]

Timeout?

[Oliver Nash]

A low-level hand proof would probably begin something like:

symmetric := by
    simp only [Matrix.IsSymm]
    ext i j
    rcases eq_or_ne j i with rfl | h; · simp
    -- ...

[Oliver Nash]

Matthew Ballard said:

Timeout?

Can we test this by manually bumping aesop's time budget?

[Matthew Ballard]

I think a set option on the declaration should work

[Newell Jensen]

I already fixed those with symmetric := by simp [Matrix.IsSymm]; aesop

[Newell Jensen]

Should have the PR ready again here in a bit once I update the rest.

[Newell Jensen]

But yeah, seems something changed with aesop

[Oliver Nash]

So effectively it was necessary to make the change:

- symmetric := by aesop
+ symmetric := by simp [Matrix.IsSymm]; aesop

(albeit autoparameters mean this isn't how it looks in the source).

[Oliver Nash]

@Jannis Limperg any thoughts?

[Jannis Limperg]

I wouldn't expect Aesop to close these goals since Matrix.Symm is a def, which Aesop (and many other tactics) don't unfold by default. Why it managed to solve it anyway I can't say since the PR branch is gone. However, you can tell Aesop to always unfold Matrix.Symm when working on proofs of symmetric:

local macro "aesop_symm" : tactic => `(tactic| aesop (add norm simp Matrix.IsSymm))

/-- A matrix `IsCoxeter` if it is a symmetric matrix with diagonal entries equal to one
and off-diagonal entries distinct from one. -/
structure Matrix.IsCoxeter : Prop where
  symmetric : M.IsSymm := by aesop_symm
  diagonal : ∀ b : B, M b b  = 1 := by aesop
  off_diagonal : ∀ b₁ b₂ : B, b₁ ≠ b₂ → M b₁ b₂ ≠ 1 := by aesop

The macro is necessary because auto-param tactics aren't allowed to contain identifiers. :(

[Newell Jensen]

Ah I remember the change now. It was because the definition of IsCoxeter was changed from a class to a structure.

[Newell Jensen]

Somehow aesop handles these differently it seems (of which I have no idea of the inner workings unfortunately).

[Jannis Limperg]

That would surprise me. Are you sure it wasn't the merge of master, which pulled in a commit that updated Aesop?

[Newell Jensen]

No I am not sure. That could very well be the reason.

[Newell Jensen]

Actually, yes come to remember this must have been the reason as merging master broke what I had. Go ahead and ignore the above!

[Newell Jensen]

However, the change that master pulled in could have updated how Aesop handles structure vs. class and thus maybe not ignore everything that I said above :joy: :shrug:

[Newell Jensen]

I suppose this is an invitation to myself to remove at least part of my ignorance of how Aesop works and go take a look at the code itself... :man_walking:

[Jannis Limperg]

I'm the primary author of Aesop and I would be very surprised if class vs structure made a difference here. But I'd be grateful if you could investigate further and isolate the change in behaviour. The update I mentioned shouldn't have affected the behaviour of Aesop in this instance, so something fishy may be going on.

[Óscar Álvarez]

Hi everyone,

As part of my master’s thesis, I formalized some results about Coxeter groups, including the strong exchange theorem and partial work on Matsumoto's theorem. The Lean code is available here: DemazureOperatorsLean.

If there’s interest, I’d be happy to work on introducing these into mathlib. Let me know what you think!

[metakuntyyy]

Hey @Óscar Álvarez your master thesis is really good and well written. You give clear, concise and useful examples. Would you be interested in making it available as a tutorial here https://leanprover-community.github.io/mathlib-overview.html?

It also answered questions about polynomials here #mathlib4 > Adding more examples to mathlib especially that you make the distinction of eval and eval2, which I didn't understand until I have read p.9 of your thesis.

[Johan Commelin]

@Óscar Álvarez Congratulations! If you want to PR (parts of) this to mathlib, I would be very happy to review your PRs.

[Johan Commelin]

@Hannah Fechtner you might also be interested in :up:

[Johan Commelin]

(Given the connection with Coxeter theory.)

[Óscar Álvarez]

@metakuntyyy Thanks a lot, I’m really happy to hear that you found my thesis helpful. The page you linked seems more like a collection of mathlib docs than a tutorial, but if you think it fits somewhere, I’d be happy to contribute. Either way, you can also feel free to use and share the LaTeX source however you’d like.

[Óscar Álvarez]

@Johan Commelin Thank you! I will start working towards a small PR to get used to the process.

[Óscar Álvarez]

@Johan Commelin Hi, I opened a PR (#19663) with some auxiliary lemmas that are needed for the proof of the Strong Exchange Theorem

[Johan Commelin]

@Óscar Álvarez Thanks! I left two minor comments.

[Óscar Álvarez]

@Johan Commelin Thanks, they should be fixed now

[Johan Commelin]

I left some more comments.

[Óscar Álvarez]

Just changed the style of the simps, let me know if I forgot any

[Mitchell Lee]

Hello, is it possible for this topic to be merged with this: #mathlib4 > Progress on Coxeter groups? Sorry; I know it is my fault that there are two topics.

[Johan Commelin]

Hmm, that would interleave the messages. I don't think we should do that.
Let's just attempt to continue the discussion in the other thread.