Polytabloid.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Saxl.finset_eq_of_signed_sum line 15

Source comment

A finite set is the unique maximizer of its strictly signed separator. Used below for the Ferrers equality case in the Specht submodule theorem.

lemma finset_eq_of_signed_sum {X : Type uX} [DecidableEq X]
    (A B : Finset X) (w : X → ℤ)
    (hp : ∀ x ∈ B, 0 < w x) (hn : ∀ x ∉ B, w x < 0)
    (he : ∑ x ∈ A, w x = ∑ x ∈ B, w x) : A = B := by
…

lemma OAI.Saxl.ferrers_rearrangement line 49
Source comment
A column-injective rearrangement of the canonical row word has precisely Ferrers support. This is the equality-of-margins argument, without using unproved Specht or Young-rule inputs.
```
lemma ferrers_rearrangement {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ)
    (g : Equiv.Perm (Fin n))
    (hinj : Function.Injective (fun i => ((t (g i)).val.1, (t i).val.2))) :
    ∀ i, ((t (g i)).val.1, (t i).val.2) ∈ μ := by
…
```
Mentions: OAI.Saxl.Tableau
def OAI.Saxl.signC line 85
Source comment
The complex-valued sign character.
```
def signC {n : ℕ} : Equiv.Perm (Fin n) →* ℂ :=
…
```
lemma OAI.Saxl.signC_def line 88
lemma OAI.Saxl.signC_inv line 91
lemma OAI.Saxl.signC_mul_self line 94
lemma OAI.Saxl.wordRep_single line 98
def OAI.Saxl.columnAlt line 117
Source comment
Actual column antisymmetrizer on the word-coordinate module.
```
def columnAlt {n d : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :
    Module.End ℂ (WordSpace n d) := by
…
```
Mentions: OAI.Saxl.Tableau, OAI.Saxl.WordSpace
lemma OAI.Saxl.columnAlt_mul line 124
lemma OAI.Saxl.columnAlt_row line 147

lemma OAI.Saxl.column_rearrangement line 152

Source comment

Construction of the witnessing column rearrangement.

lemma column_rearrangement {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ)
    (g : Equiv.Perm (Fin n))
    (hinj : Function.Injective (fun i => ((t (g i)).val.1, (t i).val.2))) :
    ∃ h : columnGroup t, rowWord t ∘ g = rowWord t ∘ (h : Equiv.Perm (Fin n)) := by
…

Mentions: OAI.Saxl.Tableau, OAI.Saxl.columnGroup, OAI.Saxl.rowWord

lemma OAI.Saxl.columnAlt_collision line 175
lemma OAI.Saxl.columnAlt_column line 194
lemma OAI.Saxl.columnAlt_single line 207