OAI/Algebra/AuslanderReiten/Cones/MappingConeTotal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.coneBlockShortComplex line 20
  2. def OAI.ArExplicit.coneShortComplexIso line 33
  3. theorem OAI.ArExplicit.cochain_adjacent_exact line 44
  4. theorem OAI.ArExplicit.cochain_adjacent_dualExact line 52
  5. theorem OAI.ArExplicit.mappingCone_exactProjective line 60
  6. theorem OAI.ArExplicit.mappingCone_dualExact line 80
  7. theorem OAI.ArExplicit.mappingCone_totallyAcyclic line 90
  8. theorem OAI.ArExplicit.mappingCone_cokernel_gorenstein line 96