Hecke, Generalized Cartan, various Props on Coxeter Systems

.gitignore

@@ -1,2 +1,3 @@
 /.lake
-/docbuild/.lake
+/docbuild/.lake
+NilHecke.lean

Coxeter.lean

@@ -1,11 +1,20 @@
 module
 
 public import Coxeter.Basic
+public import Coxeter.BraidGroup
 public import Coxeter.Bruhat
+public import Coxeter.CartanMatrix
+public import Coxeter.Component
+public import Coxeter.Dihedral
 public import Coxeter.Data.List.Lemmas
+public import Coxeter.FiniteOrAffine.Affine
+public import Coxeter.FiniteOrAffine.Finite
 public import Coxeter.GeometricRepresentation
+public import Coxeter.Hecke
+public import Coxeter.LinearAlgebra.AssociatedGraded
 public import Coxeter.LinearAlgebra.BilinearForm
 public import Coxeter.LinearAlgebra.TwoDim
 public import Coxeter.Order.Directed
 public import Coxeter.PermutationRepresentation
+public import Coxeter.SpecialFeatures
 public import Coxeter.StrongExchange

Coxeter/Basic.lean

@@ -93,6 +93,22 @@ theorem alternatingWord_even_add (i i' : B W) (k m : ℕ) :
       rw [←concat_eq_append, ←alternatingWord_succ, alternatingWord_succ']
       simp
 
+theorem reverse_alternatingWord_of_odd (i i' : B W) (m : ℕ) (hm : Odd m) :
+  (alternatingWord i i' m).reverse = alternatingWord i i' m := by
+  apply List.ext_getElem (by simp [length_alternatingWord])
+  intro k h1 h2
+  have hkm : k < m := by simpa [length_alternatingWord] using h2
+  have hkm' : m - 1 - k < m := by omega
+  simp only [List.getElem_reverse, length_alternatingWord]
+  rw [getElem_alternatingWord i i' m k hkm, getElem_alternatingWord i i' m (m - 1 - k) hkm']
+  obtain ⟨j, hj⟩ := hm
+  have hpar : Even (m + (m - 1 - k)) ↔ Even (m + k) := by
+    rw [Nat.even_iff, Nat.even_iff]
+    omega
+  by_cases hE : Even (m + k)
+  · rw [if_pos hE, if_pos (hpar.mpr hE)]
+  · rw [if_neg hE, if_neg (fun hc => hE (hpar.mp hc))]
+
 theorem reverse_alternatingWord (i i' : B W) (k : ℕ) :
   (alternatingWord i i' (2 * k)).reverse = alternatingWord i' i (2 * k) := by
   induction k with
@@ -152,6 +168,37 @@ end ReducedWord
 
 end
 
+section BraidMoves
+
+/-! ### Braid moves and Matsumoto's theorem -/
+
+/-- An **elementary braid move**
+replacing a contiguous occurrence of the braid word
+`braidWord M i i'` (i.e. `s_i s_{i'} s_i ⋯`, `M i i'` letters)
+in a list by `braidWord M i' i`
+(`s_{i'} s_i s_{i'} ⋯`) leaving the rest of the list unchanged.
+Two lists related by `BraidMove` represent the same group element -/
+def BraidMove (ω ω' : List (B W)) : Prop :=
+  ∃ (i i' : B W) (α β : List (B W)),
+    ω = α ++ braidWord M i i' ++ β ∧ ω' = α ++ braidWord M i' i ++ β
+
+theorem BraidMove.wordProd_eq {ω ω' : List (B W)} (h : BraidMove ω ω') :
+    cs.wordProd ω = cs.wordProd ω' := by
+  obtain ⟨i, i', α, β, hω, hω'⟩ := h
+  rw [hω, hω']
+  simp only [wordProd_append, wordProd_braidWord_eq]
+
+class Matsumoto (W1 : Type*) [CoxeterGroup W1] : Prop where
+  /-- **Matsumoto's theorem**
+  (Tits' solution to the word problem for Coxeter groups)
+  Any two reduced words for the same element `w`
+  are connected by a finite chain of elementary braid moves. -/
+  reduced_words_convert : ∀ w : W1,
+    ∀ ω ω': ReducedWord w,
+    Relation.EqvGen (BraidMove (W:=W1)) ω.val ω'.val
+
+end BraidMoves
+
 section opposite
 
 /-! ### Opposite group -/

Coxeter/BraidGroup.lean

@@ -0,0 +1,130 @@
+module
+
+public import Coxeter.Basic
+public import Mathlib.GroupTheory.PresentedGroup
+
+/-!
+# The Artin (braid) group of a Coxeter system
+
+The Artin (braid) group is the group
+generated by the simple reflections of a Coxeter system
+quotiented by the braid relations, but *not* the quadratic relations `s_i^2 = 1`.
+
+The natural quotient map is `quot : BraidGroup W →* W`.
+
+Assuming `Matsumoto W` there is a well-defined lift
+`existsUnique_braidLift` of `w : W` back into `BraidGroup W`,
+via any reduced word for `w`.
+
+## Main definitions
+
+* `Coxeter.BraidGroup`, `Coxeter.quot`
+* `Coxeter.existsUnique_braidLift`
+-/
+
+@[expose] public section
+
+namespace Coxeter
+
+open List CoxeterSystem CoxeterGroup
+
+variable {W : Type*} [CoxeterGroup W]
+
+section ArtinBraid
+
+/-! ### The Artin (braid) group, and the lift `W → BraidGroup W` -/
+
+/-- The defining relations of the Artin (braid) group attached to a Coxeter system:
+for each pair of simple reflections `i i'`, the two braid words
+`s_i s_{i'} s_i ⋯` and `s_{i'} s_i s_{i'} ⋯` (`M i i'` letters each) become equal. -/
+def braidGroupRels (W : Type*) [CoxeterGroup W] : Set (FreeGroup (B W)) :=
+  {r | ∃ i i' : B W,
+    r = ((braidWord M i i').map FreeGroup.of).prod
+      * (((braidWord M i' i).map FreeGroup.of).prod)⁻¹}
+
+/-- The **Artin (braid) group** of a Coxeter system
+generators `B W`, modulo only the braid relations. -/
+abbrev BraidGroup (W : Type*) [CoxeterGroup W] : Type _ := PresentedGroup (braidGroupRels W)
+
+/-- The group homomorphism collapsing `BraidGroup W` back onto `W`
+sending each generator to the corresponding simple reflection. -/
+def quot {W : Type*} [CoxeterGroup W] : BraidGroup W →* W :=
+  PresentedGroup.toGroup (f := fun i => cs.simple i) (by
+    rintro r ⟨i, i', rfl⟩
+    simp only [map_mul, map_inv, mul_inv_eq_one]
+    rw [map_list_prod, map_list_prod, List.map_map, List.map_map]
+    have : ((braidWord M i i').map (FreeGroup.lift (fun i => cs.simple i) ∘ FreeGroup.of)).prod
+        = cs.wordProd (braidWord M i i') := by
+      congr 1
+      apply List.map_congr_left
+      intro j _
+      exact FreeGroup.lift_apply_of
+    rw [this]
+    have : ((braidWord M i' i).map (FreeGroup.lift (fun i => cs.simple i) ∘ FreeGroup.of)).prod
+        = cs.wordProd (braidWord M i' i) := by
+      congr 1
+      apply List.map_congr_left
+      intro j _
+      exact FreeGroup.lift_apply_of
+    rw [this]
+    exact cs.wordProd_braidWord_eq i i')
+
+end ArtinBraid
+
+section LiftQuot
+
+/-- The naive lift of a word to `BraidGroup W`, sending each letter to its generator. -/
+def braidLift {W : Type*} [CoxeterGroup W] (ω : List (B W)) : BraidGroup W :=
+  (ω.map (PresentedGroup.of (rels := braidGroupRels W))).prod
+
+private theorem braidLift_eq_mk {W : Type*} [CoxeterGroup W] (l : List (B W)) :
+    braidLift l = PresentedGroup.mk (braidGroupRels W) ((l.map FreeGroup.of).prod) := by
+  simp only [braidLift, map_list_prod, List.map_map]
+  rfl
+
+private theorem braidLift_append {W : Type*} [CoxeterGroup W] (l1 l2 : List (B W)) :
+    braidLift (W := W) (l1 ++ l2) = braidLift l1 * braidLift l2 := by
+  simp [braidLift, List.map_append, List.prod_append]
+
+private theorem quot_braidLift {W : Type*} [CoxeterGroup W] (ω : List (B W)) :
+    quot (braidLift ω) = cs.wordProd ω := by
+  unfold braidLift quot wordProd
+  rw [map_list_prod, List.map_map]
+  congr 1
+  apply List.map_congr_left
+  intro i _
+  exact PresentedGroup.toGroup.of _
+
+private theorem braidLift_of_braidMove {ω ω' : List (B W)} (h : BraidMove ω ω') :
+    braidLift ω = braidLift ω' := by
+  obtain ⟨i, i', α, β, hω, hω'⟩ := h
+  have hrel : ((braidWord M i i').map FreeGroup.of).prod
+      * (((braidWord M i' i).map FreeGroup.of).prod)⁻¹ ∈ braidGroupRels W := ⟨i, i', rfl⟩
+  have hmid : braidLift (braidWord M i i') = braidLift (braidWord M i' i) := by
+    rw [braidLift_eq_mk, braidLift_eq_mk]
+    exact PresentedGroup.mk_eq_mk_of_mul_inv_mem hrel
+  rw [hω, hω', braidLift_append, braidLift_append, braidLift_append, braidLift_append, hmid]
+
+private theorem braidLift_of_eqvGen {ω ω' : List (B W)} (h : Relation.EqvGen BraidMove ω ω') :
+    braidLift ω = braidLift ω' := by
+  induction h with
+  | rel a b hab => exact braidLift_of_braidMove hab
+  | refl => rfl
+  | symm _ _ _ ih => exact ih.symm
+  | trans _ _ _ _ _ ih1 ih2 => exact ih1.trans ih2
+
+/-- **The set of candidate values is a singleton**
+The image of a reduced word for `w` under
+`braidLift` doesn't depend on which reduced word was chosen. -/
+theorem existsUnique_braidLift [Matsumoto W] (w : W) :
+    ∃! x : BraidGroup W,
+      ∃ ω : ReducedWord w, x = braidLift ω.val ∧ quot x = w
+  := by
+  obtain ⟨ω⟩ : Nonempty (ReducedWord w) := inferInstance
+  refine ⟨braidLift ω.val, ⟨ω, rfl, by rw [quot_braidLift, ω.wordProd_eq]⟩, ?_⟩
+  rintro x ⟨ω', rfl, -⟩
+  exact braidLift_of_eqvGen (Matsumoto.reduced_words_convert w ω' ω)
+
+end LiftQuot
+
+end Coxeter

Coxeter/Bruhat.lean

@@ -314,6 +314,14 @@ theorem finite_Icc (u w : W) : Finite (Set.Icc u w) := by
 
 noncomputable instance : LocallyFiniteOrder W := LocallyFiniteOrder.ofFiniteIcc finite_Icc
 
+/-- Bruhat intervals are finite. -/
+lemma bruhat_interval_finite (u w : W) : {v : W | u ≤ v ∧ v ≤ w}.Finite := by
+  exact Set.Finite.ofFinset (Finset.Icc u w) (by simp)
+
+/-- Principal lower Bruhat intervals are finite. -/
+lemma bruhat_le_setOf_finite (w : W) : {u : W | u ≤ w}.Finite := by
+  exact Set.Finite.ofFinset (Finset.Icc (⊥ : W) w) (by simp)
+
 /-- Bjorner--Brenti Corollary 2.2.4 -/
 theorem card_Icc_le (u w : W) : (Finset.Icc u w).card ≤ 2 ^ cs.length w := by
   classical
@@ -370,6 +378,33 @@ theorem covBy_iff {u w : W} : u ⋖ w ↔ u ≤ w ∧ cs.length u + 1 = cs.lengt
     show grade ℕ = cs.length by rfl]
   grind
 
+theorem le_mul_of_isReflection_of_length_lt {u t : W} (ht : cs.IsReflection t)
+  (hlt : cs.length u < cs.length (u * t)) : u ≤ u * t :=
+  le.step u u (u * t) (le.rfl _) (by simpa [mul_assoc] using ht.conj u) hlt
+
+theorem covBy_iff_exists_reflection {u w : W} :
+    u ⋖ w ↔ ∃ t : W, cs.IsReflection t ∧ w = u * t ∧ cs.length u + 1 = cs.length w := by
+  constructor
+  · intro h
+    have hlen := length_cover h
+    have hle := h.1.1
+    induction hle with
+    | rfl =>
+        exact (h.ne rfl).elim
+    | step v w huv href hlt ih =>
+        have huv_eq : u = v := by
+          apply eq_of_le_of_length_eq huv
+          have huv_len := length_le_of_le huv
+          have : cs.length v < cs.length u + 1 := by
+            rwa [←hlen] at hlt
+          omega
+        subst v
+        refine ⟨u⁻¹ * w, ?_, by simp, hlen⟩
+        simpa [mul_assoc] using href.conj u⁻¹
+  · rintro ⟨t, ht, rfl, hlen⟩
+    rw [covBy_iff]
+    exact ⟨le_mul_of_isReflection_of_length_lt ht (by omega), hlen⟩
+
 theorem simple_mul_covBy_self_iff (i : B W) (w : W) :
   cs.simple i * w ⋖ w ↔ cs.IsLeftDescent w i := by
   rw [covBy_iff, ←cs.isLeftDescent_iff, ←simple_mul_lt_self_iff, and_iff_right_iff_imp]
@@ -498,6 +533,25 @@ instance : IsDirectedOrder W where
         rw [simple_mul_simple_cancel_left] at h4
         exact ⟨h4, hx2.trans h3⟩
 
+lemma simple_upper (i : B W) (w : W) :
+  w <= cs.simple i ↔ (w = 1 ∨ w = cs.simple i) := by
+  constructor
+  · intro h
+    by_cases hw : w = 1
+    · exact Or.inl hw
+    · right
+      apply eq_of_le_of_length_eq h
+      have hle := length_le_of_le h
+      rw [cs.length_simple] at hle ⊢
+      have ⟨j, hj⟩ := cs.exists_leftDescent_of_ne_one hw
+      have hlt : cs.length (cs.simple j * w) < cs.length w :=
+        strictMono_length ((simple_mul_lt_self_iff j w).mpr hj)
+      have hpos : 0 < cs.length w := by omega
+      omega
+  · rintro (rfl | rfl)
+    · exact bot_le
+    · exact le_rfl
+
 section finite
 
 /-! ### Bruhat order on finite Coxeter groups -/