OAI/RepresentationTheory/Saxl/HighProjection.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Saxl.highRowEquiv line 11

   Source comment

   Translate the high part of each row to the smaller staircase.

   def highRowEquiv (h s : ℕ) :
       {x : (staircase (h+s)).cells // s ≤ x.val.2} ≃ (staircase h).cells where
   …

   Mentions: OAI.Saxl.staircase

2. def OAI.Saxl.highColEquiv line 27
3. theorem OAI.Saxl.high_positions_rigidity line 43
4. lemma OAI.Saxl.polytabloid_support line 96
5. def OAI.Saxl.sameHighProjection line 114

   Source comment

   Local same-high projection in the ordinary pair-letter coordinate space.

   def sameHighProjection (n d e s : ℕ) :
       Representation.IntertwiningMap (wordRep n (d*e)) (wordRep n (d*e)) where
   …

   Mentions: OAI.Saxl.wordRep

6. theorem OAI.Saxl.staircase_projected_high_positions line 129
7. lemma OAI.Saxl.columnAlt_left line 171
8. lemma OAI.Saxl.polytabloid_alternating line 189
9. def OAI.Saxl.rotateRowCell line 197

   Source comment

   Move low row letters to the band and high row letters to B_h.

   def rotateRowCell (h s : ℕ) (x : (staircase (h+s)).cells) : (staircase (h+s)).cells :=
   …

   Mentions: OAI.Saxl.staircase

10. lemma OAI.Saxl.rotateRowCell_injective line 203
11. def OAI.Saxl.rotateRow line 215
12. lemma OAI.Saxl.rotateRow_high line 218
13. def OAI.Saxl.rotateColumn line 224
14. lemma OAI.Saxl.rotateColumn_high line 227
15. def OAI.Saxl.rotateRowPositions line 233
16. def OAI.Saxl.rotateColumnPositions line 240
17. lemma OAI.Saxl.polytabloid_column_coeff line 247
18. theorem OAI.Saxl.staircase_projected_ne_zero line 257

    Source comment

    The projected generator is genuinely nonzero for every band width, without assuming a tensor factorization.

    theorem staircase_projected_ne_zero (h s : ℕ) :
        sameHighProjection _ _ _ s (staircaseWord (h+s)) ≠ 0 := by
    …

    Mentions: OAI.Saxl.sameHighProjection, OAI.Saxl.staircaseWord