Documentation

Coxeter.StrongExchange

Strong exchange #

This file proves the strong exchange and related properties of Coxeter groups.

Main statements #

References #

source
theorem Coxeter.mem_leftInvSeq_of_isLeftInversion {W : Type u_1} [CoxeterGroup W] {ω : List (CoxeterGroup.B W)} {t : W} (h : CoxeterGroup.cs.IsLeftInversion (CoxeterGroup.cs.wordProd ω) t) :
t ∈ CoxeterGroup.cs.leftInvSeq ω

Bjorner--Brenti Corollary 1.4.4 (a) implies (c)

source
theorem Coxeter.isLeftInversion_iff_mem_leftInvSeq {W : Type u_1} [CoxeterGroup W] {ω : List (CoxeterGroup.B W)} (hω : CoxeterGroup.cs.IsReduced ω) (t : W) :
CoxeterGroup.cs.IsLeftInversion (CoxeterGroup.cs.wordProd ω) t ↔ t ∈ CoxeterGroup.cs.leftInvSeq ω

Bjorner--Brenti Corollary 1.4.4 (a) iff (c)

source
theorem Coxeter.strong_exchange {W : Type u_1} [CoxeterGroup W] {ω : List (CoxeterGroup.B W)} {t : W} (h : CoxeterGroup.cs.IsLeftInversion (CoxeterGroup.cs.wordProd ω) t) :
∃ i < ω.length, t * CoxeterGroup.cs.wordProd ω = CoxeterGroup.cs.wordProd (ω.eraseIdx i)

Bjorner--Brenti Theorem 1.4.3

source
theorem Coxeter.exchange_property {W : Type u_1} [CoxeterGroup W] {ω : List (CoxeterGroup.B W)} {i : CoxeterGroup.B W} (h : CoxeterGroup.cs.IsLeftDescent (CoxeterGroup.cs.wordProd ω) i) :
∃ j < ω.length, CoxeterGroup.cs.simple i * CoxeterGroup.cs.wordProd ω = CoxeterGroup.cs.wordProd (ω.eraseIdx j)
source
def Coxeter.equiv_IsLeftInversion {W : Type u_1} [CoxeterGroup W] (ω : List (CoxeterGroup.B W)) (hω : CoxeterGroup.cs.IsReduced ω) :
{ t : W // CoxeterGroup.cs.IsLeftInversion (CoxeterGroup.cs.wordProd ω) t } ≃ { t : W // t ∈ CoxeterGroup.cs.leftInvSeq ω }
Equations
Instances For
    source
    instance Coxeter.instFiniteSubtypeIsLeftInversionBCs {W : Type u_1} [CoxeterGroup W] {w : W} :
    Finite { t : W // CoxeterGroup.cs.IsLeftInversion w t }
    source
    theorem Coxeter.card_of_isLeftInversion {W : Type u_1} [CoxeterGroup W] (w : W) :
    Nat.card { t : W // CoxeterGroup.cs.IsLeftInversion w t } = CoxeterGroup.cs.length w

    Bjorner--Brenti Corollary 1.4.5

    source
    theorem Coxeter.deletion_property {W : Type u_1} [CoxeterGroup W] {ω : List (CoxeterGroup.B W)} (hω : ¬CoxeterGroup.cs.IsReduced ω) :
    ∃ (i : ℕ) (j : ℕ), i < j ∧ j < ω.length ∧ CoxeterGroup.cs.wordProd ω = CoxeterGroup.cs.wordProd ((ω.eraseIdx j).eraseIdx i)

    Bjorner--Brenti Proposition 1.4.7

    source
    theorem Coxeter.exists_reduced_subword {W : Type u_1} [CoxeterGroup W] (ω : List (CoxeterGroup.B W)) :
    ∃ (ω' : List (CoxeterGroup.B W)), ω'.Sublist ω ∧ CoxeterGroup.cs.IsReduced ω' ∧ CoxeterGroup.cs.wordProd ω = CoxeterGroup.cs.wordProd ω'

    Bjorner--Brenti Corollary 1.4.8 (i)

    source
    theorem Coxeter.exists_reduced_subword' {W : Type u_1} [CoxeterGroup W] {w : W} {ω : List (CoxeterGroup.B W)} (h : w = CoxeterGroup.cs.wordProd ω) :
    ∃ (ω' : ReducedWord w), (↑ω').Sublist ω

    Right variants #

    source
    theorem Coxeter.strong_exchange_right {W : Type u_1} [CoxeterGroup W] {ω : List (CoxeterGroup.B W)} {t : W} (h : CoxeterGroup.cs.IsRightInversion (CoxeterGroup.cs.wordProd ω) t) :
    ∃ i < ω.length, CoxeterGroup.cs.wordProd ω * t = CoxeterGroup.cs.wordProd (ω.eraseIdx i)
    source
    theorem Coxeter.exchange_property_right {W : Type u_1} [CoxeterGroup W] {ω : List (CoxeterGroup.B W)} {i : CoxeterGroup.B W} (h : CoxeterGroup.cs.IsRightDescent (CoxeterGroup.cs.wordProd ω) i) :
    ∃ j < ω.length, CoxeterGroup.cs.wordProd ω * CoxeterGroup.cs.simple i = CoxeterGroup.cs.wordProd (ω.eraseIdx j)
    source
    def Coxeter.equiv_isRightInversion {W : Type u_1} [CoxeterGroup W] {w : W} :
    { t : W // CoxeterGroup.cs.IsRightInversion w t } ≃ { t : Wᵐᵒᵖ // CoxeterGroup.cs.IsLeftInversion (MulOpposite.op w) t }
    Equations
    Instances For
      source
      instance Coxeter.instFiniteSubtypeIsRightInversionBCs {W : Type u_1} [CoxeterGroup W] {w : W} :
      Finite { t : W // CoxeterGroup.cs.IsRightInversion w t }
      source
      theorem Coxeter.card_of_isRightInversion {W : Type u_1} [CoxeterGroup W] (w : W) :
      Nat.card { t : W // CoxeterGroup.cs.IsRightInversion w t } = CoxeterGroup.cs.length w