OAI/RepresentationTheory/Saxl/ShapeRigidity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Saxl.tableau_image line 13
2. lemma OAI.Saxl.tableau_sum line 22
3. def OAI.Saxl.rowMoment line 31

   Source comment

   Zero-based row-index statistic of a partition.

   def rowMoment (μ : YoungDiagram) : ℤ := ∑ c ∈ μ.cells, (c.1 : ℤ)

4. lemma OAI.Saxl.finset_signed_sum_le line 33
5. lemma OAI.Saxl.mixed_moment_le line 48
6. lemma OAI.Saxl.mixed_support_eq line 70
7. lemma OAI.Saxl.rowLen_eq_count line 93
8. lemma OAI.Saxl.shapes_eq_of_mixed line 106
9. lemma OAI.Saxl.columnAlt_polytabloid_ne_zero line 126
10. lemma OAI.Saxl.mixed_injective_of_columnAlt_ne_zero line 137
11. def OAI.Saxl.columnOperator line 165

    Source comment

    The column operator on any genuine representation of the same group.

    def columnOperator {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ)
        {V : Type uV} [AddCommGroup V] [Module ℂ V]
        (ρ : Representation ℂ (Equiv.Perm (Fin n)) V) : Module.End ℂ V := by
    …

    Mentions: OAI.Saxl.Tableau

12. lemma OAI.Saxl.columnOperator_intertwining line 172
13. lemma OAI.Saxl.columnOperator_subtype line 182
14. lemma OAI.Saxl.mixed_injective_of_equiv line 190
15. theorem OAI.Saxl.specht_shape_rigidity line 211

    Source comment

    Distinct genuine complex Specht shapes are inequivalent.

    theorem specht_shape_rigidity {n : ℕ} {μ ν : YoungDiagram}
        (t : Tableau n μ) (u : Tableau n ν)
        (e : Representation.Equiv (spechtRep t) (spechtRep u)) : μ = ν := by
    …

    Mentions: OAI.Saxl.Tableau, OAI.Saxl.spechtRep