OAI/Topology/ArtinGroups/ParabolicIntersections/CoxeterChainRoots.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Positive roots carried along a simple path in the noncommutation graph.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.reflection_nonneg_of_zero line 13
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.reflection_pos_of_neighbor line 31
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.root_along_chain line 54

    Source documentation

    A word of distinct vertices along a noncommutation path carries the last simple root to a nonnegative root positive at every vertex of the path.

    theorem root_along_chain (u : List S) (s : S) (hN : (u++[s]).Nodup)
    (hC : (u++[s]).IsChain (fun a b => a≠b ∧ M a b≠2)) :
    let x := representation M.toCoxeterSystem (M.toCoxeterSystem.wordProd u) (Pi.single s 1)
…