OAI/Analysis/KadisonKastler/PointedWordReduction.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Repeated words in commuting matrix sites

The reduction below is independent of the representation: it gathers each site into one matrix entry and records incompatible matrix indices by zero.

  1. abbrev OAI.KadisonKastler.MatrixSiteLetter line 16
  2. abbrev OAI.KadisonKastler.MatrixSiteWord line 17
  3. def OAI.KadisonKastler.MatrixSiteWord.reindex line 23
  4. def OAI.KadisonKastler.MatrixSiteWord.star line 26
  5. def OAI.KadisonKastler.MatrixSiteWord.indices line 29
  6. theorem OAI.KadisonKastler.MatrixSiteWord.reindex_nil line 31
  7. theorem OAI.KadisonKastler.MatrixSiteWord.reindex_cons line 33
  8. theorem OAI.KadisonKastler.MatrixSiteWord.reindex_append line 36
  9. theorem OAI.KadisonKastler.MatrixSiteWord.reindex_star line 40
  10. def OAI.KadisonKastler.MatrixSiteWord.eval line 46
  11. theorem OAI.KadisonKastler.MatrixSiteWord.eval_nil line 49
  12. theorem OAI.KadisonKastler.MatrixSiteWord.eval_cons line 51
  13. theorem OAI.KadisonKastler.MatrixSiteWord.eval_append line 55
  14. theorem OAI.KadisonKastler.MatrixSiteWord.eval_reindex line 59
  15. theorem OAI.KadisonKastler.MatrixSiteWord.eval_star line 64
  16. def OAI.KadisonKastler.MatrixSiteWord.insert line 79

    Source documentation

    Insert a matrix entry into a word with distinct sites.

    def insert (a : MatrixSiteLetter I) : MatrixSiteWord I → Option (MatrixSiteWord I)
  | [] => some [a]
  | b :: w =>
    if a.1 = b.1 then
      if a.2.2 = b.2.1 then some ((a.1, a.2.1, b.2.2) :: w) else none
    else (insert a w).map (List.cons b)

/-- The canonical distinct-site reduction; `none` denotes zero. -/

    Mentions: OAI.KadisonKastler.MatrixSiteLetter, OAI.KadisonKastler.MatrixSiteWord

  17. def OAI.KadisonKastler.MatrixSiteWord.reduce line 87

    Source documentation

    The canonical distinct-site reduction; none denotes zero.

    def reduce : MatrixSiteWord I → Option (MatrixSiteWord I)
  | [] => some []
  | a :: w => (reduce w).bind (insert a)

    Mentions: OAI.KadisonKastler.MatrixSiteWord, OAI.KadisonKastler.MatrixSiteWord.insert

  18. def OAI.KadisonKastler.MatrixSiteWord.evalOption line 91
  19. theorem OAI.KadisonKastler.MatrixSiteWord.evalOption_map_cons line 95
  20. theorem OAI.KadisonKastler.MatrixSiteWord.evalOption_insert line 101
  21. theorem OAI.KadisonKastler.MatrixSiteWord.evalOption_reduce line 122
  22. theorem OAI.KadisonKastler.MatrixSiteWord.indices_insert_subset line 139
  23. theorem OAI.KadisonKastler.MatrixSiteWord.indices_insert_nodup line 167
  24. theorem OAI.KadisonKastler.MatrixSiteWord.indices_reduce_nodup line 197
  25. def OAI.KadisonKastler.PointedMatrixSites.wordOperator line 221
  26. def OAI.KadisonKastler.PointedMatrixSites.wordVector line 224
  27. theorem OAI.KadisonKastler.PointedMatrixSites.wordOperator_nil line 227
  28. theorem OAI.KadisonKastler.PointedMatrixSites.wordOperator_cons line 228
  29. theorem OAI.KadisonKastler.PointedMatrixSites.wordOperator_append line 231
  30. theorem OAI.KadisonKastler.PointedMatrixSites.wordOperator_star line 234
  31. theorem OAI.KadisonKastler.PointedMatrixSites.wordVector_nil line 237
  32. theorem OAI.KadisonKastler.PointedMatrixSites.wordVector_cons line 238