SpechtSubmodule.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Saxl.mem_cyclic line 13
lemma OAI.Saxl.cyclic_le line 19
def OAI.Saxl.tabloidSub line 32
Source comment
The actual row-tabloid permutation module, embedded in the word space.
```
def tabloidSub {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :=
…
```
Mentions: OAI.Saxl.Tableau
lemma OAI.Saxl.columnAlt_mem line 35
lemma OAI.Saxl.spechtSub_le_tabloidSub line 44
lemma OAI.Saxl.columnAlt_tabloid line 52
Source comment
The Ferrers shape forces the column antisymmetrizer to have rank one on the row-tabloid module.
```
lemma columnAlt_tabloid {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ)
    {x : WordSpace n (μ.colLen 0)} (hx : x ∈ tabloidSub t) :
    columnAlt t x ∈ Submodule.span ℂ {polytabloid t} := by
…
```
Mentions: OAI.Saxl.Tableau, OAI.Saxl.WordSpace, OAI.Saxl.tabloidSub, OAI.Saxl.columnAlt, OAI.Saxl.polytabloid
lemma OAI.Saxl.wordRep_star line 68
lemma OAI.Saxl.polytabloid_real line 71
lemma OAI.Saxl.cyclic_star line 84
def OAI.Saxl.wordPerm line 101
Source comment
On words, precomposition by a position permutation is a bijection.
```
def wordPerm (n d : ℕ) (g : Equiv.Perm (Fin n)) : Equiv.Perm (Fin n → Fin d) where
…
```
lemma OAI.Saxl.wordPair_move line 107
lemma OAI.Saxl.columnAlt_pair line 113
lemma OAI.Saxl.columnAlt_coefficient line 126
lemma OAI.Saxl.polytabloid_ne_zero line 132
lemma OAI.Saxl.specht_detect line 139
theorem OAI.Saxl.specht_cyclic_of_ne_zero line 164
Source comment
Every nonzero vector in the genuine complex Specht cyclic subspace again generates that whole subspace.
```
theorem specht_cyclic_of_ne_zero {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ)
    {x : WordSpace n (μ.colLen 0)} (hx : x ∈ spechtSub t) (hx0 : x ≠ 0) :
    cyclic (wordRep n (μ.colLen 0)) x = spechtSub t := by
…
```
Mentions: OAI.Saxl.Tableau, OAI.Saxl.WordSpace, OAI.Saxl.spechtSub, OAI.Saxl.cyclic, OAI.Saxl.wordRep

def OAI.Saxl.subrepAmbient line 187

Source comment

Inclusion of a subrepresentation of a subrepresentation into the ambient space.

def subrepAmbient {G : Type uG} {V : Type uV} [Group G] [AddCommGroup V] [Module ℂ V]
    {ρ : Representation ℂ G V} (U : Subrepresentation ρ)
    (S : Subrepresentation U.toRepresentation) : Subrepresentation ρ where
…

theorem OAI.Saxl.specht_irreducible line 196
Source comment
The complex polytabloid module is irreducible.
```
theorem specht_irreducible {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :
    Representation.IsIrreducible (spechtRep t) := by
…
```
Mentions: OAI.Saxl.Tableau, OAI.Saxl.spechtRep