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

@[simp]

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

@[simp]

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

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.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)

@[simp]

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

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

Reduced words

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 }

instance Coxeter.instNonemptyReducedWord {W : Type u_1} [CoxeterGroup W] {w : W} : Nonempty (ReducedWord w)

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

Opposite group

def Coxeter.cs_op {W : Type u_1} [CoxeterGroup W] : CoxeterSystem CoxeterGroup.M Wᵐᵒᵖ

Equations

• Coxeter.cs_op = { mulEquiv := (MulEquiv.inv' W).symm.trans Coxeter.CoxeterGroup.cs.mulEquiv }

@[implicit_reducible]

instance Coxeter.instCoxeterGroupMulOpposite {W : Type u_1} [CoxeterGroup W] : CoxeterGroup Wᵐᵒᵖ

Equations

• Coxeter.instCoxeterGroupMulOpposite = { toGroup := MulOpposite.instGroup, B := Coxeter.CoxeterGroup.B W, M := Coxeter.CoxeterGroup.M, cs := Coxeter.cs_op }

theorem Coxeter.simple_op {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) : CoxeterGroup.cs.simple i = MulOpposite.op (CoxeterGroup.cs.simple i)

theorem Coxeter.wordProd_op {W : Type u_1} [CoxeterGroup W] (ω : List (CoxeterGroup.B W)) : CoxeterGroup.cs.wordProd ω = MulOpposite.op (CoxeterGroup.cs.wordProd ω.reverse)

theorem Coxeter.length_op {W : Type u_1} [CoxeterGroup W] (w : W) : CoxeterGroup.cs.length (MulOpposite.op w) = CoxeterGroup.cs.length w

theorem Coxeter.isLeftDescent_op_iff {W : Type u_1} [CoxeterGroup W] (w : W) (i : CoxeterGroup.B W) : CoxeterGroup.cs.IsLeftDescent (MulOpposite.op w) i ↔ CoxeterGroup.cs.IsRightDescent w i

theorem Coxeter.isReflection_op_iff {W : Type u_1} [CoxeterGroup W] (t : W) : CoxeterGroup.cs.IsReflection (MulOpposite.op t) ↔ CoxeterGroup.cs.IsReflection t

theorem Coxeter.isLeftInversion_op_iff {W : Type u_1} [CoxeterGroup W] (w t : W) : CoxeterGroup.cs.IsLeftInversion (MulOpposite.op w) (MulOpposite.op t) ↔ CoxeterGroup.cs.IsRightInversion w t

theorem Coxeter.leftInvSeq_op {W : Type u_1} [CoxeterGroup W] (ω : List (CoxeterGroup.B W)) : CoxeterGroup.cs.leftInvSeq ω = List.map MulOpposite.op (CoxeterGroup.cs.leftInvSeq ω)