OAI/Algebra/AuslanderReiten/Cones/TwoConeSkeleton.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.TwoCone.middleTerm line 15
  2. abbrev OAI.ArExplicit.TwoCone.skeletonTerm line 17
  3. def OAI.ArExplicit.TwoCone.middleD line 19
  4. def OAI.ArExplicit.TwoCone.attachingRow line 22
  5. def OAI.ArExplicit.TwoCone.skeletonD line 25
  6. theorem OAI.ArExplicit.TwoCone.middleD_square line 28
  7. theorem OAI.ArExplicit.TwoCone.attachingRow_comm line 34
  8. theorem OAI.ArExplicit.TwoCone.skeletonD_square line 44
  9. def OAI.ArExplicit.TwoCone.skeletonComplex line 47
  10. theorem OAI.ArExplicit.TwoCone.middleD_exact line 51
  11. theorem OAI.ArExplicit.TwoCone.skeletonD_exact line 63
  12. def OAI.ArExplicit.TwoCone.topAttaching line 67
  13. theorem OAI.ArExplicit.TwoCone.topAttaching_apply line 72
  14. theorem OAI.ArExplicit.TwoCone.topAttaching_comm line 75
  15. def OAI.ArExplicit.TwoCone.skeletonCoordinates line 94
  16. theorem OAI.ArExplicit.TwoCone.skeletonCoordinates_d line 102
  17. abbrev OAI.ArExplicit.TwoCone.SkeletonCokernel line 112
  18. def OAI.ArExplicit.TwoCone.skeletonCokernelCoordinates line 114
  19. def OAI.ArExplicit.TwoCone.negativeTopCokernelEquiv line 119
  20. def OAI.ArExplicit.TwoCone.skeletonCokernelInclusion line 123
  21. def OAI.ArExplicit.TwoCone.topCokernelProjection line 127
  22. theorem OAI.ArExplicit.TwoCone.topCokernelProjection_mk line 133
  23. def OAI.ArExplicit.TwoCone.middleCokernelEquiv line 138
  24. def OAI.ArExplicit.TwoCone.bottomCokernelInclusion line 142
  25. def OAI.ArExplicit.TwoCone.singletonCokernelProjection line 145
  26. theorem OAI.ArExplicit.TwoCone.bottomCokernelInclusion_mk line 151
  27. theorem OAI.ArExplicit.TwoCone.singletonCokernelProjection_mk line 156
  28. theorem OAI.ArExplicit.TwoCone.skeletonCokernelInclusion_mk line 161
  29. theorem OAI.ArExplicit.TwoCone.bottomCokernelInclusion_injective line 165
  30. theorem OAI.ArExplicit.TwoCone.singletonCokernelProjection_surjective line 171
  31. theorem OAI.ArExplicit.TwoCone.skeletonCokernel_exact line 175
  32. theorem OAI.ArExplicit.TwoCone.negativeD_exact line 183
  33. theorem OAI.ArExplicit.TwoCone.skeletonCokernelInclusion_injective line 194
  34. theorem OAI.ArExplicit.TwoCone.topCokernelProjection_surjective line 201
  35. theorem OAI.ArExplicit.TwoCone.topCokernel_exact line 207