OAI/RepresentationTheory/Saxl/BandFactorization.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Saxl.highPositionsEquiv line 11
2. abbrev OAI.Saxl.bandSize line 25
3. def OAI.Saxl.cutPositions line 27
4. lemma OAI.Saxl.cutPositions_high line 33
5. lemma OAI.Saxl.cutPositions_left line 38
6. lemma OAI.Saxl.bandSize_add line 43
7. def OAI.Saxl.bandTableau line 47
8. def OAI.Saxl.bandRowGroup line 50
9. def OAI.Saxl.bandColumnGroup line 51
10. def OAI.Saxl.highLetter line 53
11. def OAI.Saxl.letterLift line 56
12. lemma OAI.Saxl.letterLift_single line 60
13. lemma OAI.Saxl.letterLift_altWord line 75
14. def OAI.Saxl.bandRowWord line 85
15. def OAI.Saxl.bandColumnWord line 89
16. lemma OAI.Saxl.row_cut_group line 93
17. lemma OAI.Saxl.column_cut_group line 100
18. lemma OAI.Saxl.highRow_word line 107
19. lemma OAI.Saxl.highColumn_word line 122
20. theorem OAI.Saxl.cutRowWord_factor line 142

    Source comment

    The first-layer exact band factorization, including the high-letter shift.

    theorem cutRowWord_factor (h s : ℕ) : cutRowWord h s =
        positionProduct (cutPositions h s)
          (letterLift (highLetter h s) (polytabloid (stairRowTableau h))) (bandRowWord h s) := by
    …

    Mentions: OAI.Saxl.cutRowWord, OAI.Saxl.positionProduct, OAI.Saxl.cutPositions, OAI.Saxl.letterLift, OAI.Saxl.highLetter, OAI.Saxl.polytabloid, OAI.Saxl.stairRowTableau, OAI.Saxl.bandRowWord

21. theorem OAI.Saxl.cutColumnWord_factor line 156

    Source comment

    The second-layer exact band factorization.

    theorem cutColumnWord_factor (h s : ℕ) : cutColumnWord h s =
        positionProduct (cutPositions h s)
          (letterLift (highLetter h s) (polytabloid (stairTableau h))) (bandColumnWord h s) := by
    …

    Mentions: OAI.Saxl.cutColumnWord, OAI.Saxl.positionProduct, OAI.Saxl.cutPositions, OAI.Saxl.letterLift, OAI.Saxl.highLetter, OAI.Saxl.polytabloid, OAI.Saxl.stairTableau, OAI.Saxl.bandColumnWord

22. lemma OAI.Saxl.bandTableau_bounds line 171
23. def OAI.Saxl.bandCellsEquiv line 180
24. def OAI.Saxl.pathCellsEquiv line 206
25. def OAI.Saxl.bandPathEquiv line 217

    Source comment

    The exact path order, starting at the bottom row singleton and ending at the rightmost column singleton.

    def bandPathEquiv (h : ℕ) : Fin (2*(h+1)+1) ≃ Fin (bandSize h 2) :=
    …

    Mentions: OAI.Saxl.bandSize

26. lemma OAI.Saxl.bandPath_coordinates line 220
27. lemma OAI.Saxl.bandPath_card line 225