Coxeter

Results named in Tau Ceti's TauCeti.GroupTheory.Coxeter modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremDeodhar's lemma#

Let u be a minimal coset representative for cs.parabolic J and let s i be a simple reflection. Then either s i * u is again a minimal coset representative, or s i * u = u * s j for some j ∈ J, so that s i * u lies in the coset of u. The second case can only occur when s i * u is longer than u.

CoxeterSystem.IsMinimalCosetRep.simple_mul_or_exists_eq_mul_simple.{u_1, u_2} {B : Type u_1}
  {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {u : W}
  (hu : cs.IsMinimalCosetRep J u) (i : B) :
  cs.IsMinimalCosetRep J (cs.simple i * u) ∨ ∃ j ∈ J, cs.simple i * u = u * cs.simple j
Lean

Formalized in Tau Ceti as CoxeterSystem.IsMinimalCosetRep.simple_mul_or_exists_eq_mul_simple.

Sources
LeanCoxeterSystem.IsMinimalCosetRep.simple_mul_or_exists_eq_mul_simple

TheoremMatsumoto's theorem, relational form#

Two reduced words representing the same element of a Coxeter group are connected by braid moves.

TauCeti.braidEquivalent_of_isReduced_wordProd_eq.{u_1, u_2} {B : Type u_1} {W : Type u_2} [Group W]
  {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω ω' : List B} (hω : cs.IsReduced ω)
  (hω' : cs.IsReduced ω') (hprod : cs.wordProd ω = cs.wordProd ω') :
  CoxeterSystem.BraidEquivalent M ω ω'
Lean

Formalized in Tau Ceti as TauCeti.braidEquivalent_of_isReduced_wordProd_eq.

Other forms

Matsumoto's theorem, monoid-valued form. Formalized in Tau Ceti as TauCeti.matsumoto.

TauCeti.matsumoto.{u_1, u_2, u_3} {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B}
  (cs : CoxeterSystem M W) {G : Type u_3} [Monoid G] (f : B → G)
  (hbraid :
    ∀ (i j : B),
      (List.map f (CoxeterSystem.braidWord M i j)).prod =
        (List.map f (CoxeterSystem.braidWord M j i)).prod)
  {ω ω' : List B} (hω : cs.IsReduced ω) (hω' : cs.IsReduced ω')
  (hprod : cs.wordProd ω = cs.wordProd ω') : (List.map f ω).prod = (List.map f ω').prod
Sources
LeanTauCeti.braidEquivalent_of_isReduced_wordProd_eq · TauCeti.matsumoto
Uses 1 · Used by 3
Proof usesTits' lemma
Used byOcneanu's theorem · The basis theorem · Demazure's formula on a basis element

TheoremTits' lemma#

If i ≠ i' are both left descents of w, then w splits as a rank-two parabolic factor times a remainder, the lengths adding, and the parabolic factor is spelled by both alternating words of length orderOf (s i * s i').

Classically the exponent is the Coxeter-matrix entry M i i'; the order of s i * s i' divides it (CoxeterSystem.simple_mul_simple_pow), which gives the bound CoxeterSystem.length_le_of_isLeftDescent_pair, and the two agree by Tits' theorem on the geometric representation — see the module docstring.

CoxeterSystem.exists_wordProd_alternatingWord_mul_of_isLeftDescent_pair.{u_1, u_2} {B : Type u_1}
  {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i i' : B} (hne : i ≠ i')
  {w : W} (hd : cs.IsLeftDescent w i) (hd' : cs.IsLeftDescent w i') :
  ∃ v,
    0 < orderOf (cs.simple i * cs.simple i') ∧
      w =
          cs.wordProd (CoxeterSystem.alternatingWord i i' (orderOf (cs.simple i * cs.simple i'))) *
            v ∧
        w =
            cs.wordProd
                (CoxeterSystem.alternatingWord i' i (orderOf (cs.simple i * cs.simple i'))) *
              v ∧
          cs.length w = orderOf (cs.simple i * cs.simple i') + cs.length v
Lean

Formalized in Tau Ceti as CoxeterSystem.exists_wordProd_alternatingWord_mul_of_isLeftDescent_pair.

Sources
LeanCoxeterSystem.exists_wordProd_alternatingWord_mul_of_isLeftDescent_pair
Used by 1
Used byMatsumoto's theorem, relational form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.