Coxeter groups

We build upon the the theory of Coxeter systems currently available in mathlib.

Main definitions

• Coxeter.CoxeterGroup
• Coxeter.ReducedWord

class Coxeter.CoxeterGroup (W : Type u_1) extends Group W : Type (max u_1 (u_2 + 1))

• mul : W → W → W
• mul_assoc (a b c : W) : a * b * c = a * (b * c)
• one : W
• one_mul (a : W) : 1 * a = a
• mul_one (a : W) : a * 1 = a
• npow : ℕ → W → W
• npow_zero (x : W) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : W) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• inv : W → W
• div : W → W → W
• div_eq_mul_inv (a b : W) : a / b = a * b⁻¹
• zpow : ℤ → W → W
• zpow_zero' (a : W) : DivInvMonoid.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : W) : DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : W) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• inv_mul_cancel (a : W) : a⁻¹ * a = 1
• B : Type u_2
• M : CoxeterMatrix (B W)
• cs : CoxeterSystem M W

theorem List.drop_eraseIdx {α : Type u_1} (l : List α) (i j : ℕ) : (drop i l).eraseIdx j = drop i (l.eraseIdx (i + j))

theorem List.reverse_eraseIdx {α : Type u_1} {l : List α} {i : ℕ} (hi : i < l.length) : l.reverse.eraseIdx i = (l.eraseIdx (l.length - i - 1)).reverse

def Coxeter.ReducedWord {W : Type u_1} [CoxeterGroup W] (w : W) : Type u_2

Equations

