OAI/RepresentationTheory/Saxl/Main.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Saxl.SizedStripChain.of_horizontal line 13
2. lemma OAI.Saxl.StripChain.sized line 18
3. theorem OAI.Saxl.band_cut_support line 28

   Source comment

   Lift the factor support through the exact same-high quotient.

   theorem band_cut_support (h s m : ℕ) (he : h+s=m)
       (ν μ : YoungDiagram) (hν : ν.card = (staircase h).card)
       (t : Tableau (staircase m).card μ) (bs : List ℕ) (hs : SizedStripChain bs ν μ)
       (fh : Representation.IntertwiningMap (spechtRep (canonicalTableau ν hν))
         (staircaseCyclic h).toRepresentation) (hfh : fh ≠ 0)
       (hband : ∀ (η : YoungDiagram) (r : Tableau (bandSize h s) η), η.colLen 0 ≤ bs.length →
         ∃ F : Representation.IntertwiningMap (spechtRep r)
           (cyclic (wordRep _ _) (stairBandWord h s)).toRepresentation, F ≠ 0) :
       ∃ F : Representation.IntertwiningMap (spechtRep t) (staircaseCyclic m).toRepresentation, F ≠ 0 := by
   …

   Mentions: OAI.Saxl.staircase, OAI.Saxl.Tableau, OAI.Saxl.SizedStripChain, OAI.Saxl.spechtRep, OAI.Saxl.canonicalTableau, OAI.Saxl.staircaseCyclic, OAI.Saxl.bandSize, OAI.Saxl.cyclic, OAI.Saxl.wordRep, OAI.Saxl.stairBandWord

4. lemma OAI.Saxl.staircase_one_dominates line 47
5. theorem OAI.Saxl.full_cyclic_support line 58

   Source comment

   Strong induction, including m=1 and every partition of the exact triangular size.

   theorem full_cyclic_support (m : ℕ) (hm : 1 ≤ m) (μ : YoungDiagram)
       (t : Tableau (staircase m).card μ) :
       ∃ F : Representation.IntertwiningMap (spechtRep t) (staircaseCyclic m).toRepresentation, F ≠ 0 := by
   …

   Mentions: OAI.Saxl.Tableau, OAI.Saxl.staircase, OAI.Saxl.spechtRep, OAI.Saxl.staircaseCyclic

6. theorem OAI.Saxl.cyclic_saxl_conjecture line 82

   Source comment

   The strengthened cyclic form of Saxl’s conjecture.

   theorem cyclic_saxl_conjecture : CyclicSaxlConjecture := by
   …

   Mentions: OAI.Saxl.CyclicSaxlConjecture

7. theorem OAI.Saxl.saxl_conjecture line 88

   Source comment

   Every complex staircase tensor square contains all Specht irreducibles of its symmetric group.

   Distinct definitions of this name: ComparatorChallenges/Saxl.lean:112 (same statement text; different proof or body). Qualify references as OAI.Saxl.saxl_conjecture@path.

   theorem saxl_conjecture : SaxlConjecture := saxl_of_cyclic_support cyclic_saxl_conjecture

   Mentions: OAI.Saxl.SaxlConjecture, OAI.Saxl.saxl_of_cyclic_support, OAI.Saxl.cyclic_saxl_conjecture

8. theorem OAI.Saxl.cyclic_saxl line 92
9. theorem OAI.Saxl.saxl_contains_every_irreducible line 96

   Source comment

   Specht classification implies that every finite-dimensional irreducible complex representation embeds in the staircase tensor square.

   theorem saxl_contains_every_irreducible (m : ℕ) (hm : 1 ≤ m)
       {V : Type uV} [AddCommGroup V] [Module ℂ V] [Module.Finite ℂ V]
       (ρ : Representation ℂ (Equiv.Perm (Fin (staircase m).card)) V)
       [Representation.IsIrreducible ρ] :
       ∃ F : Representation.IntertwiningMap ρ
         ((spechtRep (stairTableau m)).tprod (spechtRep (stairTableau m))),
         Function.Injective F := by
   …

   Mentions: OAI.Saxl.staircase, OAI.Saxl.spechtRep, OAI.Saxl.stairTableau

10. theorem OAI.Saxl.saxl_kronecker_pos line 112

    Source comment

    The positive-multiplicity conclusion with the literal triangular degree, rather than the definitionally convenient cell count.

    theorem saxl_kronecker_pos (m : ℕ) (hm : 1 ≤ m) (μ : YoungDiagram)
        (hμ : μ.card = m * (m + 1) / 2) :
        0 < kronecker (canonicalTableau (staircase m) (staircase_card m))
          (canonicalTableau (staircase m) (staircase_card m)) (canonicalTableau μ hμ) := by
    …

    Mentions: OAI.Saxl.kronecker, OAI.Saxl.canonicalTableau, OAI.Saxl.staircase, OAI.Saxl.staircase_card