instance CoxeterSystem.instDecidableEq_demazureOperators {W : Type} : DecidableEq W

Equations

• CoxeterSystem.instDecidableEq_demazureOperators = Classical.typeDecidableEq W

def CoxeterSystem.T {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Type

Equations

• cs.T = { t : W // cs.IsReflection t }

def CoxeterSystem.nReflectionOccurrences {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (t : cs.T) : ℕ

Equations

• cs.nReflectionOccurrences l t = List.count (↑t) (cs.leftInvSeq l)

def CoxeterSystem.parityReflectionOccurrences {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (t : cs.T) : ZMod 2

Equations

• cs.parityReflectionOccurrences l t = ↑(cs.nReflectionOccurrences l t)

def CoxeterSystem.conj {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (t : cs.T) (w : W) : cs.T

Equations

• cs.conj t w = ⟨w * ↑t * w⁻¹, ⋯⟩

theorem CoxeterSystem.t_eq_conj_t {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (t : cs.T) : t = cs.conj t ↑t

def CoxeterSystem.eta {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (t : cs.T) : ZMod 2

Equations

• cs.eta i t = if cs.simple i = ↑t then 1 else 0

theorem CoxeterSystem.eta_simpleConj_eq_eta {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (t : cs.T) : cs.eta i t = cs.eta i (cs.conj t (cs.simple i))

def CoxeterSystem.permutationMap {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : cs.T × ZMod 2 → cs.T × ZMod 2

Equations

• cs.permutationMap i (t, z) = (cs.conj t (cs.simple i), z + cs.eta i t)

theorem CoxeterSystem.permutationMap_orderTwo {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : cs.permutationMap i ∘ cs.permutationMap i = id

theorem CoxeterSystem.Odd.add_one {n : ℕ} : Odd n → Even (n + 1)

theorem CoxeterSystem.getElem_alternatingWord {B : Type} (i : B) (j : B) (p : ℕ) (k : Fin (CoxeterSystem.alternatingWord i j p).length) : (CoxeterSystem.alternatingWord i j p)[k] = if Even (p + ↑k) then i else j

theorem CoxeterSystem.getElem_alternatingWord' {B : Type} (i : B) (j : B) (p : ℕ) (k : ℕ) (h : k < p) : (CoxeterSystem.alternatingWord i j p)[k] = if Even (p + k) then i else j

theorem CoxeterSystem.lt_of_lt_plus_one (k : ℕ) (n : ℕ) (h : k + 1 < n) : k < n

theorem CoxeterSystem.alternatingWordLength_eq_reverse_alternatingWordLength {B : Type} (i : B) (j : B) (p : ℕ) : (CoxeterSystem.alternatingWord i j p).length = (CoxeterSystem.alternatingWord j i p).length

theorem CoxeterSystem.centralS_equal_swapping_indices {B : Type} (i : B) (j : B) (p : ℕ) (k : ℕ) (h : k + 1 < (CoxeterSystem.alternatingWord i j p).length) : (CoxeterSystem.alternatingWord i j p)[k + 1] = (CoxeterSystem.alternatingWord j i p)[k]

theorem CoxeterSystem.get_leftInvSeq {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (j : Fin l.length) : (cs.leftInvSeq l).get ⟨↑j, ⋯⟩ = cs.wordProd (List.take (↑j) l) * cs.simple (l.get ⟨↑j, ⋯⟩) * (cs.wordProd (List.take (↑j) l))⁻¹

theorem CoxeterSystem.eq_flip_variables {B : Type} (i : B) (j : B) (p : ℕ) : (if Even p then j else i) = if Even (p + 1) then i else j

theorem CoxeterSystem.list_take_alternatingWord {B : Type} {p : ℕ} (i : B) (j : B) (k : ℕ) (h : k < 2 * p) : List.take k (CoxeterSystem.alternatingWord i j (2 * p)) = if Even k then CoxeterSystem.alternatingWord i j k else CoxeterSystem.alternatingWord j i k

theorem CoxeterSystem.list_take_induction {B : Type} (i : B) (j : B) (p : ℕ) (k : ℕ) (h : k + 1 < 2 * p) : List.take (k + 1) (CoxeterSystem.alternatingWord i j (2 * p)) = i :: List.take k (CoxeterSystem.alternatingWord j i (2 * p))

theorem CoxeterSystem.leftInvSeq_alternatingWord_induction {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (j : B) (p : ℕ) (k : ℕ) (h : k + 1 < 2 * p) : (cs.leftInvSeq (CoxeterSystem.alternatingWord i j (2 * p))).get ⟨k + 1, ⋯⟩ = (MulAut.conj (cs.simple i)) ((cs.leftInvSeq (CoxeterSystem.alternatingWord j i (2 * p))).get ⟨k, ⋯⟩)

theorem CoxeterSystem.alternatingWord_of_get_leftInvSeq_alternatingWord {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (j : B) (p : ℕ) (k : ℕ) (h : k < 2 * p) : (cs.leftInvSeq (CoxeterSystem.alternatingWord i j (2 * p))).get ⟨k, ⋯⟩ = cs.wordProd (CoxeterSystem.alternatingWord j i (2 * k + 1))

theorem CoxeterSystem.alternatingWord_of_getElem_leftInvSeq_alternatingWord {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (j : B) (p : ℕ) (k : ℕ) (h : k < 2 * p) : (cs.leftInvSeq (CoxeterSystem.alternatingWord i j (2 * p)))[k] = cs.wordProd (CoxeterSystem.alternatingWord j i (2 * k + 1))

theorem CoxeterSystem.leftInvSeq_repeats {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i : B} {j : B} (k : ℕ) (h : k < M.M i j) : (cs.leftInvSeq (CoxeterSystem.alternatingWord i j (2 * M.M i j))).get ⟨M.M i j + k, ⋯⟩ = (cs.leftInvSeq (CoxeterSystem.alternatingWord i j (2 * M.M i j))).get ⟨k, ⋯⟩

theorem CoxeterSystem.leftInvSeq_repeats' {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i : B} {j : B} (k : ℕ) (h : k < M.M i j) : (cs.leftInvSeq (CoxeterSystem.alternatingWord i j (2 * M.M i j)))[M.M i j + k] = (cs.leftInvSeq (CoxeterSystem.alternatingWord i j (2 * M.M i j)))[k]

theorem CoxeterSystem.nReflectionOccurrences_even_braidWord {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i : B} {j : B} (t : cs.T) : Even (cs.nReflectionOccurrences (CoxeterSystem.alternatingWord i j (2 * M.M i j)) t)

theorem CoxeterSystem.parityReflectionOccurrences_braidWord {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i : B} {j : B} (t : cs.T) : cs.parityReflectionOccurrences (CoxeterSystem.alternatingWord i j (2 * M.M i j)) t = 0

theorem CoxeterSystem.alternatingWord_reverse : ∀ {α : Type u_1} {i j : α} {p : ℕ}, (CoxeterSystem.alternatingWord i j (2 * p)).reverse = CoxeterSystem.alternatingWord j i (2 * p)

instance CoxeterSystem.instMul {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Mul (cs.T × ZMod 2 → cs.T × ZMod 2)

Equations

• cs.instMul = { mul := fun (f g : cs.T × ZMod 2 → cs.T × ZMod 2) => f ∘ g }

theorem CoxeterSystem.mulDef {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (f : cs.T × ZMod 2 → cs.T × ZMod 2) (g : cs.T × ZMod 2 → cs.T × ZMod 2) : f * g = f ∘ g

instance CoxeterSystem.instMonoidForallProdTZModOfNatNat {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Monoid (cs.T × ZMod 2 → cs.T × ZMod 2)

Equations

• cs.instMonoidForallProdTZModOfNatNat = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

def CoxeterSystem.permutationMap_ofList {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) : cs.T × ZMod 2 → cs.T × ZMod 2

Equations

• cs.permutationMap_ofList [] = id
• cs.permutationMap_ofList (a :: t) = cs.permutationMap a * cs.permutationMap_ofList t

theorem CoxeterSystem.IsReflection.conj' {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {t : W} (ht : cs.IsReflection t) (w : W) : cs.IsReflection (w⁻¹ * t * w)

theorem CoxeterSystem.permutationMap_ofList_mk_1 {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {t : cs.T} {z : ZMod 2} (l : List B) : (cs.permutationMap_ofList l (t, z)).1 = cs.conj t (cs.wordProd l)

theorem CoxeterSystem.permutationMap_ofList_mk_2 {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {t : cs.T} {z : ZMod 2} (l : List B) : (cs.permutationMap_ofList l (t, z)).2 = z + cs.parityReflectionOccurrences l.reverse t

theorem CoxeterSystem.permutationMap_ofList_mk {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (t : cs.T) (z : ZMod 2) : cs.permutationMap_ofList l (t, z) = (cs.conj t (cs.wordProd l), z + cs.parityReflectionOccurrences l.reverse t)

theorem CoxeterSystem.permutationMap_isLiftable {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : M.IsLiftable cs.permutationMap

def CoxeterSystem.permutationMap_lift {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : W →* cs.T × ZMod 2 → cs.T × ZMod 2

Equations

• cs.permutationMap_lift = cs.lift ⟨cs.permutationMap, ⋯⟩

theorem CoxeterSystem.permutationMap_lift_mk_ofList {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (t : cs.T) (z : ZMod 2) : cs.permutationMap_lift (cs.wordProd l) (t, z) = cs.permutationMap_ofList l (t, z)

theorem CoxeterSystem.permutationMap_ext {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (l' : List B) (t : cs.T) (z : ZMod 2) (h : cs.wordProd l = cs.wordProd l') : cs.permutationMap_ofList l (t, z) = cs.permutationMap_ofList l' (t, z)

def CoxeterSystem.parityReflectionOccurrences_lift {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (t : cs.T) : ZMod 2

Equations

• cs.parityReflectionOccurrences_lift w t = (cs.permutationMap_lift w⁻¹ (t, 0)).2

theorem CoxeterSystem.parityReflectionOccurrences_lift_mk {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (t : cs.T) : cs.parityReflectionOccurrences_lift (cs.wordProd l) t = cs.parityReflectionOccurrences l t

theorem CoxeterSystem.permutationMap_lift_mk {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (t : cs.T) (z : ZMod 2) : cs.permutationMap_lift w (t, z) = (⟨w * ↑t * w⁻¹, ⋯⟩, z + cs.parityReflectionOccurrences_lift w⁻¹ t)

theorem CoxeterSystem.parityReflectionOccurrences_ext {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (l' : List B) (t : cs.T) (h : cs.wordProd l = cs.wordProd l') : cs.parityReflectionOccurrences l t = cs.parityReflectionOccurrences l' t

theorem CoxeterSystem.odd_iff_parity_eq_one (n : ℕ) : Odd n ↔ ↑n = 1

theorem CoxeterSystem.gt_one_of_odd (n : ℕ) : Odd n → n > 0

theorem CoxeterSystem.isInLeftInvSeq_of_parityReflectionOccurrences_eq_one {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (t : cs.T) (h : cs.parityReflectionOccurrences l t = 1) : ↑t ∈ cs.leftInvSeq l

theorem CoxeterSystem.isLeftInversion_of_parityReflectionOccurrences_eq_one {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (t : cs.T) : cs.parityReflectionOccurrences l t = 1 → cs.IsLeftInversion (cs.wordProd l) ↑t

theorem CoxeterSystem.isLeftInversion_of_parityReflectionOccurrences_lift_eq_one {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (t : cs.T) : cs.parityReflectionOccurrences_lift w t = 1 → cs.IsLeftInversion w ↑t

theorem CoxeterSystem.eraseIdx_of_mul_leftInvSeq {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (t : cs.T) (h : ↑t ∈ cs.leftInvSeq l) : ∃ (k : Fin l.length), ↑t * cs.wordProd l = cs.wordProd (l.eraseIdx ↑k)

theorem CoxeterSystem.permutationMap_lift_simple {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (p : B) : cs.permutationMap_lift (cs.simple p) = cs.permutationMap p

theorem CoxeterSystem.permutationMap_lift_of_reflection {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (t : cs.T) (z : ZMod 2) : cs.permutationMap_lift ↑t (t, z) = (t, z + 1)

theorem CoxeterSystem.isLeftInversion_iff_parityReflectionOccurrences_eq_one {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (t : cs.T) : cs.IsLeftInversion (cs.wordProd l) ↑t ↔ cs.parityReflectionOccurrences l t = 1

theorem CoxeterSystem.strongExchangeProperty {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (t : cs.T) (h' : cs.IsLeftInversion (cs.wordProd l) ↑t) : ∃ (k : Fin l.length), ↑t * cs.wordProd l = cs.wordProd (l.eraseIdx ↑k)