OAI/Analysis/TracialCohomology/InteriorHomotopy.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Interior homotopy for bounded Hochschild cohomology.

  1. lemma OAI.BoundedHochschild.firstSliceN_add' line 24
  2. lemma OAI.BoundedHochschild.firstSliceN_smul' line 29
  3. lemma OAI.BoundedHochschild.normalFirst_add' line 34
  4. lemma OAI.BoundedHochschild.normalFirst_smul' line 40
  5. def OAI.BoundedHochschild.normalFirstCLM line 46
  6. lemma OAI.BoundedHochschild.normalFirstCLM_apply line 53
  7. def OAI.BoundedHochschild.normalSecond line 56
  8. lemma OAI.BoundedHochschild.normalSecond_cons line 59
  9. def OAI.BoundedHochschild.secondInsertion line 63
  10. lemma OAI.BoundedHochschild.secondInsertion_cons line 67
  11. def OAI.BoundedHochschild.secondRemainder line 71
  12. lemma OAI.BoundedHochschild.secondRemainder_identity line 74
  13. lemma OAI.BoundedHochschild.secondRemainder_cocycle line 81
  14. lemma OAI.BoundedHochschild.normalSecond_norm line 86
  15. lemma OAI.BoundedHochschild.differentialValue_cons_cons line 95
  16. lemma OAI.BoundedHochschild.normalSecond_cocycle_identity line 117
  17. lemma OAI.BoundedHochschild.secondRemainder_apply line 152
  18. lemma OAI.BoundedHochschild.secondInsertion_norm line 170
  19. lemma OAI.BoundedHochschild.firstNormalRemainderN_one line 193
  20. lemma OAI.BoundedHochschild.normalSecond_first_one line 199
  21. lemma OAI.BoundedHochschild.secondInsertion_first_one line 213
  22. lemma OAI.BoundedHochschild.secondRemainder_first_one line 218
  23. lemma OAI.BoundedHochschild.secondRemainder_second_one line 227
  24. def OAI.BoundedHochschild.firstSliceCLM line 245
  25. lemma OAI.BoundedHochschild.firstSliceCLM_apply line 258
  26. def OAI.BoundedHochschild.firstTwoSlice line 261
  27. lemma OAI.BoundedHochschild.firstTwoSlice_apply line 264
  28. lemma OAI.BoundedHochschild.firstTwoSlice_flip line 269
  29. lemma OAI.BoundedHochschild.normalSecond_first_slice line 274
  30. lemma OAI.BoundedHochschild.normalSecond_second_normal line 282
  31. lemma OAI.BoundedHochschild.normalSecond_first_normal_factored line 293
  32. lemma OAI.BoundedHochschild.secondInsertion_first_slice line 309
  33. lemma OAI.BoundedHochschild.HasPreadjoint.add line 316
  34. lemma OAI.BoundedHochschild.HasPreadjoint.sub line 325
  35. lemma OAI.BoundedHochschild.HasPreadjoint.comp line 334
  36. lemma OAI.BoundedHochschild.secondRemainder_first_normal line 341
  37. lemma OAI.BoundedHochschild.secondRemainder_second_normal line 364
  38. theorem OAI.BoundedHochschild.second_slot_step_of_factors line 388