OAI/Algebra/AuslanderReiten/Complete/CompleteComparison.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ArExplicit.ExactProjectiveComplex line 16
  2. structure OAI.ArExplicit.TotallyAcyclicComplex line 22
  3. theorem OAI.ArExplicit.ExactProjectiveComplex.exactAt_of_indices line 26
  4. theorem OAI.ArExplicit.TotallyAcyclicComplex.dualExact_of_indices line 34
  5. theorem OAI.ArExplicit.CompleteComparison.differential_comp line 46
  6. abbrev OAI.ArExplicit.CompleteComparison.Cokernel line 50
  7. structure OAI.ArExplicit.CompleteComparison.UpPair line 53
  8. theorem OAI.ArExplicit.CompleteComparison.exists_upStep line 58
  9. def OAI.ArExplicit.CompleteComparison.upSequence line 71
  10. theorem OAI.ArExplicit.CompleteComparison.upSequence_succ_lo line 76
  11. structure OAI.ArExplicit.CompleteComparison.DownPair line 81
  12. theorem OAI.ArExplicit.CompleteComparison.exists_downStep line 87
  13. def OAI.ArExplicit.CompleteComparison.downSequence line 103
  14. theorem OAI.ArExplicit.CompleteComparison.downSequence_succ_hi line 108
  15. theorem OAI.ArExplicit.CompleteComparison.exists_downStart line 113
  16. def OAI.ArExplicit.CompleteComparison.components line 125
  17. def OAI.ArExplicit.CompleteComparison.fromPairs line 131
  18. theorem OAI.ArExplicit.CompleteComparison.lift_cokernels line 160
  19. def OAI.ArExplicit.CompleteComparison.cokernelMap line 172
  20. theorem OAI.ArExplicit.CompleteComparison.cokernelMap_mkQ line 181
  21. theorem OAI.ArExplicit.CompleteComparison.cokernelMap_id line 187
  22. theorem OAI.ArExplicit.CompleteComparison.cokernelMap_comp line 194
  23. theorem OAI.ArExplicit.CompleteComparison.cokernelMap_add line 203
  24. theorem OAI.ArExplicit.CompleteComparison.cokernelMap_zero line 211
  25. theorem OAI.ArExplicit.CompleteComparison.cokernelMap_surjective line 217