• Coxeter.ReducedWord w = { ω : List (Coxeter.CoxeterGroup.B W) // Coxeter.CoxeterGroup.cs.IsReduced ω ∧ w = Coxeter.CoxeterGroup.cs.wordProd ω }

@[implicit_reducible]

instance Coxeter.instCoeOutReducedWordListB {W : Type u_1} [CoxeterGroup W] {w : W} : CoeOut (ReducedWord w) (List (CoxeterGroup.B W))

Equations

• Coxeter.instCoeOutReducedWordListB = { coe := Subtype.val }

@[implicit_reducible]

noncomputable instance Coxeter.instInhabitedReducedWord {W : Type u_1} [CoxeterGroup W] {w : W} : Inhabited (ReducedWord w)

Equations

• Coxeter.instInhabitedReducedWord = { default := ⟨Classical.choose ⋯, ⋯⟩ }

def Coxeter.ReducedWord.reverse {W : Type u_1} [CoxeterGroup W] {w : W} (ω : ReducedWord w) : ReducedWord w⁻¹

Equations

• ω.reverse = ⟨(↑ω).reverse, ⋯⟩

theorem Coxeter.ReducedWord.length_eq {W : Type u_1} [CoxeterGroup W] {w : W} (ω : ReducedWord w) : (↑ω).length = CoxeterGroup.cs.length w

theorem Coxeter.ReducedWord.wordProd_eq {W : Type u_1} [CoxeterGroup W] {w : W} (ω : ReducedWord w) : CoxeterGroup.cs.wordProd ↑ω = w

theorem Coxeter.IsReduced_nil {W : Type u_1} [CoxeterGroup W] : CoxeterGroup.cs.IsReduced []

theorem Coxeter.IsReduced_cons {W : Type u_1} [CoxeterGroup W] {ω : List (CoxeterGroup.B W)} (hω : CoxeterGroup.cs.IsReduced ω) (i : CoxeterGroup.B W) : CoxeterGroup.cs.IsReduced (i :: ω) ↔ ¬CoxeterGroup.cs.IsLeftDescent (CoxeterGroup.cs.wordProd ω) i

theorem Coxeter.not_IsReduced_cons {W : Type u_1} [CoxeterGroup W] {ω : List (CoxeterGroup.B W)} (hω : CoxeterGroup.cs.IsReduced ω) (i : CoxeterGroup.B W) : ¬CoxeterGroup.cs.IsReduced (i :: ω) ↔ CoxeterGroup.cs.IsLeftDescent (CoxeterGroup.cs.wordProd ω) i

theorem Coxeter.isReduced_of_append_left {W : Type u_1} [CoxeterGroup W] {μ ω : List (CoxeterGroup.B W)} (h : CoxeterGroup.cs.IsReduced (μ ++ ω)) : CoxeterGroup.cs.IsReduced μ

theorem Coxeter.isReduced_of_append_right {W : Type u_1} [CoxeterGroup W] {μ ω : List (CoxeterGroup.B W)} (h : CoxeterGroup.cs.IsReduced (μ ++ ω)) : CoxeterGroup.cs.IsReduced ω

theorem Coxeter.tail_leftInvSeq {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) (ω : List (CoxeterGroup.B W)) : (CoxeterGroup.cs.leftInvSeq (i :: ω)).tail = List.map (⇑(MulAut.conj (CoxeterGroup.cs.simple i))) (CoxeterGroup.cs.leftInvSeq ω)

theorem Coxeter.drop_leftInvSeq {W : Type u_1} [CoxeterGroup W] (j : ℕ) (ω : List (CoxeterGroup.B W)) : List.drop j (CoxeterGroup.cs.leftInvSeq ω) = List.map (⇑(MulAut.conj (CoxeterGroup.cs.wordProd (List.take j ω)))) (CoxeterGroup.cs.leftInvSeq (List.drop j ω))

theorem Coxeter.leftInvSeq_append {W : Type u_1} [CoxeterGroup W] (μ ω : List (CoxeterGroup.B W)) : CoxeterGroup.cs.leftInvSeq (μ ++ ω) = CoxeterGroup.cs.leftInvSeq μ ++ List.map (⇑(MulAut.conj (CoxeterGroup.cs.wordProd μ))) (CoxeterGroup.cs.leftInvSeq ω)

theorem Coxeter.tail_alternatingWord {W : Type u_1} [CoxeterGroup W] (i j : CoxeterGroup.B W) (p : ℕ) : (CoxeterSystem.alternatingWord i j (p + 1)).tail = CoxeterSystem.alternatingWord i j p

theorem Coxeter.drop_alternatingWord {W : Type u_1} [CoxeterGroup W] (i j : CoxeterGroup.B W) (p q : ℕ) : List.drop p (CoxeterSystem.alternatingWord i j (p + q)) = CoxeterSystem.alternatingWord i j q

theorem Coxeter.alternatingWord_even_add {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) (k m : ℕ) : CoxeterSystem.alternatingWord i i' (2 * k + m) = CoxeterSystem.alternatingWord i i' m ++ CoxeterSystem.alternatingWord i i' (2 * k)

theorem Coxeter.reverse_alternatingWord {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) (k : ℕ) : (CoxeterSystem.alternatingWord i i' (2 * k)).reverse = CoxeterSystem.alternatingWord i' i (2 * k)

theorem Coxeter.getD_leftInvSeq_mul_wordProd₂ {W : Type u_1} [CoxeterGroup W] {i j : ℕ} (ω : List (CoxeterGroup.B W)) (hij : i < j) : (CoxeterGroup.cs.leftInvSeq ω).getD i 1 * (CoxeterGroup.cs.leftInvSeq ω).getD j 1 * CoxeterGroup.cs.wordProd ω = CoxeterGroup.cs.wordProd ((ω.eraseIdx j).eraseIdx i)

theorem Coxeter.getElem_leftInvSeq_mul_wordProd₂ {W : Type u_1} [CoxeterGroup W] {i j : ℕ} (ω : List (CoxeterGroup.B W)) (h1 : i < j) (h2 : j < ω.length) : (CoxeterGroup.cs.leftInvSeq ω)[i] * (CoxeterGroup.cs.leftInvSeq ω)[j] * CoxeterGroup.cs.wordProd ω = CoxeterGroup.cs.wordProd ((ω.eraseIdx j).eraseIdx i)

theorem Coxeter.adjacent_ne_of_isReduced {W : Type u_1} [CoxeterGroup W] {i : ℕ} {ω : List (CoxeterGroup.B W)} (hi : i + 1 < ω.length) (hω : CoxeterGroup.cs.IsReduced ω) : ω[i] ≠ ω[i + 1]

@[simp]

theorem Coxeter.simple_ne_one {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) : CoxeterGroup.cs.simple i ≠ 1

@[simp]

theorem Coxeter.isReduced_of_singleton {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) : CoxeterGroup.cs.IsReduced [i]

theorem Coxeter.not_isLeftInversion_one {W : Type u_1} [CoxeterGroup W] (t : W) : ¬CoxeterGroup.cs.IsLeftInversion 1 t

theorem Coxeter.not_isRightInversion_one {W : Type u_1} [CoxeterGroup W] (t : W) : ¬CoxeterGroup.cs.IsRightInversion 1 t