OAI/RepresentationTheory/YoungSymmetry/Irreducible.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubeShuffle.Specht.rowEquiv line 9
2. def OAI.CubeShuffle.Specht.rowCost line 19
3. lemma OAI.CubeShuffle.Specht.eq_of_row_preserving line 21
4. lemma OAI.CubeShuffle.Specht.column_injective_rowCost line 38
5. lemma OAI.CubeShuffle.Specht.swap_relabel line 56
6. lemma OAI.CubeShuffle.Specht.sign_vector_rowCost line 65

   Source documentation

   A nonzero column-sign vector in another tabloid module forces the usual Young dominance inequality. For inequivalence, the single strictly increasing row-cost is enough: equality forces equality of shapes.

   lemma sign_vector_rowCost (μ ν : YoungDiagram) (e : Cell μ ≃ Cell ν)
       (v : Tabloid ν → ℂ) (hv : v ≠ 0)
       (hs : ∀ c : colGroup μ,
         tabloidRep ν (e.permCongr c) v = permSign (c : Equiv.Perm (Cell μ)) • v) :
       rowCost μ ≤ rowCost ν ∧ (rowCost μ = rowCost ν → μ = ν) := by
   …

   Mentions: OAI.CubeShuffle.Specht.Cell, OAI.CubeShuffle.Specht.Tabloid, OAI.CubeShuffle.Specht.colGroup, OAI.CubeShuffle.Specht.tabloidRep, OAI.CubeShuffle.Specht.permSign, OAI.CubeShuffle.Specht.rowCost

7. lemma OAI.CubeShuffle.Specht.polytabloid_col_action line 90
8. theorem OAI.CubeShuffle.Specht.shapes_eq_of_equivariant_equiv line 96

   Source documentation

   Specht modules of different shapes cannot be equivalent, including after an arbitrary relabeling of the underlying finite sets.

   theorem shapes_eq_of_equivariant_equiv (μ ν : YoungDiagram) (e : Cell μ ≃ Cell ν)
       (T : space μ ≃ₗ[ℂ] space ν)
       (hT : ∀ p v, T (representation μ p v) = representation ν (e.permCongr p) (T v)) :
       μ = ν := by
   …

   Mentions: OAI.CubeShuffle.Specht.Cell, OAI.CubeShuffle.Specht.space, OAI.CubeShuffle.Specht.representation

9. def OAI.CubeShuffle.Specht.cellRowsEquiv line 140
10. lemma OAI.CubeShuffle.Specht.card_eq_sum_rowLen line 147
11. lemma OAI.CubeShuffle.Specht.sum_rowLens line 151
12. def OAI.CubeShuffle.Specht.diagramPartition line 160
13. def OAI.CubeShuffle.Specht.partitionDiagram line 165
14. lemma OAI.CubeShuffle.Specht.partitionDiagram_rowLens line 168
15. lemma OAI.CubeShuffle.Specht.partitionDiagram_card line 174
16. lemma OAI.CubeShuffle.Specht.partitionDiagram_diagramPartition line 179
17. abbrev OAI.CubeShuffle.Specht.Shapes line 188

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:220 (same declaration text).

18. def OAI.CubeShuffle.Specht.shapePartitionEquiv line 190
19. instance OAI.CubeShuffle.Specht.(instance at line 204) line 204
20. def OAI.CubeShuffle.Specht.conjugacyPartition line 206
21. lemma OAI.CubeShuffle.Specht.conjugacyPartition_injective line 210
22. lemma OAI.CubeShuffle.Specht.card_conjugacy_le_shapes line 218
23. def OAI.CubeShuffle.Specht.labels line 223

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:222 (same declaration text).

24. def OAI.CubeShuffle.Specht.labelledRepresentation line 226
25. lemma OAI.CubeShuffle.Specht.labelledRepresentation_irreducible line 230
26. lemma OAI.CubeShuffle.Specht.labelledRepresentation_equiv_shapes line 256
27. theorem OAI.CubeShuffle.Specht.labelled_complete line 279

    Source documentation

    Actual completeness of the polytabloid representations of the full symmetric group.

    theorem labelled_complete {N : ℕ}
        {V : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
        (ρ : Representation ℂ (Equiv.Perm (Fin N)) V) [Representation.IsIrreducible ρ] :
        ∃ μ : Shapes N, Nonempty (Representation.Equiv (labelledRepresentation μ) ρ) := by
    …

    Mentions: OAI.CubeShuffle.Specht.Shapes, OAI.CubeShuffle.Specht.labelledRepresentation