OAI/Analysis/BoundedHochschild/MatrixCommutants.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Matrix coefficients, commutant algebras and their preduals.

  1. def OAI.HochschildMatrixSystems.MatrixSystem.commutant line 39
  2. lemma OAI.HochschildMatrixSystems.MatrixSystem.mem_commutant line 51
  3. instance OAI.HochschildMatrixSystems.MatrixSystem.commutant_closed line 53
  4. def OAI.HochschildMatrixSystems.MatrixSystem.coefficient line 60
  5. lemma OAI.HochschildMatrixSystems.MatrixSystem.entry_mul_coefficient line 62
  6. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_mul_entry line 68
  7. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_mem line 74
  8. lemma OAI.HochschildMatrixSystems.MatrixSystem.reconstruct line 78
  9. lemma OAI.HochschildMatrixSystems.MatrixSystem.factor_of_commutant line 81
  10. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_star line 98
  11. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_nil line 102
  12. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_diagonal_base line 105
  13. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_corner line 108
  14. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_mul line 112
  15. lemma OAI.HochschildMatrixSystems.MatrixSystem.diagonal_proj line 136
  16. lemma OAI.HochschildMatrixSystems.MatrixSystem.inflate_projection line 142
  17. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_recover line 150
  18. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_of_commutant line 157
  19. lemma OAI.HochschildMatrixSystems.MatrixSystem.commutant_no_minimal line 186
  20. lemma OAI.HochschildMatrixSystems.MatrixSystem.commutantClosure_eq line 240
  21. def OAI.HochschildMatrixSystems.MatrixSystem.commutantPredual line 261
  22. instance OAI.HochschildMatrixSystems.MatrixSystem.(instance at line 262) line 262
  23. instance OAI.HochschildMatrixSystems.MatrixSystem.(instance at line 264) line 264
  24. instance OAI.HochschildMatrixSystems.MatrixSystem.(instance at line 266) line 266
  25. def OAI.HochschildMatrixSystems.MatrixSystem.subalgebraIsoOfEq line 269
  26. def OAI.HochschildMatrixSystems.MatrixSystem.commutantPredualEquiv line 273
  27. lemma OAI.HochschildMatrixSystems.MatrixSystem.subalgebraIsoOfEq_coe line 277
  28. lemma OAI.HochschildMatrixSystems.MatrixSystem.subalgebraIsoOfEq_symm_coe line 282
  29. lemma OAI.HochschildMatrixSystems.MatrixSystem.commutantPredualEquiv_symm_mk line 287
  30. def OAI.HochschildMatrixSystems.MatrixSystem.commutantTrace line 297
  31. lemma OAI.HochschildMatrixSystems.MatrixSystem.commutantTrace_normal line 301
  32. lemma OAI.HochschildMatrixSystems.MatrixSystem.commutantTrace_one line 308
  33. lemma OAI.HochschildMatrixSystems.MatrixSystem.commutantTrace_tracial line 309
  34. lemma OAI.HochschildMatrixSystems.MatrixSystem.commutantTrace_faithful line 311