OAI/Analysis/TracialCohomology/CornerTraces.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Corner traces for bounded Hochschild cohomology.

  1. def OAI.PopaCorner.trace line 25
  2. lemma OAI.PopaCorner.trace_apply line 34
  3. lemma OAI.PopaCorner.trace_faithful line 37
  4. lemma OAI.PopaCorner.trace_tracial line 51
  5. lemma OAI.PopaCorner.trace_one line 56
  6. lemma OAI.PopaCorner.trace_normal line 66
  7. lemma OAI.PopaCorner.corner_diffuse line 73
  8. lemma OAI.PopaCorner.full_center_lift line 91
  9. lemma OAI.PopaCorner.full_corner line 126
  10. lemma OAI.PopaCorner.corner_factor line 157
  11. lemma OAI.PopaCenter.corner_typeII line 176
  12. lemma OAI.PopaCenter.full_corner_center line 198
  13. def OAI.PopaCenter.centerAlgebra line 244
  14. instance OAI.PopaCenter.centerAlgebra_closed line 253
  15. def OAI.PopaCenter.centerCompression line 259
  16. lemma OAI.PopaCenter.centerCompression_injective line 282
  17. lemma OAI.PopaCenter.center_compression_norm line 292
  18. lemma OAI.PopaCenter.full_center_lift_norm line 298
  19. def OAI.PopaCenter.cornerAverage line 320
  20. lemma OAI.PopaCenter.cornerAverage_central line 324
  21. lemma OAI.PopaCenter.central_corner line 329
  22. lemma OAI.PopaCenter.average_cornerAverage line 340
  23. lemma OAI.PopaCenter.cornerAverage_lift line 360
  24. lemma OAI.PopaCenter.average_corner_rank line 374