leanprover-community
diff --git a/‎Mathlib/GroupTheory/Coxeter/Basic.lean
Lines changed: 104 additions & 152 deletions b/‎Mathlib/GroupTheory/Coxeter/Basic.lean
Lines changed: 104 additions & 152 deletions
@@ -1,51 +1,45 @@
 /-
 Copyright (c) 2024 Newell Jensen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Newell Jensen
+Authors: Newell Jensen, Mitchell Lee
 -/
-import Mathlib.GroupTheory.Coxeter.Matrix
 import Mathlib.GroupTheory.PresentedGroup
+import Mathlib.GroupTheory.Coxeter.Matrix
 
 /-!
-# 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:
+# Coxeter groups and Coxeter systems
 
-* `Aₙ, Bₙ, Dₙ, I₂ₘ`
+This file defines Coxeter groups and Coxeter systems.
 
-And the exceptional systems:
+Let `B` be a (possibly infinite) type, and let $M = (M_{i,i'})_{i, i' \in B}$ be a matrix
+of natural numbers. Further assume that $M$ is a *Coxeter matrix* (`CoxeterMatrix`); that is, $M$ is
+symmetric and $M_{i,i'} = 1$ if and only if $i = i'$. The *Coxeter group* associated to $M$
+(`CoxeterMatrix.group`) has the presentation
+$$\langle \{s_i\}_{i \in B} \vert \{(s_i s_{i'})^{M_{i, i'}}\}_{i, i' \in B} \rangle.$$
+The elements $s_i$ are called the *simple reflections* (`CoxeterMatrix.simple`) of the Coxeter
+group. Note that every simple reflection is an involution.
 
-* `E₆, E₇, E₈, F₄, G₂, H₃, H₄`
+A *Coxeter system* (`CoxeterSystem`) is a group $W$, together with an isomorphism between $W$ and
+the Coxeter group associated to some Coxeter matrix $M$. By abuse of language, we also say that $W$
+is a Coxeter group (`IsCoxeterGroup`), and we may speak of the simple reflections $s_i \in W$
+(`CoxeterSystem.simple`). We state all of our results about Coxeter groups in terms of Coxeter
+systems where possible.
 
 ## 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.
+Much of the literature on Coxeter groups conflates the set $S = \{s_i : i \in B\} \subseteq W$ of
+simple reflections with the set $B$ that indexes the simple reflections. This is usually permissible
+because the simple reflections $s_i$ of any Coxeter group are all distinct (a nontrivial fact that
+we do not prove in this file). In contrast, we try not to refer to the set $S$ of simple
+reflections unless necessary; instead, we state our results in terms of $B$ wherever possible.
 
 ## Main definitions
 
-* `Matrix.CoxeterGroup` : The group presentation corresponding to a Coxeter matrix.
-* `CoxeterSystem` : A structure recording the isomorphism between a group `W` and the
-  group presentation corresponding to a Coxeter matrix, i.e. `Matrix.CoxeterGroup M`.
-* `equivCoxeterGroup` : Coxeter groups of isomorphic types are isomorphic.
-* `IsCoxeterGroup` : A group is a Coxeter group if it is registered in a Coxeter system.
+* `CoxeterMatrix.group`
+* `CoxeterSystem`
+* `IsCoxeterGroup`
+* `CoxeterSystem.simple` : If `cs` is a Coxeter system on the group `W`, then `cs.simple i` is the
+  simple reflection of `W` at the index `i`.
 
 ## References
 
@@ -56,162 +50,120 @@ presentation corresponding to a Coxeter matrix which is registered in a Coxeter
 
 ## 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`.
+* The simple reflections of a Coxeter system are distinct.
 
 ## Tags
 
 coxeter system, coxeter group
+
 -/
 
+open Function
 
-universe u
+/-! ### Coxeter groups -/
 
-noncomputable section
+namespace CoxeterMatrix
 
-variable {B : Type*} [DecidableEq B]
-variable (M : Matrix B B ℕ)
+variable {B B' : Type*} (M : CoxeterMatrix B) (e : B ≃ B')
 
-namespace CoxeterGroup
+/-- The Coxeter relation associated to a Coxeter matrix $M$ and two indices $i, i' \in B$.
+That is, the relation $(s_i s_{i'})^{M_{i, i'}}$, considered as an element of the free group
+on $\{s_i\}_{i \in B}$.
+If $M_{i, i'} = 0$, then this is the identity, indicating that there is no relation between
+$s_i$ and $s_{i'}$. -/
+def relation (i i' : B) : FreeGroup B := (FreeGroup.of i * FreeGroup.of i') ^ M i i'
 
-namespace Relations
+/-- The set of all Coxeter relations associated to the Coxeter matrix $M$. -/
+def relationsSet : Set (FreeGroup B) := Set.range <| uncurry M.relation
 
-/-- The relations corresponding to a Coxeter matrix. -/
-def ofMatrix : B × B → FreeGroup B :=
-  Function.uncurry fun b₁ b₂ => (FreeGroup.of b₁ * FreeGroup.of b₂) ^ M b₁ b₂
+/-- The Coxeter group associated to a Coxeter matrix $M$; that is, the group
+$$\langle \{s_i\}_{i \in B} \vert \{(s_i s_{i'})^{M_{i, i'}}\}_{i, i' \in B} \rangle.$$ -/
+protected def Group : Type _ := PresentedGroup M.relationsSet
 
-/-- The set of relations corresponding to a Coxeter matrix. -/
-def toSet : Set (FreeGroup B) :=
-  Set.range <| ofMatrix M
+instance : Group M.Group := QuotientGroup.Quotient.group _
 
-end Relations
+/-- The simple reflection of the Coxeter group `M.group` at the index `i`. -/
+def simple (i : B) : M.Group := PresentedGroup.of i
 
-end CoxeterGroup
+theorem reindex_relationsSet :
+    (M.reindex e).relationsSet =
+    FreeGroup.freeGroupCongr e '' M.relationsSet := let M' := M.reindex e; calc
+  Set.range (uncurry M'.relation)
+  _ = Set.range (uncurry M'.relation ∘ Prod.map e e) := by simp [Set.range_comp]
+  _ = Set.range (FreeGroup.freeGroupCongr e ∘ uncurry M.relation) := by
+      apply congrArg Set.range
+      ext ⟨i, i'⟩
+      simp [relation, reindex_apply, M']
+  _ = _ := by simp [Set.range_comp]; rfl
 
-/-- The group presentation corresponding to a Coxeter matrix. -/
-def Matrix.CoxeterGroup := PresentedGroup <| CoxeterGroup.Relations.toSet M
+/-- The isomorphism between the Coxeter group associated to the reindexed matrix `M.reindex e` and
+the Coxeter group associated to `M`. -/
+def reindexGroupEquiv : (M.reindex e).Group ≃* M.Group :=
+  (QuotientGroup.congr (Subgroup.normalClosure M.relationsSet)
+    (Subgroup.normalClosure (M.reindex e).relationsSet)
+    (FreeGroup.freeGroupCongr e) (by
+      rw [reindex_relationsSet,
+        Subgroup.map_normalClosure _ _ (FreeGroup.freeGroupCongr e).surjective,
+        ← MulEquiv.coe_toMonoidHom]
+      rfl)).symm
 
-instance : Group (Matrix.CoxeterGroup M) :=
-  QuotientGroup.Quotient.group _
+theorem reindexGroupEquiv_apply_simple (i : B') :
+    (M.reindexGroupEquiv e) ((M.reindex e).simple i) = M.simple (e.symm i) := rfl
 
-namespace CoxeterGroup
+theorem reindexGroupEquiv_symm_apply_simple (i : B) :
+    (M.reindexGroupEquiv e).symm (M.simple i) = (M.reindex e).simple (e i) := rfl
 
-/-- 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`. -/
-def of (b : B) : Matrix.CoxeterGroup M := PresentedGroup.of b
+end CoxeterMatrix
 
-@[simp]
-theorem of_apply (b : B) : of M b = PresentedGroup.of (rels := Relations.toSet M) b :=
-  rfl
-
-end CoxeterGroup
-
-/-- 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`. -/
-structure CoxeterSystem (W : Type*) [Group W]  where
-  /-- `CoxeterSystem.ofMulEquiv` constructs a Coxeter system given an equivalence with the group
-  presentation corresponding to a Coxeter matrix `M`. -/
-  ofMulEquiv ::
-    /-- `mulEquiv` is the isomorphism between the group `W` and the group presentation
-    corresponding to a Coxeter matrix `M`. -/
-    mulEquiv : W ≃* Matrix.CoxeterGroup M
+/-! ### Coxeter systems -/
 
-/-- A group is a Coxeter group if it admits a Coxeter system for some Coxeter matrix `M`. -/
-class IsCoxeterGroup (W : Type u) [Group W] : Prop where
-  nonempty_system : ∃ B : Type u, ∃ M : Matrix B B ℕ, M.IsCoxeter ∧ Nonempty (CoxeterSystem M W)
+section
 
-namespace CoxeterSystem
+variable {B : Type*} (M : CoxeterMatrix B)
 
-open Matrix
+/-- A Coxeter system `CoxeterSystem M W` is a structure recording the isomorphism between
+a group `W` and the Coxeter group associated to a Coxeter matrix `M`. -/
+@[ext]
+structure CoxeterSystem (W : Type*) [Group W] where
+  /-- The isomorphism between `W` and the Coxeter group associated to `M`. -/
+  mulEquiv : W ≃* M.Group
 
-variable {B B' W H : Type*} [Group W] [Group H]
-variable {M : Matrix B B ℕ}
+/-- A group is a Coxeter group if it admits a Coxeter system for some Coxeter matrix `M`. -/
+class IsCoxeterGroup.{u} (W : Type u) [Group W] : Prop where
+  nonempty_system : ∃ B : Type u, ∃ M : CoxeterMatrix B, Nonempty (CoxeterSystem M 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. -/
-instance funLike : FunLike (CoxeterSystem M W) B W where
-  coe cs := fun b => cs.mulEquiv.symm (.of b)
-  coe_injective' := by
-    rintro ⟨cs⟩ ⟨cs'⟩ hcs'
-    have H : (cs.symm : CoxeterGroup M →* W) = (cs'.symm : CoxeterGroup M →* W) := by
-      unfold CoxeterGroup
-      ext i; exact congr_fun hcs' i
-    have : cs.symm = cs'.symm := by ext x; exact DFunLike.congr_fun H x
-    rw [ofMulEquiv.injEq, ← MulEquiv.symm_symm cs, ← MulEquiv.symm_symm cs', this]
+/-- The canonical Coxeter system on the Coxeter group associated to `M`. -/
+def CoxeterMatrix.toCoxeterSystem : CoxeterSystem M M.Group := ⟨.refl _⟩
 
-@[simp]
-theorem mulEquiv_apply_coe (cs : CoxeterSystem M W) (b : B) : cs.mulEquiv (cs b) = .of b :=
-  cs.mulEquiv.eq_symm_apply.mp rfl
+end
 
-/-- The map sending a Coxeter system to its associated map `B → W` is injective. -/
-theorem ext' {cs₁ cs₂ : CoxeterSystem M W} (H : ⇑cs₁ = ⇑cs₂) : cs₁ = cs₂ := DFunLike.coe_injective H
+namespace CoxeterSystem
 
-/-- Extensionality rule for Coxeter systems. -/
-theorem ext {cs₁ cs₂ : CoxeterSystem M W} (H : ∀ b, cs₁ b = cs₂ b) : cs₁ = cs₂ :=
-  ext' <| by ext; apply H
+open CoxeterMatrix
 
-/-- The canonical Coxeter system of the Coxeter group over `X`. -/
-def ofCoxeterGroup (X : Type*) (D : Matrix X X ℕ) : CoxeterSystem D (CoxeterGroup D) where
-  mulEquiv := .refl _
+variable {B B' : Type*} (e : B ≃ B')
+variable {W H : Type*} [Group W] [Group H]
+variable {M : CoxeterMatrix B} (cs : CoxeterSystem M W)
 
-@[simp]
-theorem ofCoxeterGroup_apply {X : Type*} (D : Matrix X X ℕ) (x : X) :
-    CoxeterSystem.ofCoxeterGroup X D x = CoxeterGroup.of D x :=
-  rfl
-
-theorem map_relations_eq_reindex_relations (e : B ≃ B') :
-    (MulEquiv.toMonoidHom (FreeGroup.freeGroupCongr e)) '' CoxeterGroup.Relations.toSet M =
-    CoxeterGroup.Relations.toSet (reindex e e M) := by
-  simp only [MulEquiv.coe_toMonoidHom, FreeGroup.freeGroupCongr_apply, CoxeterGroup.Relations.toSet,
-    CoxeterGroup.Relations.ofMatrix, reindex_apply, submatrix_apply]
-  ext x
-  simp only [Set.mem_image, Set.mem_range, Prod.exists, Function.uncurry_apply_pair]
-  constructor
-  · rintro ⟨x, ⟨a, b, rfl⟩, rfl⟩
-    use e a, e b
-    simp
-  · rintro ⟨a, b, h⟩
-    refine ⟨(FreeGroup.freeGroupCongr e).symm x, ⟨e.symm a, e.symm b, ?_⟩, ?_⟩ <;> aesop
-
-/-- Coxeter groups of isomorphic types are isomorphic. -/
-def equivCoxeterGroup (e : B ≃ B') : CoxeterGroup M ≃* CoxeterGroup (reindex e e M) :=
-  QuotientGroup.congr (Subgroup.normalClosure (CoxeterGroup.Relations.toSet M))
-    (Subgroup.normalClosure (CoxeterGroup.Relations.toSet (reindex e e M)))
-    (FreeGroup.freeGroupCongr e) (by
-      have := Subgroup.map_normalClosure (CoxeterGroup.Relations.toSet M)
-        (FreeGroup.freeGroupCongr e).toMonoidHom (FreeGroup.freeGroupCongr e).surjective
-      rwa [map_relations_eq_reindex_relations] at this)
+/-- Reindex a Coxeter system through a bijection of the indexing sets. -/
+@[simps]
+protected def reindex (e : B ≃ B') : CoxeterSystem (M.reindex e) W :=
+  ⟨cs.mulEquiv.trans (M.reindexGroupEquiv e).symm⟩
 
-theorem equivCoxeterGroup_apply_of (b : B) (M : Matrix B B ℕ) (e : B ≃ B') :
-    (equivCoxeterGroup e) (CoxeterGroup.of M b) = CoxeterGroup.of (reindex e e M) (e b) :=
-  rfl
+/-- Push a Coxeter system through a group isomorphism. -/
+@[simps] protected def map (e : W ≃* H) : CoxeterSystem M H := ⟨e.symm.trans cs.mulEquiv⟩
 
-theorem equivCoxeterGroup_symm_apply_of (b' : B') (M : Matrix B B ℕ) (e : B ≃ B') :
-    (equivCoxeterGroup e).symm (CoxeterGroup.of (reindex e e M) b') =
-    CoxeterGroup.of M (e.symm b') :=
-  rfl
+/-! ### Simple reflections -/
 
-/-- Reindex a Coxeter system through a bijection of the indexing sets. -/
-@[simps]
-protected def reindex (cs : CoxeterSystem M W) (e : B ≃ B') :
-    CoxeterSystem (reindex e e M) W :=
-  ofMulEquiv (cs.mulEquiv.trans (equivCoxeterGroup e))
+/-- The simple reflection of `W` at the index `i`. -/
+def simple (i : B) : W := cs.mulEquiv.symm (PresentedGroup.of i)
 
 @[simp]
-theorem reindex_apply (cs : CoxeterSystem M W) (e : B ≃ B') (b' : B') :
-    cs.reindex e b' = cs (e.symm b') :=
-  rfl
+theorem _root_.CoxeterMatrix.toCoxeterSystem_simple (M : CoxeterMatrix B) :
+    M.toCoxeterSystem.simple = M.simple := rfl
 
-/-- Pushing a Coxeter system through a group isomorphism. -/
-@[simps]
-protected def map (cs : CoxeterSystem M W) (e : W ≃* H) : CoxeterSystem M H :=
-  ofMulEquiv (e.symm.trans cs.mulEquiv)
+@[simp] theorem reindex_simple (i' : B') : (cs.reindex e).simple i' = cs.simple (e.symm i') := rfl
 
-@[simp]
-theorem map_apply (cs : CoxeterSystem M W) (e : W ≃* H) (b : B) : cs.map e b = e (cs b) :=
-  rfl
+@[simp] theorem map_simple (e : W ≃* H) (i : B) : (cs.map e).simple i = e (cs.simple i) := rfl
 
 end CoxeterSystem