OAI/Topology/ArtinGroups/ParabolicIntersections/CoxeterChainMinimum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A noncommutation path starting outside a parabolic gives a minimal Coxeter coset representative.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.conjugate_simple_not_parabolic line 14
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.minimum_append_chain line 41
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.chain_word_minimum line 60

    Source documentation

    Every prefix of a simple noncommutation path starting outside X is minimal in its left X-coset.

    theorem chain_word_minimum (X : Set S) (a : S) (ha : a∉X) (u : List S)
    (hN : (a::u).Nodup) (hC : (a::u).IsChain (fun a b => a≠b ∧ M a b≠2)) :
    IsParabolicMinimum cs X ((cs).wordProd (a::u)) := by
…