OAI/Analysis/BoundedHochschild/CentralHomotopy.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

The Hochschild differential and homotopies for central idempotents.

  1. def OAI.BoundedHochschild.centralCut line 27
  2. lemma OAI.BoundedHochschild.centralCut_apply line 30
  3. lemma OAI.BoundedHochschild.norm_centralCut_le line 33
  4. lemma OAI.BoundedHochschild.central_mul_assoc line 43
  5. lemma OAI.BoundedHochschild.central_idempotent_mul line 46
  6. lemma OAI.BoundedHochschild.mergeInputs_central line 50
  7. theorem OAI.BoundedHochschild.differential_centralCut line 59
  8. lemma OAI.BoundedHochschild.centralCut_cocycle line 67
  9. def OAI.BoundedHochschild.leftCoboundary line 82
  10. lemma OAI.BoundedHochschild.leftCoboundary_apply line 86
  11. def OAI.BoundedHochschild.rightCoboundary line 89
  12. lemma OAI.BoundedHochschild.rightCoboundary_apply line 92
  13. def OAI.BoundedHochschild.middleCoboundary line 95
  14. lemma OAI.BoundedHochschild.middleCoboundary_apply line 100
  15. def OAI.BoundedHochschild.differential line 132
  16. theorem OAI.BoundedHochschild.differential_apply line 137
  17. def OAI.BoundedHochschild.tupleInsert line 151
  18. lemma OAI.BoundedHochschild.tupleInsert_eq line 155
  19. lemma OAI.BoundedHochschild.tupleInsert_lt line 171
  20. lemma OAI.BoundedHochschild.tupleInsert_gt line 177
  21. lemma OAI.BoundedHochschild.merge_insert_same line 184
  22. lemma OAI.BoundedHochschild.merge_insert_before line 198
  23. lemma OAI.BoundedHochschild.merge_insert_after line 212
  24. lemma OAI.BoundedHochschild.tail_insert line 227
  25. lemma OAI.BoundedHochschild.init_insert line 237
  26. lemma OAI.BoundedHochschild.last_insert line 244
  27. def OAI.BoundedHochschild.centralJTerm line 258
  28. lemma OAI.BoundedHochschild.centralJTerm_apply line 264
  29. def OAI.BoundedHochschild.centralJ line 274
  30. lemma OAI.BoundedHochschild.norm_centralJTerm_le line 277
  31. lemma OAI.BoundedHochschild.norm_centralJ_le line 298
  32. lemma OAI.BoundedHochschild.centralJ_range line 310
  33. lemma OAI.BoundedHochschild.centralJTerm_eq_zero_lt line 315
  34. lemma OAI.BoundedHochschild.centralJTerm_eq_zero_gt line 323
  35. lemma OAI.BoundedHochschild.centralJ_first_q line 333
  36. lemma OAI.BoundedHochschild.centralJ_all_z line 355
  37. lemma OAI.BoundedHochschild.centralJ_merge_before line 376
  38. lemma OAI.BoundedHochschild.centralJ_merge_after line 403
  39. lemma OAI.BoundedHochschild.centralJ_merge_boundary line 430
  40. lemma OAI.BoundedHochschild.centralJ_inner_cancellation line 453
  41. lemma OAI.BoundedHochschild.centralJ_left_cancellation line 475
  42. lemma OAI.BoundedHochschild.centralJ_right_cancellation line 506
  43. lemma OAI.BoundedHochschild.differential_centralJ_first_q line 536
  44. lemma OAI.BoundedHochschild.differential_centralJ_all_z line 560
  45. theorem OAI.BoundedHochschild.differential_centralJ line 577
  46. theorem OAI.BoundedHochschild.central_cocycle_correction line 639