LeanPool.DemazureOperatorsLean.StrongExchange

@[implicit_reducible]

noncomputable instance CoxeterSystem.instDecidableEqLeanPool {W : Type} : DecidableEq W

Equations

• CoxeterSystem.instDecidableEqLeanPool = Classical.typeDecidableEq W

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

The subtype of reflections in a Coxeter system.

Equations

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

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

The number of times a reflection appears in the left inversion sequence of a word.

Equations

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

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

The parity of the number of occurrences of a reflection in a left inversion sequence.

Equations

• cs.reflectionMemLeftInvSeqParity l t = ↑(cs.reflectionMemLeftInvSeqCount l t)

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

Conjugate a reflection and keep its reflection witness.

Equations

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

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

The parity contribution of a simple reflection to the permutation action.

Equations

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

theorem CoxeterSystem.eta_eq_eta_of_simpleConj {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (t : cs.Reflection) : cs.eta i t = cs.eta i (cs.conjOfReflection t (cs.simple i))

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

The permutation action associated to a simple reflection.

Equations

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

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

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

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

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

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

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

@[implicit_reducible]

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

Equations

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

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

@[implicit_reducible]

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

Equations

• cs.instMonoidForallProdReflectionZModOfNatNat = { toMul := cs.instMul, mul_assoc := ⋯, one := id, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }

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

The permutation map associated to a word, built by composing simple permutation maps.

Equations

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

theorem CoxeterSystem.isReflection_conj_inv_mul_mul {B 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 W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {t : cs.Reflection} {z : ZMod 2} (l : List B) : (cs.permutationMapOfList l (t, z)).1 = cs.conjOfReflection t (cs.wordProd l)

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

theorem CoxeterSystem.permutationMap_ofList_mk {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (t : cs.Reflection) (z : ZMod 2) : cs.permutationMapOfList l (t, z) = (cs.conjOfReflection t (cs.wordProd l), z + cs.reflectionMemLeftInvSeqParity l.reverse t)

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

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

The homomorphic lift of the simple permutation maps to the Coxeter group.

Equations

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

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

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

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

The parity of reflection occurrences defined using the lifted permutation action.

Equations

• cs.parityReflectionOccurrencesLift w t = (cs.permutationMapLift w⁻¹ (t, 0)).2

theorem CoxeterSystem.parityReflectionOccurrences_lift_mk {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (t : cs.Reflection) : cs.parityReflectionOccurrencesLift (cs.wordProd l) t = cs.reflectionMemLeftInvSeqParity l t

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

theorem CoxeterSystem.parityReflectionOccurrences_ext {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l l' : List B) (t : cs.Reflection) (h : cs.wordProd l = cs.wordProd l') : cs.reflectionMemLeftInvSeqParity l t = cs.reflectionMemLeftInvSeqParity 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 W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (t : cs.Reflection) (h : cs.reflectionMemLeftInvSeqParity l t = 1) : ↑t ∈ cs.leftInvSeq l

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

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

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

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

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

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

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