def CoxeterSystem.M (n : ℕ) : CoxeterMatrix (Fin n)

Equations

• CoxeterSystem.M n = CoxeterMatrix.Aₙ n

def CoxeterSystem.cs (n : ℕ) : CoxeterSystem (CoxeterSystem.M n) (CoxeterSystem.M n).Group

Equations

• CoxeterSystem.cs n = (CoxeterSystem.M n).toCoxeterSystem

@[reducible, inline]

abbrev CoxeterSystem.S (n : ℕ) : Type

Equations

• CoxeterSystem.S n = Equiv.Perm (Fin n)

@[reducible, inline]

abbrev CoxeterSystem.S' (n : ℕ) : Type

Equations

• CoxeterSystem.S' n = (CoxeterSystem.M n).Group

instance CoxeterSystem.instGroupSHAddNatOfNat (n : ℕ) : Group (CoxeterSystem.S (n + 1))

Equations

• CoxeterSystem.instGroupSHAddNatOfNat n = Equiv.Perm.permGroup

def CoxeterSystem.f_simple (n : ℕ) : Fin n → CoxeterSystem.S (n + 1)

Equations

• CoxeterSystem.f_simple n i = Equiv.swap i.castSucc i.succ

theorem CoxeterSystem.cycle_of_adjacent_swap (n : ℕ) (i : Fin n) (j : Fin n) (hij : i ≠ j) (h1 : j.succ = i.castSucc ∨ i.succ = j.castSucc) : (Equiv.swap i.castSucc i.succ * Equiv.swap j.castSucc j.succ).IsThreeCycle

theorem CoxeterSystem.f_liftable (n : ℕ) : (CoxeterSystem.M n).IsLiftable (CoxeterSystem.f_simple n)

def CoxeterSystem.f (n : ℕ) : (CoxeterSystem.M n).Group →* CoxeterSystem.S (n + 1)

Equations

• CoxeterSystem.f n = (CoxeterSystem.cs n).lift ⟨CoxeterSystem.f_simple n, ⋯⟩

theorem CoxeterSystem.f_apply_simple (n : ℕ) (i : Fin n) : (CoxeterSystem.f n) ((CoxeterSystem.cs n).simple i) = Equiv.swap i.castSucc i.succ

theorem CoxeterSystem.f_surjective (n : ℕ) : Function.Surjective ⇑(CoxeterSystem.f n)

def CoxeterSystem.f_equiv (n : ℕ) : CoxeterSystem.S' n ≃* CoxeterSystem.S (n + 1)

Equations

• CoxeterSystem.f_equiv n = MulEquiv.ofBijective (CoxeterSystem.f n) ⋯

theorem CoxeterSystem.f_equiv_apply_simple (n : ℕ) (i : Fin n) : (CoxeterSystem.f_equiv n) ((CoxeterSystem.cs n).simple i) = Equiv.swap i.castSucc i.succ

def CoxeterSystem.S_cox (n : ℕ) : CoxeterSystem (CoxeterSystem.M n) (CoxeterSystem.S (n + 1))

Equations

• CoxeterSystem.S_cox n = { mulEquiv := (CoxeterSystem.f_equiv n).symm }

theorem CoxeterSystem.S_cox_simple (n : ℕ) (i : Fin n) : (CoxeterSystem.S_cox n).simple i = Equiv.swap i.castSucc i.succ

instance CoxeterSystem.instOfMatsumotoReady (n : ℕ) : (CoxeterSystem.S_cox n).MatsumotoCondition

Equations

• CoxeterSystem.instOfMatsumotoReady n = { one_le_M := ⋯, alternatingWords_ne_one := ⋯ }