OAI/Analysis/TracialCohomology/Cohomology.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Cohomology for bounded Hochschild cohomology.

  1. def OAI.BoundedHochschild.differentialLinearMap line 21
  2. def OAI.BoundedHochschild.incomingDifferential line 30
  3. lemma OAI.BoundedHochschild.incomingDifferential_succ line 34
  4. def OAI.BoundedHochschild.cocycles line 37
  5. lemma OAI.BoundedHochschild.mem_cocycles line 40
  6. def OAI.BoundedHochschild.coboundaries line 43
  7. lemma OAI.BoundedHochschild.coboundaries_le_cocycles line 46
  8. def OAI.BoundedHochschild.incomingToCocycles line 56
  9. abbrev OAI.BoundedHochschild.Cohomology line 60
  10. theorem OAI.BoundedHochschild.cohomology_subsingleton_iff line 63