OAI/Algebra/AuslanderReiten/Duality/DualResolution.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.Resolution.fixedLeft line 16
  2. abbrev OAI.ArExplicit.Resolution.rightE line 31
  3. abbrev OAI.ArExplicit.Resolution.rightF line 32
  4. def OAI.ArExplicit.Resolution.evaluateE line 34
  5. def OAI.ArExplicit.Resolution.fromRightE line 40
  6. theorem OAI.ArExplicit.Resolution.fromRightE_apply line 45
  7. theorem OAI.ArExplicit.Resolution.evaluateE_fromRightE line 48
  8. theorem OAI.ArExplicit.Resolution.fromRightE_evaluateE line 52
  9. def OAI.ArExplicit.Resolution.homEEquiv line 58
  10. def OAI.ArExplicit.Resolution.homERightLinearEquiv line 64
  11. theorem OAI.ArExplicit.Resolution.rightE_coeff_zero line 69
  12. theorem OAI.ArExplicit.Resolution.rightE_coeff_t line 74
  13. theorem OAI.ArExplicit.Resolution.rightE_coeff_j line 76
  14. theorem OAI.ArExplicit.Resolution.rightE_coeff_f line 78
  15. theorem OAI.ArExplicit.Resolution.rightE_coeff_n line 80
  16. theorem OAI.ArExplicit.Resolution.rightE_expand line 83
  17. def OAI.ArExplicit.Resolution.leftEll line 90
  18. theorem OAI.ArExplicit.Resolution.coe_leftEll line 100
  19. theorem OAI.ArExplicit.Resolution.evaluateE_precompose line 103
  20. theorem OAI.ArExplicit.Resolution.ell_mul_formula line 116
  21. theorem OAI.ArExplicit.Resolution.smul_vertexF line 123
  22. def OAI.ArExplicit.Resolution.evaluateF line 127
  23. def OAI.ArExplicit.Resolution.fromRightF line 133
  24. theorem OAI.ArExplicit.Resolution.evaluateF_fromRightF line 138
  25. theorem OAI.ArExplicit.Resolution.fromRightF_evaluateF line 142
  26. def OAI.ArExplicit.Resolution.homFEquiv line 148
  27. def OAI.ArExplicit.Resolution.homFRightLinearEquiv line 154
  28. theorem OAI.ArExplicit.Resolution.rightF_coeff_zero line 159
  29. theorem OAI.ArExplicit.Resolution.rightF_coeff_e line 164
  30. theorem OAI.ArExplicit.Resolution.rightF_coeff_x line 166
  31. theorem OAI.ArExplicit.Resolution.rightF_coeff_y line 168
  32. theorem OAI.ArExplicit.Resolution.rightF_coeff_z line 170
  33. theorem OAI.ArExplicit.Resolution.rightF_coeff_u line 172
  34. theorem OAI.ArExplicit.Resolution.rightF_coeff_v line 174
  35. theorem OAI.ArExplicit.Resolution.rightF_expand line 177
  36. def OAI.ArExplicit.Resolution.leftU line 183
  37. theorem OAI.ArExplicit.Resolution.coe_leftU line 191
  38. theorem OAI.ArExplicit.Resolution.evaluate_precompose_dU line 193
  39. theorem OAI.ArExplicit.Resolution.u_mul_formula line 204
  40. theorem OAI.ArExplicit.Resolution.leftU_injective line 211
  41. def OAI.ArExplicit.Resolution.leftUPreimage line 223
  42. theorem OAI.ArExplicit.Resolution.leftUPreimage_spec line 228
  43. theorem OAI.ArExplicit.Resolution.ell_mul_eq_zero_iff line 237
  44. def OAI.ArExplicit.Resolution.leftEllPreimage line 263
  45. theorem OAI.ArExplicit.Resolution.leftEllPreimage_spec line 270
  46. theorem OAI.ArExplicit.Resolution.leftEll_kernel_expand line 278
  47. theorem OAI.ArExplicit.Resolution.leftEll_exact line 287
  48. theorem OAI.ArExplicit.Resolution.leftEll_one_kernel_expand line 305
  49. theorem OAI.ArExplicit.Resolution.leftU_exact line 316
  50. def OAI.ArExplicit.Resolution.exceptionalBoundaryPreimage line 331
  51. theorem OAI.ArExplicit.Resolution.exceptionalBoundaryPreimage_spec line 337
  52. theorem OAI.ArExplicit.Resolution.exceptional_boundary_iff line 344
  53. def OAI.ArExplicit.Resolution.exceptionalCycle line 357
  54. theorem OAI.ArExplicit.Resolution.exceptionalCycle_closed line 362
  55. theorem OAI.ArExplicit.Resolution.exceptionalCycle_not_boundary line 368
  56. theorem OAI.ArExplicit.Resolution.exceptional_right_action line 373