OAI/RepresentationTheory/Saxl/DominatedQuotient.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Saxl.subrepProject_subtype line 11
2. def OAI.Saxl.wordTensorEquiv line 17
3. def OAI.Saxl.ambientSignMap line 25
4. lemma OAI.Saxl.ambientSignMap_subtype line 33
5. def OAI.Saxl.pairAntiMap line 40
6. lemma OAI.Saxl.pairAntiMap_tensor line 49
7. lemma OAI.Saxl.signed_average_staircase line 59
8. def OAI.Saxl.dominatedQuotient line 82
9. theorem OAI.Saxl.repeatedTarget_in_quotient line 93

   Source comment

   The exact staircase permutation generator occurs in the image of the sign-twisted cyclic staircase module, with no Young-rule input.

   theorem repeatedTarget_in_quotient (m : ℕ)
       (φ : (spechtRep (stairTableau m)).Equiv (signTwist (spechtRep (stairRowTableau m)))) :
       Pi.single (repeatedTarget m) (1:ℂ) ∈ (dominatedQuotient m φ).range := by
   …

   Mentions: OAI.Saxl.spechtRep, OAI.Saxl.stairTableau, OAI.Saxl.signTwist, OAI.Saxl.stairRowTableau, OAI.Saxl.repeatedTarget, OAI.Saxl.dominatedQuotient