OAI/RepresentationTheory/Saxl/BandSupport.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Saxl.stairBandWord line 11
2. def OAI.Saxl.lowPairLetter line 15
3. lemma OAI.Saxl.bandColumn_path_eval' line 19
4. lemma OAI.Saxl.stairBandWord_path_eval line 28
5. theorem OAI.Saxl.twoBand_support line 45

   Source comment

   Every Specht shape with at most four rows occurs in the cyclic module generated by the prescribed two-band vector.

   theorem twoBand_support (h : ℕ) (hh : 1 ≤ h) (μ : YoungDiagram)
       (t : Tableau (bandSize h 2) μ) (hμ : μ.colLen 0 ≤ 4) :
       ∃ f : Representation.IntertwiningMap (spechtRep t)
         (cyclic (wordRep _ _) (stairBandWord h 2)).toRepresentation, f ≠ 0 := by
   …

   Mentions: OAI.Saxl.Tableau, OAI.Saxl.bandSize, OAI.Saxl.spechtRep, OAI.Saxl.cyclic, OAI.Saxl.wordRep, OAI.Saxl.stairBandWord

6. def OAI.Saxl.alphabetSub line 68

   Source comment

   Coordinate subrepresentation using only letters with property A.

   def alphabetSub (n d : ℕ) (A : Fin d → Prop) : Subrepresentation (wordRep n d) where
   …

   Mentions: OAI.Saxl.wordRep

7. lemma OAI.Saxl.alphabetSub_iff line 80
8. lemma OAI.Saxl.cyclic_alphabet line 92
9. lemma OAI.Saxl.single_mem_alphabet line 96
10. lemma OAI.Saxl.altWord_mem_alphabet line 106
11. lemma OAI.Saxl.letterLift_mem_alphabet line 116
12. lemma OAI.Saxl.letterLift_eval line 129
13. lemma OAI.Saxl.letterLift_injective line 142
14. def OAI.Saxl.pairLift line 149
15. lemma OAI.Saxl.pairLift_wordTensor line 154
16. lemma OAI.Saxl.pairLift_injective line 162
17. lemma OAI.Saxl.pairWord_mem_alphabetLeft line 168
18. def OAI.Saxl.shiftedStairWord line 179
19. lemma OAI.Saxl.highLetter_injective line 181
20. lemma OAI.Saxl.shiftedStairWord_support line 188
21. lemma OAI.Saxl.shiftedStairWord_alphabet line 205
22. lemma OAI.Saxl.bandRowWord_alphabet line 215
23. lemma OAI.Saxl.stairBandWord_alphabet line 225
24. theorem OAI.Saxl.staircase_cut_factor line 232

    Source comment

    The actual same-high image factors as the smaller Specht tensor cyclic vector and the exact retained band vector on independent position blocks.

    theorem staircase_cut_factor (h s : ℕ) :
        sameHighProjection _ _ _ s (staircaseWord (h+s)) =
          positionProduct (cutPositions h s) (shiftedStairWord h s) (stairBandWord h s) := by
    …

    Mentions: OAI.Saxl.sameHighProjection, OAI.Saxl.staircaseWord, OAI.Saxl.positionProduct, OAI.Saxl.cutPositions, OAI.Saxl.shiftedStairWord, OAI.Saxl.stairBandWord

25. lemma OAI.Saxl.bandColumnWord_alphabet line 244
26. lemma OAI.Saxl.alphabet_small_invariant line 254
27. lemma OAI.Saxl.oneBand_invariant line 275
28. lemma OAI.Saxl.stairBandWord_ne_zero line 286
29. lemma OAI.Saxl.oneRow_support_invariant line 294
30. theorem OAI.Saxl.oneBand_support line 326

    Source comment

    The width-one band is the genuine trivial constituent required by Pieri.

    theorem oneBand_support (h : ℕ) (μ : YoungDiagram) (t : Tableau (bandSize h 1) μ)
        (hμ : μ.colLen 0 ≤ 1) :
        ∃ f : Representation.IntertwiningMap (spechtRep t)
          (cyclic (wordRep _ _) (stairBandWord h 1)).toRepresentation, f ≠ 0 :=
    …

    Mentions: OAI.Saxl.Tableau, OAI.Saxl.bandSize, OAI.Saxl.spechtRep, OAI.Saxl.cyclic, OAI.Saxl.wordRep, OAI.Saxl.stairBandWord