OAI/Algebra/AuslanderReiten/HomComplex/FullHomFunctor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.fullHomCochainEquiv line 16
  2. theorem OAI.ArExplicit.fullHomCochainEquiv_differential line 30
  3. def OAI.ArExplicit.fullHomCocycleMap line 34
  4. theorem OAI.ArExplicit.fullHomCocycleMap_bijective line 41
  5. theorem OAI.ArExplicit.fullHomCocycleMap_boundary line 59
  6. def OAI.ArExplicit.fullHomCohomologyMap line 75
  7. theorem OAI.ArExplicit.fullHomCohomologyMap_mk line 83
  8. theorem OAI.ArExplicit.fullHomCohomologyMap_bijective line 87
  9. def OAI.ArExplicit.fullHomCohomologyEquiv line 100
  10. theorem OAI.ArExplicit.fullHomCohomologyMap_product line 106