ParabolicReadReduced.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A parabolic read of a reduced gallery is reduced.

lemma OAI.HarmonicArtin.ParabolicIntersections.conjugate_sequence line 11
theorem OAI.HarmonicArtin.ParabolicIntersections.reduced_of_nodup_inversions line 20
Source documentation
The converse to the usual no-repeated-inversion property.
```
theorem reduced_of_nodup_inversions (u : List S) (hu : (cs.leftInvSeq u).Nodup) :
    cs.IsReduced u := by
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.parabolicRead_inversions line 37
Source documentation
The read gallery crosses a subsequence of the original reflecting walls; conjugating by the initial component identifies their labels.
```
theorem parabolicRead_inversions (J : Set S) (w : W) (u : List S) :
    ((cs.leftInvSeq ((parabolicRead cs J w u).map Subtype.val)).map
      (MulAut.conj (parabolicComponent cs J w))).Sublist
      ((cs.leftInvSeq u).map (MulAut.conj w)) := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.parabolicRead, OAI.HarmonicArtin.ParabolicIntersections.parabolicComponent
theorem OAI.HarmonicArtin.ParabolicIntersections.parabolicRead_reduced line 70
Source documentation
Retraction to a standard parabolic preserves reducedness of galleries, allowing letters which do not cross a parabolic wall to disappear.
```
theorem parabolicRead_reduced (J : Set S) (w : W) (u : List S) (hu : cs.IsReduced u) :
    cs.IsReduced ((parabolicRead cs J w u).map Subtype.val) := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.parabolicRead