OAI/RepresentationTheory/Saxl/ColumnContraction.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Saxl.Columns.Cells line 11

    Source comment

    A concrete ordered disjoint union of consecutive columns.
    @[reducible] def Cells : List ℕ → Type
  | [] => Empty
  | r :: rs => Fin r ⊕ Cells rs
  2. instance OAI.Saxl.Columns.cellsFintype line 15
  3. instance OAI.Saxl.Columns.cellsDecEq line 19
  4. def OAI.Saxl.Columns.row line 23
  5. def OAI.Saxl.Columns.col line 27
  6. def OAI.Saxl.Columns.enumerate line 31
  7. lemma OAI.Saxl.Columns.enumerate_left line 35
  8. lemma OAI.Saxl.Columns.enumerate_right line 40
  9. def OAI.Saxl.Columns.Perms line 45
  10. instance OAI.Saxl.Columns.permsFintype line 49
  11. def OAI.Saxl.Columns.perm line 53
  12. def OAI.Saxl.Columns.sg line 57
  13. lemma OAI.Saxl.Columns.sign_perm line 61
  14. lemma OAI.Saxl.Columns.perm_col line 71
  15. lemma OAI.Saxl.Columns.coords_injective line 80
  16. lemma OAI.Saxl.Columns.coords_range line 102
  17. def OAI.Saxl.Columns.chain line 130

    Source comment

    The matrix product indexed by the actual consecutive position order.
    def chain (rs : List ℕ) (p : ℕ) (N : ℕ → Band.Mat) (π : Perms rs) : Band.Mat :=
…

    Mentions: OAI.Saxl.Band.Mat, OAI.Saxl.Columns.Perms

  18. lemma OAI.Saxl.Columns.chain_cons line 133
  19. def OAI.Saxl.Columns.segments line 153

    Source comment

    Ordered product of independent alternating column segments.
    def segments : ℕ → List ℕ → (ℕ → Band.Mat) → Band.Mat
  | _, [], _ => 1
  | p, r :: rs, N =>
      (∑ π : Equiv.Perm (Fin r), (((Equiv.Perm.sign π : ℤ) : ℂ)) •
        (List.ofFn fun i : Fin r => Band.D (p + i.val) (N (π i).val)).prod) *
      segments (p+r) rs N

/- Factorization over independent column permutations, without commuting factors. -/

    Mentions: OAI.Saxl.Band.Mat, OAI.Saxl.Band.D

  20. lemma OAI.Saxl.Columns.sum_chain line 161

    Source comment

    Factorization over independent column permutations, without commuting factors.
    lemma sum_chain (rs : List ℕ) (p : ℕ) (N : ℕ → Band.Mat) :
    (∑ π : Perms rs, sg π • chain rs p N π) = segments p rs N := by
…

    Mentions: OAI.Saxl.Band.Mat, OAI.Saxl.Columns.Perms, OAI.Saxl.Columns.sg, OAI.Saxl.Columns.chain, OAI.Saxl.Columns.segments

  21. lemma OAI.Saxl.Columns.perm_injective line 169
  22. lemma OAI.Saxl.Columns.perm_surjective line 183
  23. def OAI.Saxl.Columns.toYoung line 204

    Source comment

    The column-recursive coordinates enumerate the actual Ferrers cells.
    def toYoung (μ : YoungDiagram) : Cells μ.transpose.rowLens ≃ μ.cells := by
…

    Mentions: OAI.Saxl.Columns.Cells

  24. lemma OAI.Saxl.Columns.toYoung_val line 220
  25. lemma OAI.Saxl.Columns.row_lt line 223
  26. def OAI.Saxl.Columns.columnTableau line 228
  27. lemma OAI.Saxl.Columns.columnTableau_val line 231
  28. def OAI.Saxl.Columns.columnPerm line 235
  29. lemma OAI.Saxl.Columns.columnPerm_bijective line 243
  30. def OAI.Saxl.Columns.columnEquiv line 263
  31. lemma OAI.Saxl.Columns.columnPerm_sign line 266
  32. lemma OAI.Saxl.Columns.mapped_columnTableau line 272