OAI/Algebra/AuslanderReiten/Complete/CompleteNullhomotopy.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ArExplicit.CompleteComparison.comm_linear line 17
  2. structure OAI.ArExplicit.CompleteComparison.UpHomPair line 21
  3. theorem OAI.ArExplicit.CompleteComparison.exists_upHomStep line 27
  4. def OAI.ArExplicit.CompleteComparison.upHomSequence line 38
  5. theorem OAI.ArExplicit.CompleteComparison.upHomSequence_succ_lo line 44
  6. structure OAI.ArExplicit.CompleteComparison.DownHomPair line 49
  7. theorem OAI.ArExplicit.CompleteComparison.exists_downHomStep line 56
  8. def OAI.ArExplicit.CompleteComparison.downHomSequence line 72
  9. theorem OAI.ArExplicit.CompleteComparison.downHomSequence_succ_hi line 79
  10. def OAI.ArExplicit.CompleteComparison.homComponents line 84
  11. theorem OAI.ArExplicit.CompleteComparison.nullhomotopy_from_pairs_with_initial line 100
  12. theorem OAI.ArExplicit.CompleteComparison.nullhomotopy_of_initial_with_component line 153
  13. theorem OAI.ArExplicit.CompleteComparison.nullhomotopy_of_initial line 174
  14. theorem OAI.ArExplicit.CompleteComparison.nullhomotopy_of_cokernel_zero line 182
  15. theorem OAI.ArExplicit.CompleteComparison.nullhomotopy_of_factorization line 197
  16. theorem OAI.ArExplicit.CompleteComparison.factorization_of_nullhomotopy line 217
  17. theorem OAI.ArExplicit.CompleteComparison.nullhomotopy_iff_stable_zero line 233