OAI/RepresentationTheory/Saxl/SignEquivalence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Saxl.transposeTableau line 13
2. def OAI.Saxl.signTwist line 21

   Source comment

   Twisting by the actual sign character, on the same complex vector space.

   def signTwist {n : ℕ} {V : Type uV} [AddCommGroup V] [Module ℂ V]
       (ρ : Representation ℂ (Equiv.Perm (Fin n)) V) :
       Representation ℂ (Equiv.Perm (Fin n)) V where
   …

3. lemma OAI.Saxl.signTwist_irreducible line 28
4. def OAI.Saxl.orbitAverage line 49
5. lemma OAI.Saxl.orbitAverage_base line 71
6. theorem OAI.Saxl.specht_sign_transpose line 91

   Source comment

   Sign-conjugacy proved using the column-antisymmetrized row tabloids.

   theorem specht_sign_transpose {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :
       Nonempty ((spechtRep t).Equiv (signTwist (spechtRep (transposeTableau t)))) := by
   …

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