OAI/RepresentationTheory/Saxl/StaircaseTensor.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Saxl.splitLeft line 10
  2. def OAI.Saxl.splitRight line 13
  3. def OAI.Saxl.mergeWords line 16
  4. lemma OAI.Saxl.splitLeft_merge line 19
  5. lemma OAI.Saxl.splitRight_merge line 21
  6. lemma OAI.Saxl.merge_split line 23
  7. def OAI.Saxl.wordUncurry line 28
  8. def OAI.Saxl.wordTensor line 38

    Source comment

    Tensor regrouping by positions.
    def wordTensor (n d e : ℕ) :
    WordSpace n d ⊗[ℂ] WordSpace n e ≃ₗ[ℂ] WordSpace n (d*e) :=
…

    Mentions: OAI.Saxl.WordSpace

  9. lemma OAI.Saxl.wordTensor_tmul line 42
  10. lemma OAI.Saxl.wordTensor_equivariant line 48
  11. def OAI.Saxl.wordTensorIntertwiner line 62
  12. def OAI.Saxl.staircaseSwap line 75

    Source comment

    Transposition is an honest permutation of the self-conjugate staircase.
    def staircaseSwap (m : ℕ) : (staircase m).cells ≃ (staircase m).cells where
…

    Mentions: OAI.Saxl.staircase

  13. abbrev OAI.Saxl.stairTableau line 85
  14. def OAI.Saxl.stairRowTableau line 88
  15. def OAI.Saxl.staircaseWord line 91
  16. def OAI.Saxl.staircaseCyclic line 94
  17. def OAI.Saxl.spechtInclusion line 98
  18. def OAI.Saxl.staircaseTensorMap line 103
  19. lemma OAI.Saxl.staircaseTensorMap_injective line 109
  20. lemma OAI.Saxl.staircaseCyclic_le_tensorRange line 115