OAI/Topology/ArtinGroups/ParabolicIntersections/ParabolicRetractionAction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The parabolic gallery retraction as an action of the Artin presentation.

  1. def OAI.HarmonicArtin.ParabolicIntersections.parabolicStepArtin line 15
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicStepArtin_reverse line 19
  3. def OAI.HarmonicArtin.ParabolicIntersections.parabolicStepPerm line 24
  4. def OAI.HarmonicArtin.ParabolicIntersections.parabolicWordPerm line 40
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicWordPerm_apply line 45

    Source documentation

    Using the opposite permutation group makes the word act in its written order.

    lemma parabolicWordPerm_apply (u : List S) (w : M.Group) (a : Artin R) :
    MulOpposite.unop (parabolicWordPerm M J u) (w,a) =
      (w*(cs).wordProd u,a*wordArtin R (parabolicRead cs J w u)) := by
…

    Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.parabolicWordPerm, OAI.HarmonicArtin.wordArtin, OAI.HarmonicArtin.ParabolicIntersections.parabolicRead

  6. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicWordPerm_braid line 56
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicPerm_relators line 65
  8. def OAI.HarmonicArtin.ParabolicIntersections.parabolicRetractionAction line 73
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.parabolicRetractionAction_generator line 76