OAI/Analysis/BoundedHochschild/Ultrapowers.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Tracial ultrapowers, quotient traces and bounded-ball maps.

  1. def OAI.HochschildUltrapower.ideal line 23
  2. instance OAI.HochschildUltrapower.ideal_twoSided line 35
  3. instance OAI.HochschildUltrapower.ideal_starClosed line 38
  4. instance OAI.HochschildUltrapower.ideal_closed line 41
  5. abbrev OAI.HochschildUltrapower.Ultrapower line 44
  6. instance OAI.HochschildUltrapower.ultrapowerCStar line 46
  7. lemma OAI.HochschildUltrapower.norm_trace_le line 51
  8. def OAI.HochschildUltrapower.sequenceTrace line 60
  9. lemma OAI.HochschildUltrapower.tendsto_sequenceTrace line 62
  10. def OAI.HochschildUltrapower.sequenceTraceLinear line 76
  11. lemma OAI.HochschildUltrapower.sequenceTrace_null line 87
  12. def OAI.HochschildUltrapower.quotientTraceLinear line 94
  13. lemma OAI.HochschildUltrapower.quotientTraceLinear_mk line 98
  14. instance OAI.HochschildUltrapower.ultrapowerOrder line 102
  15. instance OAI.HochschildUltrapower.ultrapowerStarOrder line 105
  16. lemma OAI.HochschildUltrapower.quotientTraceLinear_nonneg line 108
  17. def OAI.HochschildUltrapower.quotientTrace line 118
  18. lemma OAI.HochschildUltrapower.quotientTrace_mk line 122
  19. lemma OAI.HochschildUltrapower.quotientTrace_one line 126
  20. lemma OAI.HochschildUltrapower.quotientTrace_tracial line 133
  21. lemma OAI.HochschildUltrapower.sequenceTrace_star_mul line 142
  22. lemma OAI.HochschildUltrapower.quotientTrace_preGNS_norm line 152
  23. lemma OAI.HochschildUltrapower.quotientTrace_faithful line 171
  24. def OAI.HochschildUltrapower.quotientHom line 189
  25. def OAI.HochschildUltrapower.constantSequence line 195
  26. def OAI.HochschildUltrapower.constant line 204
  27. lemma OAI.HochschildUltrapower.quotientTrace_constant line 207
  28. lemma OAI.HochschildUltrapower.constant_injective line 211
  29. def OAI.HochschildUltrapower.boundedHom line 221
  30. lemma OAI.HochschildUltrapower.boundedHom_apply line 237
  31. lemma OAI.HochschildUltrapower.boundedHom_star line 241
  32. def OAI.HochschildUltrapower.quotientFamily line 248
  33. lemma OAI.HochschildUltrapower.quotientFamily_star line 251
  34. lemma OAI.HochschildUltrapower.quotientFamily_trace_zero line 257
  35. def OAI.HochschildUltrapower.map line 264
  36. lemma OAI.HochschildUltrapower.map_modulus line 268
  37. lemma OAI.HochschildUltrapower.map_asymptotic_identity line 281