OAI/Topology/ArtinGroups/ParabolicIntersections/ParabolicRead.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Reading the parabolic letters crossed by a Coxeter gallery.

  1. def OAI.HarmonicArtin.ParabolicIntersections.parabolicLetterValue line 12
  2. def OAI.HarmonicArtin.ParabolicIntersections.parabolicLetter line 16
  3. def OAI.HarmonicArtin.ParabolicIntersections.parabolicStepLetter line 19
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicStepLetter_value line 22
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicStepLetter_reverse line 31
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicStepLetter_conjugate line 36
  7. def OAI.HarmonicArtin.ParabolicIntersections.parabolicRead line 55
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicLetter_word line 59
  9. theorem OAI.HarmonicArtin.ParabolicIntersections.parabolicRead_product line 64

    Source documentation

    The read word records exactly the change in the parabolic component.

    theorem parabolicRead_product (w : W) (u : List S) :
    cs.wordProd ((parabolicRead cs J w u).map Subtype.val) =
      (parabolicComponent cs J w)⁻¹*parabolicComponent cs J (w*cs.wordProd u) := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.parabolicRead, OAI.HarmonicArtin.ParabolicIntersections.parabolicComponent