ParabolicReadBraid.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The parabolic read respects braid relations by the reduced-word theorem.

theorem OAI.HarmonicArtin.ParabolicIntersections.parabolicRead_word_eq line 17
Source documentation
Equal reduced galleries have equal positive reads in the parabolic.
```
theorem parabolicRead_word_eq (w : M.Group) (u v : List S)
    (hu : (cs).IsReduced u) (hv : (cs).IsReduced v) (he : (cs).wordProd u=(cs).wordProd v) :
    wordArtin R (parabolicRead cs J w u)=wordArtin R (parabolicRead cs J w v) := by
…
```
Mentions: OAI.HarmonicArtin.wordArtin, OAI.HarmonicArtin.ParabolicIntersections.parabolicRead
theorem OAI.HarmonicArtin.ParabolicIntersections.parabolicRead_braid line 31
Source documentation
The precise braid compatibility needed for the parabolic retraction.
```
theorem parabolicRead_braid (w : M.Group) (i j : S) :
    wordArtin R (parabolicRead cs J w (altList i j (M i j))) =
      wordArtin R (parabolicRead cs J w (altList j i (M i j))) := by
…
```
Mentions: OAI.HarmonicArtin.wordArtin, OAI.HarmonicArtin.ParabolicIntersections.parabolicRead