OAI/Analysis/BoundedHochschild/CornerCochains.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Restriction and extension of cochains along central corners.

  1. def OAI.HochschildAtomic.cornerInclude line 25
  2. def OAI.HochschildAtomic.centralCornerMap line 31
  3. lemma OAI.HochschildAtomic.centralCornerMap_coe line 41
  4. lemma OAI.HochschildAtomic.cornerInclude_coe line 44
  5. lemma OAI.HochschildAtomic.centralCornerMap_norm line 48
  6. lemma OAI.HochschildAtomic.centralCornerMap_mul line 55
  7. lemma OAI.HochschildAtomic.centralCornerMap_left line 62
  8. lemma OAI.HochschildAtomic.centralCornerMap_right line 70
  9. lemma OAI.HochschildAtomic.cornerInclude_left line 77
  10. lemma OAI.HochschildAtomic.cornerInclude_right line 84
  11. def OAI.HochschildAtomic.cornerRestrict line 91
  12. def OAI.HochschildAtomic.cornerExtend line 95
  13. lemma OAI.HochschildAtomic.cornerRestrict_apply line 99
  14. lemma OAI.HochschildAtomic.cornerExtend_apply line 103
  15. lemma OAI.HochschildAtomic.cornerRestrict_norm line 108
  16. lemma OAI.HochschildAtomic.cornerExtend_norm line 113
  17. lemma OAI.HochschildAtomic.merge_corner_include line 121
  18. lemma OAI.HochschildAtomic.merge_corner_map line 129
  19. lemma OAI.HochschildAtomic.differential_cornerRestrict line 136
  20. lemma OAI.HochschildAtomic.differential_cornerExtend line 142
  21. lemma OAI.HochschildAtomic.cornerExtend_support line 148
  22. lemma OAI.HochschildAtomic.cornerExtend_primitive line 154