Permutation representation of Coxeter groups

This file defines the permutation representation of a Coxeter group.

Main definitions

• Coxeter.ReflectionSet
• Coxeter.RootSet
• Coxeter.permRep
• Coxeter.η

Main statements

• Coxeter.eta_spec
• Coxeter.permRep_eq
• Coxeter.permRep_inj

References

• [BB05] A. Björner and F. Brenti, Combinatorics of Coxeter Groups

def Coxeter.ReflectionSet (W : Type u_1) [CoxeterGroup W] : Type u_1

Equations

• Coxeter.ReflectionSet W = { t : W // Coxeter.CoxeterGroup.cs.IsReflection t }

def Coxeter.RootSet (W : Type u_1) [CoxeterGroup W] : Type u_1

Equations

• Coxeter.RootSet W = (Coxeter.ReflectionSet W × ZMod 2)

theorem Coxeter.ReflectionSet.induction {W : Type u_1} [CoxeterGroup W] {P : ReflectionSet W → Prop} (sh : ∀ (i : CoxeterGroup.B W), P ⟨CoxeterGroup.cs.simple i, ⋯⟩) (ih : ∀ (t : ReflectionSet W) (i : CoxeterGroup.B W), P t → P ⟨CoxeterGroup.cs.simple i * ↑t * (CoxeterGroup.cs.simple i)⁻¹, ⋯⟩) (t : ReflectionSet W) : P t

Induction principle for reflections

noncomputable def Coxeter.etaAux {W : Type u_1} [CoxeterGroup W] (ω : List (CoxeterGroup.B W)) (t : W) : ZMod 2

Equations

• Coxeter.etaAux ω t = ↑(List.count t (Coxeter.CoxeterGroup.cs.leftInvSeq ω))

theorem Coxeter.etaAux_append {W : Type u_1} [CoxeterGroup W] (μ ω : List (CoxeterGroup.B W)) (t : W) : etaAux (μ ++ ω) t = etaAux μ t + etaAux ω ((CoxeterGroup.cs.wordProd μ)⁻¹ * t * CoxeterGroup.cs.wordProd μ)

noncomputable def Coxeter.permRepAux {W : Type u_1} [CoxeterGroup W] (ω : List (CoxeterGroup.B W)) (r : RootSet W) : RootSet W

Equations

• Coxeter.permRepAux ω r = (⟨(MulAut.conj (Coxeter.CoxeterGroup.cs.wordProd ω)) ↑r.1, ⋯⟩, r.2 + Coxeter.etaAux ω.reverse ↑r.1)

theorem Coxeter.permRepAux_nil {W : Type u_1} [CoxeterGroup W] : permRepAux [] = id

theorem Coxeter.permRepAux_cons {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) (ω : List (CoxeterGroup.B W)) : permRepAux (i :: ω) = permRepAux [i] ∘ permRepAux ω

theorem Coxeter.permRepAux_append {W : Type u_1} [CoxeterGroup W] (ω₁ ω₂ : List (CoxeterGroup.B W)) : permRepAux (ω₁ ++ ω₂) = permRepAux ω₁ ∘ permRepAux ω₂

theorem Coxeter.permRepAux_alternatingWord {W : Type u_1} [CoxeterGroup W] (i i' : CoxeterGroup.B W) : permRepAux (CoxeterSystem.alternatingWord i i' (2 * CoxeterGroup.M.M i i')) = id

theorem Coxeter.permRepAux_singleton_involutive {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) : Function.Involutive (permRepAux [i])

noncomputable def Coxeter.permRepAux_equiv {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) : Equiv.Perm (RootSet W)

Equations

• Coxeter.permRepAux_equiv i = { toFun := Coxeter.permRepAux [i], invFun := Coxeter.permRepAux [i], left_inv := ⋯, right_inv := ⋯ }

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

theorem Coxeter.permRepAux_liftable {W : Type u_1} [CoxeterGroup W] : CoxeterGroup.M.IsLiftable permRepAux_equiv

noncomputable def Coxeter.permRep {W : Type u_1} [CoxeterGroup W] : W →* Equiv.Perm (RootSet W)

Bjorner--Brenti Theorem 1.3.2 (i): extension

Equations

• Coxeter.permRep = Coxeter.CoxeterGroup.cs.lift ⟨Coxeter.permRepAux_equiv, ⋯⟩

noncomputable def Coxeter.η {W : Type u_1} [CoxeterGroup W] (w t : W) : ZMod 2

Equations

• Coxeter.η w t = ↑(List.count t (Coxeter.CoxeterGroup.cs.leftInvSeq (Classical.choose ⋯)))

theorem Coxeter.permRep_wordProd_eq_permRepAux {W : Type u_1} [CoxeterGroup W] (ω : List (CoxeterGroup.B W)) : ⇑(permRep (CoxeterGroup.cs.wordProd ω)) = permRepAux ω

theorem Coxeter.eta_spec {W : Type u_1} [CoxeterGroup W] (ω : List (CoxeterGroup.B W)) (t : W) : η (CoxeterGroup.cs.wordProd ω) t = ↑(List.count t (CoxeterGroup.cs.leftInvSeq ω))

@[simp]

theorem Coxeter.eta_simple {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) : η (CoxeterGroup.cs.simple i) (CoxeterGroup.cs.simple i) = 1

@[simp]

theorem Coxeter.eta_conj {W : Type u_1} [CoxeterGroup W] (i : CoxeterGroup.B W) (t : W) : η (CoxeterGroup.cs.simple i) (CoxeterGroup.cs.simple i * t * (CoxeterGroup.cs.simple i)⁻¹) = η (CoxeterGroup.cs.simple i) t

theorem Coxeter.permRep_eq {W : Type u_1} [CoxeterGroup W] (w : W) (r : RootSet W) : (permRep w) r = (⟨(MulAut.conj w) ↑r.1, ⋯⟩, r.2 + η w⁻¹ ↑r.1)

theorem Coxeter.permRep_inv_eq {W : Type u_1} [CoxeterGroup W] (w : W) (r : RootSet W) : (permRep w⁻¹) r = (⟨(MulAut.conj w⁻¹) ↑r.1, ⋯⟩, r.2 + η w ↑r.1)

theorem Coxeter.permRep_inj {W : Type u_1} [CoxeterGroup W] : Function.Injective ⇑permRep

Bjorner--Brenti Theorem 1.3.2 (i): injectivity

theorem Coxeter.permRep_reflection {W : Type u_1} [CoxeterGroup W] (t : ReflectionSet W) (ε : ZMod 2) : (permRep ↑t) (t, ε) = (t, ε + 1)

Bjorner--Brenti Theorem 1.3.2 (ii)

theorem Coxeter.isLeftInversion_of_eta_eq_one {W : Type u_1} [CoxeterGroup W] {w t : W} (h : η w t = 1) : CoxeterGroup.cs.IsLeftInversion w t

theorem Coxeter.not_isLeftInversion_of_eta_eq_zero {W : Type u_1} [CoxeterGroup W] {w t : W} (h : η w t = 0) : ¬CoxeterGroup.cs.IsLeftInversion w t

theorem Coxeter.eta_eq_one_iff {W : Type u_1} [CoxeterGroup W] {t w : W} : η w t = 1 ↔ CoxeterGroup.cs.IsLeftInversion w t

theorem Coxeter.eta_eq_zero_iff {W : Type u_1} [CoxeterGroup W] {t w : W} : η w t = 0 ↔ ¬CoxeterGroup.cs.IsLeftInversion w t