OAI/RingTheory/Tachikawa/DownHom.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Tachikawa.CokerAt.mapLinear line 15
  2. def OAI.Tachikawa.FullHomComparison.toStable line 30
  3. def OAI.Tachikawa.FullHomComparison.toHomotopy line 34
  4. lemma OAI.Tachikawa.FullHomComparison.toStable_surjective line 39
  5. lemma OAI.Tachikawa.FullHomComparison.kernel_eq line 48
  6. def OAI.Tachikawa.FullHomComparison.equiv line 61
  7. abbrev OAI.Tachikawa.CompleteTranslate.complex line 86
  8. lemma OAI.Tachikawa.CompleteTranslate.exact line 98
  9. lemma OAI.Tachikawa.CompleteTranslate.totallyAcyclic line 104
  10. def OAI.Tachikawa.CompleteTranslate.map line 114
  11. def OAI.Tachikawa.CompleteTranslate.cokerEquiv line 119
  12. abbrev OAI.Tachikawa.DownHom.Cochain line 136
  13. def OAI.Tachikawa.DownHom.Closed line 139
  14. lemma OAI.Tachikawa.DownHom.transport_left line 143
  15. lemma OAI.Tachikawa.DownHom.transport_right line 146
  16. lemma OAI.Tachikawa.DownHom.d_pre_eq line 150
  17. lemma OAI.Tachikawa.DownHom.d_post_eq line 154
  18. def OAI.Tachikawa.DownHom.ofChain line 160
  19. lemma OAI.Tachikawa.DownHom.ofChain_closed line 163
  20. def OAI.Tachikawa.DownHom.toChain line 171
  21. lemma OAI.Tachikawa.DownHom.to_ofChain line 176
  22. lemma OAI.Tachikawa.DownHom.of_toChain line 179
  23. def OAI.Tachikawa.DownHom.Boundary line 185
  24. lemma OAI.Tachikawa.DownHom.ofHomotopy_boundary line 190
  25. lemma OAI.Tachikawa.DownHom.boundary_homotopy line 212
  26. structure OAI.Tachikawa.DownHom.Index line 239
  27. def OAI.Tachikawa.DownHom.indexEquiv line 244
  28. instance OAI.Tachikawa.DownHom.(instance at line 249) line 249
  29. instance OAI.Tachikawa.DownHom.(instance at line 250) line 250
  30. lemma OAI.Tachikawa.DownHom.zero_apply line 253
  31. lemma OAI.Tachikawa.DownHom.add_apply line 255
  32. lemma OAI.Tachikawa.DownHom.twice line 258
  33. lemma OAI.Tachikawa.DownHom.negative line 262
  34. lemma OAI.Tachikawa.DownHom.closed_zero line 265
  35. lemma OAI.Tachikawa.DownHom.closed_add line 267
  36. lemma OAI.Tachikawa.DownHom.closed_of_adjacent line 272
  37. def OAI.Tachikawa.DownHom.diff line 284
  38. lemma OAI.Tachikawa.DownHom.diff_add line 287
  39. lemma OAI.Tachikawa.DownHom.diff_closed line 291
  40. lemma OAI.Tachikawa.DownHom.boundary_diff line 300
  41. lemma OAI.Tachikawa.DownHom.boundary_add line 303
  42. lemma OAI.Tachikawa.DownHom.boundary_zero line 312
  43. lemma OAI.Tachikawa.DownHom.boundary_iff_diff line 315
  44. lemma OAI.Tachikawa.DownHom.closed_iff_diff_zero line 323
  45. def OAI.Tachikawa.DownHom.pre line 339
  46. def OAI.Tachikawa.DownHom.post line 342
  47. lemma OAI.Tachikawa.DownHom.pre_closed line 344
  48. lemma OAI.Tachikawa.DownHom.post_closed line 348
  49. def OAI.Tachikawa.DownHom.cochainEquiv line 363
  50. lemma OAI.Tachikawa.DownHom.cochainEquiv_closed_iff line 376
  51. lemma OAI.Tachikawa.DownHom.cochainEquiv_diff line 387
  52. lemma OAI.Tachikawa.DownHom.cochainEquiv_boundary_iff line 394
  53. lemma OAI.Tachikawa.exists_augmented_complete_lift line 417
  54. def OAI.Tachikawa.DownHom.evalCycle line 441
  55. def OAI.Tachikawa.DownHom.evalClass line 448
  56. lemma OAI.Tachikawa.DownHom.eval_boundary line 452
  57. lemma OAI.Tachikawa.DownHom.boundary_of_eval_zero line 467
  58. lemma OAI.Tachikawa.DownHom.eval_surjective line 500
  59. lemma OAI.Tachikawa.DownHom.eval_add line 534
  60. abbrev OAI.Tachikawa.DownHom.mapComplex line 546
  61. def OAI.Tachikawa.DownHom.mapCochain line 549
  62. lemma OAI.Tachikawa.DownHom.map_closed line 551
  63. lemma OAI.Tachikawa.DownHom.map_augmentation_zero line 560
  64. def OAI.Tachikawa.DownHom.actionDelta line 564
  65. lemma OAI.Tachikawa.DownHom.actionDelta_closed line 566
  66. abbrev OAI.Tachikawa.DownHom.homologyDelta line 569
  67. lemma OAI.Tachikawa.DownHom.eval_actionDelta line 576
  68. lemma OAI.Tachikawa.Triangular.diagonal₀_comp line 607
  69. lemma OAI.Tachikawa.Triangular.diagonal₁_comp line 613
  70. lemma OAI.Tachikawa.Triangular.diagonal₀_post line 619
  71. lemma OAI.Tachikawa.Triangular.diagonal₁_post line 622
  72. lemma OAI.Tachikawa.Triangular.cross₁₀_comp_right line 625
  73. lemma OAI.Tachikawa.Triangular.cross₁₀_comp_left line 631
  74. abbrev OAI.Tachikawa.Triangular.down₀ line 639
  75. abbrev OAI.Tachikawa.Triangular.down₁ line 641
  76. abbrev OAI.Tachikawa.Triangular.downCross line 643
  77. lemma OAI.Tachikawa.Triangular.down₀_closed line 647
  78. lemma OAI.Tachikawa.Triangular.down₁_closed line 651
  79. lemma OAI.Tachikawa.Triangular.downCross_closed line 655
  80. lemma OAI.Tachikawa.Triangular.down₀_boundary line 659
  81. lemma OAI.Tachikawa.Triangular.down₁_boundary line 663
  82. lemma OAI.Tachikawa.Triangular.downCross_boundary line 667
  83. lemma OAI.Tachikawa.Triangular.downCross_delta line 672