OAI/Analysis/FactorGeneration/MatrixAlgebras.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Equal-trace finite partitions extend to actual matrix units in the same factor. The theorem also retains a prescribed corner as the sum of diagonals.

  1. theorem OAI.Generator.Tracial.exists_matrixUnits_for_partition line 24
  2. def OAI.Generator.MatrixUnitSystem.concreteHom line 75
  3. def OAI.Generator.MatrixUnitSystem.concreteAlgebra line 78
  4. theorem OAI.Generator.MatrixUnitSystem.concreteAlgebra_le line 80
  5. theorem OAI.Generator.MatrixUnitSystem.mem_concreteAlgebra line 84
  6. instance OAI.Generator.MatrixUnitSystem.concrete_finiteDimensional line 92
  7. def OAI.Generator.MatrixUnitSystem.wotLinearMap line 97
  8. theorem OAI.Generator.MatrixUnitSystem.concreteAlgebra_wotClosed line 100
  9. theorem OAI.Generator.MatrixUnitSystem.concreteHom_injective line 113
  10. theorem OAI.Generator.Tracial.exists_matrixAlgebra_for_unit_partition line 120
  11. def OAI.Generator.MatrixUnitSystem.relativeStar line 154
  12. theorem OAI.Generator.MatrixUnitSystem.relativeStar_mem line 163
  13. theorem OAI.Generator.MatrixUnitSystem.relativeStar_bicommutant line 171
  14. def OAI.Generator.MatrixUnitSystem.relativeVonNeumann line 186
  15. theorem OAI.Generator.MatrixUnitSystem.relativeVonNeumann_le line 190
  16. def OAI.Generator.MatrixUnitSystem.relativeEquiv line 194
  17. theorem OAI.Generator.MatrixUnitSystem.relative_scalar_center line 205
  18. theorem OAI.Generator.MatrixUnitSystem.relative_diffuse line 222
  19. theorem OAI.Generator.MatrixUnitSystem.commute_mapped_of_amplify line 253
  20. theorem OAI.Generator.MatrixUnitSystem.relative_inclusion line 271
  21. theorem OAI.Generator.MatrixUnitSystem.relative_irreducible line 278
  22. theorem OAI.Generator.Bell.char_sum line 310
  23. theorem OAI.Generator.Bell.char_star line 316
  24. def OAI.Generator.Bell.projection line 320
  25. theorem OAI.Generator.Bell.projection_star line 324
  26. theorem OAI.Generator.Bell.projection_mul line 331
  27. theorem OAI.Generator.Bell.projection_total line 377
  28. def OAI.Generator.Bell.leftEntry line 405

    Source documentation

    The matrix unit in the first tensor factor, with identity on the second.

    def leftEntry (i j : ZMod n) : Matrix (ZMod n × ZMod n) (ZMod n × ZMod n) ℂ :=
…
  29. theorem OAI.Generator.Bell.mul_leftEntry line 408
  30. theorem OAI.Generator.Bell.projection_sandwich line 416
  31. theorem OAI.Generator.MatrixUnitSystem.trace_diagonal_eq line 467
  32. theorem OAI.Generator.MatrixUnitSystem.trace_off_diagonal line 471
  33. theorem OAI.Generator.MatrixUnitSystem.trace_diagonal line 475
  34. theorem OAI.Generator.MatrixUnitSystem.trace_hom line 488
  35. theorem OAI.Generator.MatrixUnitSystem.product_hom_leftEntry line 514
  36. def OAI.Generator.MatrixUnitSystem.bellPiece line 527
  37. theorem OAI.Generator.MatrixUnitSystem.bellPiece_orthogonal line 536
  38. theorem OAI.Generator.MatrixUnitSystem.bellPiece_total line 541
  39. def OAI.Generator.MatrixUnitSystem.bellPartition line 546
  40. theorem OAI.Generator.MatrixUnitSystem.bellPiece_sandwich_entry line 555
  41. theorem OAI.Generator.MatrixUnitSystem.bellPartition_pinch_entry line 563
  42. theorem OAI.Generator.MatrixUnitSystem.bellPartition_pinch_algebra line 578