OAI/RepresentationTheory/Saxl/BandPairing.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Saxl.Band.conjugation line 11
2. lemma OAI.Saxl.Band.conjugation_one line 16
3. lemma OAI.Saxl.Band.conjugation_mul line 20
4. lemma OAI.Saxl.Band.conjugation_D line 24
5. lemma OAI.Saxl.Band.conjugation_prod line 32
6. lemma OAI.Saxl.Band.segments_conjugation line 37
7. lemma OAI.Saxl.Band.conjugation_blocks_ne_zero line 55
8. def OAI.Saxl.Path.chainFunctional line 65
9. lemma OAI.Saxl.Path.chainFunctional_pure line 70
10. lemma OAI.Saxl.Path.chainFunctional_column line 73
11. lemma OAI.Saxl.Path.chainFunctional_endpoint line 82
12. lemma OAI.Saxl.Path.fourRow_column_lengths line 90
13. lemma OAI.Saxl.Path.fourRow_tableau_noncancellation line 98
14. theorem OAI.Saxl.Path.fourRow_support line 111

    Source comment

    The actual complex Specht modules with at most four rows occur in the specified two-layer alternating path cyclic module.

    theorem fourRow_support (r : ℕ) (_hr : 2 ≤ r) (μ : YoungDiagram)
        (t : Tableau (2*r+1) μ) (hμ : μ.colLen 0 ≤ 4) :
        ∃ f : Representation.IntertwiningMap (spechtRep t)
          (cyclic (wordRep (2*r+1) 4) (bandWord r)).toRepresentation, f ≠ 0 := by
    …

    Mentions: OAI.Saxl.Tableau, OAI.Saxl.spechtRep, OAI.Saxl.cyclic, OAI.Saxl.wordRep, OAI.Saxl.Path.bandWord

15. lemma OAI.Saxl.PathLayer.J_flip line 132
16. lemma OAI.Saxl.PathLayer.rowAlt_rev_formula line 135
17. theorem OAI.Saxl.PathLayer.paired_rowAlt line 156