StripSupport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Saxl.placed_strip_restriction line 13

Source comment

Place the smaller tableau on any chosen block, with the remaining strip colors on its complement. No transitivity or induction rule is assumed.

theorem placed_strip_restriction {n a b : ℕ} {ν μ : YoungDiagram} {bs : List ℕ}
    (hs : SizedStripChain bs ν μ) (s : Tableau a ν) (t : Tableau n μ)
    (e : Fin n ≃ Fin a ⊕ Fin b) :
    ∃ (c : Fin b → Fin bs.length) (F : Specht t →ₗ[ℂ] Specht s), Function.Surjective F ∧
      ∀ (h : Equiv.Perm (Fin a)) (q : Equiv.Perm (Fin b)), c ∘ q = c →
        ∀ x, F (spechtRep t (sumPerm e h q) x) = spechtRep s h (F x) := by
…

Mentions: OAI.Saxl.SizedStripChain, OAI.Saxl.Tableau, OAI.Saxl.Specht, OAI.Saxl.spechtRep, OAI.Saxl.sumPerm

theorem OAI.Saxl.strip_product_support line 76

Source comment

Required support transfer from a genuine iterated horizontal-strip restriction and genuine independent high/band cyclic factors.

theorem strip_product_support {n a b d : ℕ} {ν μ : YoungDiagram} {bs : List ℕ}
    (hs : SizedStripChain bs ν μ) (s : Tableau a ν) (t : Tableau n μ)
    (e : Fin n ≃ Fin a ⊕ Fin b) (v : WordSpace a d) (u : WordSpace b d)
    (A : Fin d → Prop) (hv : v ∈ alphabetSub a d A)
    (hu : u ∈ alphabetSub b d (fun z => ¬A z))
    (f : Representation.IntertwiningMap (spechtRep s) (cyclic (wordRep a d) v).toRepresentation)
    (hf : f ≠ 0)
    (hband : ∀ (η : YoungDiagram) (r : Tableau b η), η.colLen 0 ≤ bs.length →
      ∃ F : Representation.IntertwiningMap (spechtRep r) (cyclic (wordRep b d) u).toRepresentation, F ≠ 0) :
    ∃ F : Representation.IntertwiningMap (spechtRep t)
      (cyclic (wordRep n d) (positionProduct e v u)).toRepresentation, F ≠ 0 := by
…

Mentions: OAI.Saxl.SizedStripChain, OAI.Saxl.Tableau, OAI.Saxl.WordSpace, OAI.Saxl.alphabetSub, OAI.Saxl.spechtRep, OAI.Saxl.cyclic, OAI.Saxl.wordRep, OAI.Saxl.positionProduct