PieriRestriction.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Saxl.HorizontalStrip line 11
Source comment
A horizontal strip removes at most one cell in each column.
```
def HorizontalStrip (ν μ : YoungDiagram) : Prop :=
…
```
def OAI.Saxl.tableauInclusion line 15
Source comment
Position embedding induced by inclusion of the actual Young diagrams.
```
def tableauInclusion {a n : ℕ} {ν μ : YoungDiagram} (s : Tableau a ν) (t : Tableau n μ)
    (h : ν ≤ μ) : Fin a ↪ Fin n where
…
```
Mentions: OAI.Saxl.Tableau
lemma OAI.Saxl.colLen_mono line 24
def OAI.Saxl.rowLetterInclusion line 30
def OAI.Saxl.wordRestrict line 35
Source comment
Restrict letters on a specified position set, and sum over all other letters. This is precisely contraction with the all-ones functional at deleted positions.
```
def wordRestrict {a n d e : ℕ} (i : Fin a ↪ Fin n) (j : Fin d ↪ Fin e) :
    WordSpace n e →ₗ[ℂ] WordSpace a d where
…
```
Mentions: OAI.Saxl.WordSpace
lemma OAI.Saxl.wordRestrict_single line 55
lemma OAI.Saxl.wordRestrict_equivariant line 66
lemma OAI.Saxl.tableauInclusion_cell line 92
lemma OAI.Saxl.column_fixed_of_strip line 98
lemma OAI.Saxl.strip_contraction_coefficient line 124
lemma OAI.Saxl.column_viaEmbedding line 157
lemma OAI.Saxl.signC_viaEmbedding line 167
lemma OAI.Saxl.strip_contraction_pair line 172

theorem OAI.Saxl.pieri_strip_restriction line 201

Source comment

Positive horizontal-strip Pieri map, equivariant for the full Young subgroup.

theorem pieri_strip_restriction {a n : ℕ} {ν μ : YoungDiagram}
    (s : Tableau a ν) (t : Tableau n μ) (hs : HorizontalStrip ν μ) :
    ∃ F : Specht t →ₗ[ℂ] Specht s, F ≠ 0 ∧
      ∀ (g : Equiv.Perm (Fin n)) (h : Equiv.Perm (Fin a)),
        (∀ k, g (tableauInclusion s t hs.1 k) = tableauInclusion s t hs.1 (h k)) →
        ∀ x, F (spechtRep t g x) = spechtRep s h (F x) := by
…

Mentions: OAI.Saxl.Tableau, OAI.Saxl.HorizontalStrip, OAI.Saxl.Specht, OAI.Saxl.tableauInclusion, OAI.Saxl.spechtRep