OAI/Analysis/TracialCohomology/SlotHomotopy.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

Slot homotopy for bounded Hochschild cohomology.

  1. def OAI.BoundedHochschild.sliceAt line 25
  2. lemma OAI.BoundedHochschild.sliceAt_apply line 28
  3. def OAI.BoundedHochschild.normalAt line 31
  4. lemma OAI.BoundedHochschild.normalAt_insert line 35
  5. lemma OAI.BoundedHochschild.normalAt_normal line 42
  6. def OAI.BoundedHochschild.slotInsertion line 50
  7. lemma OAI.BoundedHochschild.slotInsertion_apply line 53
  8. lemma OAI.BoundedHochschild.sliceAt_norm line 57
  9. lemma OAI.BoundedHochschild.normalAt_norm line 66
  10. lemma OAI.BoundedHochschild.slotInsertion_norm line 85
  11. lemma OAI.BoundedHochschild.merge_insert_product line 99
  12. lemma OAI.BoundedHochschild.merge_insert_prev line 116
  13. lemma OAI.BoundedHochschild.sliceAt_add line 140
  14. lemma OAI.BoundedHochschild.sliceAt_smul line 143
  15. lemma OAI.BoundedHochschild.sliceAt_sum line 146
  16. lemma OAI.BoundedHochschild.sliceAt_zero line 150
  17. lemma OAI.BoundedHochschild.sliceAt_left line 153
  18. lemma OAI.BoundedHochschild.sliceAt_right line 164
  19. lemma OAI.BoundedHochschild.sliceAt_middle_same line 174
  20. lemma OAI.BoundedHochschild.sliceAt_middle_before line 183
  21. lemma OAI.BoundedHochschild.sliceAt_middle_after line 190
  22. lemma OAI.BoundedHochschild.sliceAt_middle_before_boundary line 197
  23. def OAI.BoundedHochschild.NormalBefore line 206
  24. def OAI.BoundedHochschild.UnitZeroBefore line 209
  25. lemma OAI.BoundedHochschild.projected_left_zero line 212
  26. lemma OAI.BoundedHochschild.projected_middle_before_zero line 222
  27. lemma OAI.BoundedHochschild.projected_middle_boundary line 230
  28. lemma OAI.BoundedHochschild.projected_middle_same line 240
  29. lemma OAI.BoundedHochschild.projected_middle_after line 248
  30. lemma OAI.BoundedHochschild.projected_right line 254
  31. lemma OAI.BoundedHochschild.projected_middle_sum line 263
  32. lemma OAI.BoundedHochschild.slot_cocycle_identity line 300
  33. def OAI.BoundedHochschild.prefixDifferential line 319
  34. lemma OAI.BoundedHochschild.prefixDifferential_apply line 324
  35. def OAI.BoundedHochschild.slotRemainder line 337
  36. def OAI.BoundedHochschild.slotCorrection line 340
  37. lemma OAI.BoundedHochschild.slotCorrection_norm line 343
  38. lemma OAI.BoundedHochschild.slotRemainder_identity line 348
  39. lemma OAI.BoundedHochschild.slotRemainder_cocycle line 354
  40. lemma OAI.BoundedHochschild.slotRemainder_apply line 361
  41. lemma OAI.BoundedHochschild.UnitZeroBefore.apply line 401
  42. lemma OAI.BoundedHochschild.normalAt_preserves_unitZero line 407
  43. lemma OAI.BoundedHochschild.insertion_preserves_unitZero line 421
  44. def OAI.BoundedHochschild.pairSlice line 430
  45. lemma OAI.BoundedHochschild.pairSlice_apply line 434
  46. lemma OAI.BoundedHochschild.pairSlice_flip line 438
  47. lemma OAI.BoundedHochschild.normalAt_pairSlice line 446
  48. lemma OAI.BoundedHochschild.normalAt_retains_factored_slice line 453
  49. lemma OAI.BoundedHochschild.HasPreadjoint.smul line 470
  50. lemma OAI.BoundedHochschild.HasPreadjoint.zero line 477
  51. lemma OAI.BoundedHochschild.HasPreadjoint.sum line 483
  52. lemma OAI.BoundedHochschild.leftCoboundary_before_normal line 493
  53. lemma OAI.BoundedHochschild.middleCoboundary_before_normal line 511
  54. lemma OAI.BoundedHochschild.prefixDifferential_before_normal line 533
  55. lemma OAI.BoundedHochschild.prefix_middle_unit_other line 546
  56. lemma OAI.BoundedHochschild.prefixDifferential_unit line 573
  57. lemma OAI.BoundedHochschild.prefixDifferential_unit_before line 602
  58. lemma OAI.BoundedHochschild.prefixDifferential_unit_at line 607
  59. lemma OAI.BoundedHochschild.normalAt_old_slice line 612
  60. lemma OAI.BoundedHochschild.normalAt_before_normal_of_factors line 638
  61. lemma OAI.BoundedHochschild.insertion_before_normal line 656
  62. lemma OAI.BoundedHochschild.slotRemainder_normal line 668
  63. lemma OAI.BoundedHochschild.slotRemainder_unitZero line 692
  64. theorem OAI.BoundedHochschild.slot_step_of_factors line 711
  65. def OAI.BoundedHochschild.penultimateSlice line 740
  66. lemma OAI.BoundedHochschild.penultimateSlice_apply line 744
  67. lemma OAI.BoundedHochschild.differentialValue_snoc_snoc line 748
  68. theorem OAI.BoundedHochschild.cocycle_last_normal_of_penultimate_normal line 765