SpechtClassification.lean`

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Saxl.rowCellEquiv line 14
Source comment
Rows enumerate exactly the actual cells, including the empty diagram.
```
def rowCellEquiv (μ : YoungDiagram) : μ.cells ≃ (i : Fin (μ.colLen 0)) × Fin (μ.rowLen i) where
…
```
lemma OAI.Saxl.card_eq_sum_rowLens line 22
def OAI.Saxl.partitionDiagram line 35
Source comment
Conversion from Mathlib's partition type to its Young diagram.
```
def partitionDiagram {n : ℕ} (p : Nat.Partition n) : YoungDiagram :=
…
```
lemma OAI.Saxl.partitionDiagram_rowLens line 38
lemma OAI.Saxl.partitionDiagram_card line 44
lemma OAI.Saxl.partitionDiagram_injective line 48
def OAI.Saxl.partitionTableau line 55
def OAI.Saxl.permPartition line 59
Source comment
Cycle-type partition, with only the definitional `card (Fin n)=n` transport.
```
def permPartition {n : ℕ} (g : Equiv.Perm (Fin n)) : Nat.Partition n :=
…
```
lemma OAI.Saxl.isConj_of_permPartition_eq line 62
def OAI.Saxl.classFunctions line 69
Source comment
Class functions on the symmetric group, indexed by cycle type.
```
def classFunctions (n : ℕ) : Submodule ℂ (Equiv.Perm (Fin n) → ℂ) where
…
```
def OAI.Saxl.classEvaluation line 80
Source comment
Select one representative where a cycle partition is realized; unused coordinates are zero. This gives an injection even without surjectivity of cycle-type realization.
```
def classEvaluation (n : ℕ) : (classFunctions n) →ₗ[ℂ] (Nat.Partition n → ℂ) where
…
```
Mentions: OAI.Saxl.classFunctions
lemma OAI.Saxl.classEvaluation_injective line 91
lemma OAI.Saxl.classFunctions_finrank_le line 103
lemma OAI.Saxl.char_mem_classFunctions line 108
def OAI.Saxl.spechtCharacter line 116
Source comment
Character of the actual Specht module as an actual class function.
```
def spechtCharacter {n : ℕ} (p : Nat.Partition n) : classFunctions n :=
…
```
Mentions: OAI.Saxl.classFunctions
def OAI.Saxl.charFunctional line 120
Source comment
Bilinear character scalar product used by the finite-group orthogonality theorem.
```
def charFunctional {G : Type uG} [Group G] [Fintype G] (y : G → ℂ) : (G → ℂ) →ₗ[ℂ] ℂ where
…
```
lemma OAI.Saxl.complex_card_ne_zero line 125
lemma OAI.Saxl.spechtCharacter_orthonormal line 128
lemma OAI.Saxl.spechtCharacter_linearIndependent line 148
lemma OAI.Saxl.spechtCharacter_span line 162
theorem OAI.Saxl.irreducible_equiv_specht line 170
lemma OAI.Saxl.columnAlt_eq_zero_of_rows line 200
theorem OAI.Saxl.specht_rows_of_hom line 232
Source comment
A Specht constituent of a `d`-letter position representation has at most `d` rows, proved by the genuine first-column antisymmetrizer.
```
theorem specht_rows_of_hom {n d : ℕ} {μ : YoungDiagram} (t : Tableau n μ)
    (f : Representation.IntertwiningMap (spechtRep t) (wordRep n d)) (hf : f ≠ 0) :
    μ.colLen 0 ≤ d := by
…
```
Mentions: OAI.Saxl.Tableau, OAI.Saxl.spechtRep, OAI.Saxl.wordRep