Model.lean`

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Saxl.WordSpace line 14
Source comment
Coefficients of position tensors on an alphabet of size `d`.
Also declared: ComparatorChallenges/Saxl.lean:14 (same declaration text), ComparatorChallenges/UniversalTensorSquares.lean:15 (same declaration text).
```
abbrev WordSpace (n d : ℕ) := (Fin n → Fin d) → ℂ
```
def OAI.Saxl.wordRep line 17
Source comment
The position action satisfies `g e_a = e_(a ∘ g⁻¹)`.
Also declared: ComparatorChallenges/Saxl.lean:17 (same declaration text), ComparatorChallenges/UniversalTensorSquares.lean:17 (same declaration text).
```
def wordRep (n d : ℕ) : Representation ℂ (Equiv.Perm (Fin n)) (WordSpace n d) where
…
```
Mentions: OAI.Saxl.WordSpace
def OAI.Saxl.cyclic line 26
Source comment
The cyclic subrepresentation generated by an actual vector.
Also declared: ComparatorChallenges/Saxl.lean:26 (same declaration text), ComparatorChallenges/UniversalTensorSquares.lean:25 (same declaration text).
```
def cyclic {G : Type uG} {V : Type uV} [Group G] [AddCommGroup V] [Module ℂ V]
    (ρ : Representation ℂ G V) (v : V) : Subrepresentation ρ where
…
```
abbrev OAI.Saxl.Tableau line 43
Source comment
A tableau is an enumeration of all cells by the position set.
Also declared: ComparatorChallenges/Saxl.lean:43 (same declaration text), ComparatorChallenges/UniversalTensorSquares.lean:41 (same declaration text).
```
abbrev Tableau (n : ℕ) (μ : YoungDiagram) := Fin n ≃ μ.cells
```
def OAI.Saxl.canonicalTableau line 46
Source comment
One fixed tableau; changing its enumeration gives an isomorphic Specht module.
Also declared: ComparatorChallenges/Saxl.lean:46 (same declaration text), ComparatorChallenges/UniversalTensorSquares.lean:43 (same declaration text).
```
def canonicalTableau {n : ℕ} (μ : YoungDiagram) (hn : μ.card = n) : Tableau n μ :=
…
```
Mentions: OAI.Saxl.Tableau
def OAI.Saxl.rowWord line 50
Source comment
The row word corresponding to the tabloid of a tableau.
Also declared: ComparatorChallenges/Saxl.lean:50 (same declaration text), ComparatorChallenges/UniversalTensorSquares.lean:46 (same declaration text).
```
def rowWord {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) : Fin n → Fin (μ.colLen 0) :=
…
```
Mentions: OAI.Saxl.Tableau
def OAI.Saxl.columnGroup line 55
Source comment
The column permutations of a tableau.
Also declared: ComparatorChallenges/Saxl.lean:55 (same declaration text), ComparatorChallenges/UniversalTensorSquares.lean:50 (same declaration text).
```
def columnGroup {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :
    Subgroup (Equiv.Perm (Fin n)) where
…
```
Mentions: OAI.Saxl.Tableau
def OAI.Saxl.polytabloid line 68
Source comment
The standard column-antisymmetrized row tabloid, with complex coefficients.
Also declared: ComparatorChallenges/Saxl.lean:68 (same declaration text), ComparatorChallenges/UniversalTensorSquares.lean:62 (same declaration text).
```
def polytabloid {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :
    WordSpace n (μ.colLen 0) := by
…
```
Mentions: OAI.Saxl.Tableau, OAI.Saxl.WordSpace
def OAI.Saxl.spechtSub line 78
Source comment
The Specht module, defined as the orbit span of a polytabloid in the row-tabloid permutation module, realized inside the word space.
Also declared: ComparatorChallenges/Saxl.lean:78 (same declaration text), ComparatorChallenges/UniversalTensorSquares.lean:70 (same declaration text).
```
def spechtSub {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :=
…
```
Mentions: OAI.Saxl.Tableau
abbrev OAI.Saxl.Specht line 81
Also declared: ComparatorChallenges/Saxl.lean:81 (same declaration text), ComparatorChallenges/UniversalTensorSquares.lean:73 (same declaration text).
def OAI.Saxl.spechtRep line 85
Source comment
The genuine symmetric-group representation on the complex Specht module.
Also declared: ComparatorChallenges/Saxl.lean:85 (same declaration text), ComparatorChallenges/UniversalTensorSquares.lean:76 (same declaration text).
```
def spechtRep {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :
    Representation ℂ (Equiv.Perm (Fin n)) (Specht t) :=
…
```
Mentions: OAI.Saxl.Tableau, OAI.Saxl.Specht
def OAI.Saxl.kronecker line 91
Source comment
Kronecker multiplicity is the complex dimension of Hom, with the diagonal symmetric-group action on the tensor product.
Also declared: ComparatorChallenges/Saxl.lean:91 (same declaration text), ComparatorChallenges/UniversalTensorSquares.lean:80 (same declaration text).
```
def kronecker {n : ℕ} {α β μ : YoungDiagram}
    (a : Tableau n α) (b : Tableau n β) (t : Tableau n μ) : ℕ :=
…
```
Mentions: OAI.Saxl.Tableau
def OAI.Saxl.staircase line 97
Also declared: ComparatorChallenges/Saxl.lean:97 (same declaration text).
def OAI.Saxl.SaxlConjecture line 107
Also declared: ComparatorChallenges/Saxl.lean:107 (same declaration text).