OAI/Analysis/TracialCohomology/Corners.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Corners for bounded Hochschild cohomology.

  1. def OAI.PopaCorner.algebra line 20
  2. instance OAI.PopaCorner.algebra_closed line 43
  3. instance OAI.PopaCorner.instOne line 47
  4. instance OAI.PopaCorner.instRing line 48
  5. instance OAI.PopaCorner.instAlgebra line 53
  6. instance OAI.PopaCorner.instNormedRing line 55
  7. instance OAI.PopaCorner.instNormedAlgebra line 58
  8. instance OAI.PopaCorner.instCStarAlgebra line 60
  9. instance OAI.PopaCorner.instStarOrderedRing line 62
  10. def OAI.PopaCorner.incl line 80
  11. lemma OAI.PopaCorner.coe_one line 89
  12. lemma OAI.PopaCorner.incl_apply line 91
  13. def OAI.PopaCorner.compress line 99
  14. lemma OAI.PopaCorner.compress_norm_le line 105
  15. def OAI.PopaCorner.weakSpace line 124
  16. lemma OAI.PopaCorner.weakSpace_closed line 128
  17. def OAI.PopaCorner.strongEquiv line 143
  18. def OAI.PopaCorner.predualEquiv line 157
  19. lemma OAI.PopaCorner.predualEquiv_symm_apply_mk line 162
  20. theorem OAI.PopaCorner.corner_wstar line 176