OAI/RepresentationTheory/Saxl/SizedStrips.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.Saxl.SizedStripChain line 11
2. lemma OAI.Saxl.SizedStripChain.le line 16
3. abbrev OAI.Saxl.shapeTableau line 21
4. lemma OAI.Saxl.tableauInclusion_self line 23
5. theorem OAI.Saxl.stripChain_restriction line 31

   Source comment

   Iterated positive Pieri, with an explicit coloring of the added strips. The map is surjective and equivariant for all permutations preserving each strip, not just for the smaller symmetric group.

   theorem stripChain_restriction {bs ν μ} (hs : SizedStripChain bs ν μ) :
       ∃ (c : Fin μ.card → ℕ) (F : Specht (shapeTableau μ) →ₗ[ℂ] Specht (shapeTableau ν)),
         Function.Surjective F ∧
         (∀ i, c i ≤ bs.length) ∧
         (∀ i, c i = 0 ↔ i ∈ Set.range (tableauInclusion (shapeTableau ν) (shapeTableau μ) hs.le)) ∧
         (∀ j (hj : j < bs.length), (Finset.univ.filter (fun i => c i = j+1)).card = bs[j]) ∧
         (∀ (g : Equiv.Perm (Fin μ.card)) (h : Equiv.Perm (Fin ν.card)),
           (∀ i, c (g i) = c i) →
           (∀ k, g (tableauInclusion (shapeTableau ν) (shapeTableau μ) hs.le k) =
             tableauInclusion (shapeTableau ν) (shapeTableau μ) hs.le (h k)) →
           ∀ x, F (spechtRep (shapeTableau μ) g x) = spechtRep (shapeTableau ν) h (F x)) := by
   …

   Mentions: OAI.Saxl.SizedStripChain, OAI.Saxl.Specht, OAI.Saxl.shapeTableau, OAI.Saxl.tableauInclusion, OAI.Saxl.spechtRep

6. theorem OAI.Saxl.stripChain_restriction_any line 118