Permutation representation of Coxeter groups

This file defines the permutation representation of a Coxeter group.

Main definitions

• Coxeter.ReflectionSet
• Coxeter.AbstractRootSet
• Coxeter.permRep
• Coxeter.eta

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.AbstractRootSet (W : Type u_1) [CoxeterGroup W] : Type u_1

Equations

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

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

Induction principle for reflections

Construction of the permutation representation

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 : AbstractRootSet W) : AbstractRootSet 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_append {W : Type u_1} [CoxeterGroup W] (ω₁ ω₂ : List (CoxeterGroup.B W)) : permRepAux (ω₁ ++ ω₂) = permRepAux ω₁ ∘ permRepAux ω₂

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_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 (AbstractRootSet 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 (AbstractRootSet W)

Bjorner--Brenti Theorem 1.3.2 (i): extension

Equations

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

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

Equations

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

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

Properties of $η$

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

theorem Coxeter.eta_mul {W : Type u_1} [CoxeterGroup W] (u w t : W) : eta (u * w) t = eta u t + eta w (u⁻¹ * t * u)

@[simp]

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

theorem Coxeter.eta_reflection_self {W : Type u_1} [CoxeterGroup W] {t : W} (ht : CoxeterGroup.cs.IsReflection t) : eta t t = 1

theorem Coxeter.isLeftInversion_of_eta_eq_one {W : Type u_1} [CoxeterGroup W] {w t : W} (h : eta 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 : eta w t = 0) : ¬CoxeterGroup.cs.IsLeftInversion w t

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

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

Properties of the permutation representation

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

theorem Coxeter.permRep_inv_eq {W : Type u_1} [CoxeterGroup W] (w : W) (r : AbstractRootSet W) : (permRep w⁻¹) r = (⟨(MulAut.conj w⁻¹) ↑r.1, ⋯⟩, r.2 + eta 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)