OAI/RepresentationTheory/Saxl/StaircaseSign.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Saxl.rowReversalCell line 13
2. lemma OAI.Saxl.rowReversalCell_involutive line 19
3. def OAI.Saxl.rowReversalEquiv line 28
4. def OAI.Saxl.rowReversal line 31
5. def OAI.Saxl.repeatedTarget line 38
6. lemma OAI.Saxl.repeatedTarget_fixed line 41
7. lemma OAI.Saxl.repeated_letters_injective line 47
8. lemma OAI.Saxl.repeated_complement line 58
9. theorem OAI.Saxl.staircase_repeated_projection line 70
10. lemma OAI.Saxl.staircase_repeated_projection_nonzero line 80
11. theorem OAI.Saxl.staircase_sign_equiv line 97
12. lemma OAI.Saxl.alternating_specht_line line 159
13. def OAI.Saxl.rowAverage line 180
14. lemma OAI.Saxl.rowAverage_nonzero line 186
15. lemma OAI.Saxl.rowAverage_fixed line 202
16. lemma OAI.Saxl.signEquiv_rowAverage line 212
17. def OAI.Saxl.signTwistMap line 231
18. def OAI.Saxl.tensorAnti line 243

    Source comment

    A sign intertwiner in the second factor twists the diagonal product.

    def tensorAnti {n : ℕ} {X : Type uX} {Y : Type uY} {Z : Type uZ} [AddCommGroup X] [Module ℂ X]
        [AddCommGroup Y] [Module ℂ Y] [AddCommGroup Z] [Module ℂ Z]
        (ρ : Representation ℂ (Equiv.Perm (Fin n)) X)
        {σ : Representation ℂ (Equiv.Perm (Fin n)) Y} {τ : Representation ℂ (Equiv.Perm (Fin n)) Z}
        (f : Representation.IntertwiningMap σ (signTwist τ)) :
        Representation.IntertwiningMap (signTwist (ρ.tprod σ)) (ρ.tprod τ) where
    …

    Mentions: OAI.Saxl.signTwist