OAI/Algebra/AuslanderReiten/Triangular/TriangularCrossHom.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.TriangularInduction.crossHomAdd line 22
  2. theorem OAI.ArExplicit.TriangularInduction.crossHomAdd_source line 36
  3. theorem OAI.ArExplicit.TriangularInduction.crossHomAdd_target line 43
  4. abbrev OAI.ArExplicit.TriangularInduction.tensorCochain line 52
  5. def OAI.ArExplicit.TriangularInduction.crossCochainEquiv line 57
  6. theorem OAI.ArExplicit.TriangularInduction.crossCochainEquiv_v line 75
  7. theorem OAI.ArExplicit.TriangularInduction.crossCochainEquiv_differential line 79
  8. def OAI.ArExplicit.TriangularInduction.crossFullHomEquivalence line 100
  9. def OAI.ArExplicit.TriangularInduction.crossCohomologyEquiv line 105
  10. def OAI.ArExplicit.TriangularInduction.crossChainMap line 112
  11. theorem OAI.ArExplicit.TriangularInduction.crossChainMap_ofHom line 122
  12. theorem OAI.ArExplicit.TriangularInduction.crossCochainEquiv_source line 130
  13. theorem OAI.ArExplicit.TriangularInduction.crossCochainEquiv_target line 141