OAI/RingTheory/Tachikawa/StableShift.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Tachikawa.VectorSplit.Z line 12
  2. def OAI.Tachikawa.VectorSplit.inc line 14
  3. def OAI.Tachikawa.VectorSplit.retract line 16
  4. lemma OAI.Tachikawa.VectorSplit.retract_inc line 19
  5. lemma OAI.Tachikawa.VectorSplit.retract_cycle line 22
  6. lemma OAI.Tachikawa.VectorSplit.cycle_d line 25
  7. def OAI.Tachikawa.VectorSplit.boundary line 33
  8. lemma OAI.Tachikawa.VectorSplit.boundary_cycle line 39
  9. abbrev OAI.Tachikawa.VectorSplit.H line 43
  10. def OAI.Tachikawa.VectorSplit.quotient line 45
  11. def OAI.Tachikawa.VectorSplit.representatives line 47
  12. lemma OAI.Tachikawa.VectorSplit.quotient_representatives line 51
  13. lemma OAI.Tachikawa.VectorSplit.quotient_representatives_apply line 56
  14. lemma OAI.Tachikawa.VectorSplit.quotient_boundary line 60
  15. def OAI.Tachikawa.VectorSplit.boundaryPart line 64
  16. def OAI.Tachikawa.VectorSplit.rawLift line 70
  17. lemma OAI.Tachikawa.VectorSplit.boundary_rawLift line 74
  18. def OAI.Tachikawa.VectorSplit.lift line 81
  19. lemma OAI.Tachikawa.VectorSplit.boundary_lift line 84
  20. lemma OAI.Tachikawa.VectorSplit.retract_lift line 90
  21. def OAI.Tachikawa.VectorSplit.complement line 96
  22. lemma OAI.Tachikawa.VectorSplit.complement_cycle line 99
  23. lemma OAI.Tachikawa.VectorSplit.complement_eq_lift line 104
  24. def OAI.Tachikawa.VectorSplit.homotopyComponent line 116
  25. lemma OAI.Tachikawa.VectorSplit.homotopy_d line 119
  26. lemma OAI.Tachikawa.VectorSplit.homotopy_boundary line 124
  27. def OAI.Tachikawa.completeHom line 146
  28. lemma OAI.Tachikawa.completeHom_d line 149
  29. lemma OAI.Tachikawa.completeHom_memZ line 152
  30. def OAI.Tachikawa.CompleteHom.cokerCycles line 160
  31. lemma OAI.Tachikawa.CompleteHom.boundary_iff line 184
  32. def OAI.Tachikawa.CompleteHom.equiv line 203
  33. lemma OAI.Tachikawa.linear_descent line 227
  34. lemma OAI.Tachikawa.StableShift.hom_lift_surjective line 242
  35. def OAI.Tachikawa.StableShift.liftLinear line 246
  36. lemma OAI.Tachikawa.StableShift.liftLinear_lifts line 250
  37. def OAI.Tachikawa.StableShift.kernelMap line 255
  38. lemma OAI.Tachikawa.StableShift.kernelMap_class line 276
  39. lemma OAI.Tachikawa.StableShift.kernelMap_factors line 301
  40. def OAI.Tachikawa.StableShift.map line 313
  41. lemma OAI.Tachikawa.StableShift.map_class line 318
  42. lemma OAI.Tachikawa.StableShift.kernelMap_reflects_factors line 325
  43. lemma OAI.Tachikawa.StableShift.map_injective line 350
  44. lemma OAI.Tachikawa.StableShift.map_surjective line 360
  45. def OAI.Tachikawa.StableShift.equiv line 377
  46. theorem OAI.Tachikawa.exact_square_factors_iff line 395
  47. theorem OAI.Tachikawa.exists_exact_square_down line 458
  48. def OAI.Tachikawa.VectorSplit.cycleMap line 486
  49. lemma OAI.Tachikawa.VectorSplit.cycleMap_boundary line 494
  50. def OAI.Tachikawa.VectorSplit.Hmap line 499
  51. lemma OAI.Tachikawa.VectorSplit.Hmap_quotient line 503
  52. lemma OAI.Tachikawa.VectorSplit.quotient_eq_zero_iff line 506
  53. lemma OAI.Tachikawa.VectorSplit.quotient_surjective line 510
  54. lemma OAI.Tachikawa.VectorSplit.Hmap_comp line 513
  55. lemma OAI.Tachikawa.VectorSplit.Hmap_id line 520
  56. lemma OAI.Tachikawa.VectorSplit.Hmap_zero line 526
  57. lemma OAI.Tachikawa.VectorSplit.Hmap_add line 532
  58. lemma OAI.Tachikawa.VectorSplit.Hmap_smul line 541
  59. lemma OAI.Tachikawa.VectorSplit.quotient_zero_iff_predecessor line 551
  60. lemma OAI.Tachikawa.VectorSplit.memZ_iff line 559
  61. lemma OAI.Tachikawa.VectorSplit.comm_apply line 575
  62. lemma OAI.Tachikawa.VectorSplit.Hmap_surjective_of_right_zero line 581
  63. lemma OAI.Tachikawa.VectorSplit.Hmap_injective_of_prev_surjective line 612
  64. lemma OAI.Tachikawa.VectorSplit.Hmap_injective_of_prev_zero line 645
  65. lemma OAI.Tachikawa.VectorSplit.Hmap_bijective_of_zeros line 652
  66. def OAI.Tachikawa.completeHomMap line 667
  67. lemma OAI.Tachikawa.completeHomMap_apply line 678
  68. lemma OAI.Tachikawa.completeHomMap_comp line 681
  69. lemma OAI.Tachikawa.completeHomMap_id line 686
  70. lemma OAI.Tachikawa.completeHomMap_zero line 690
  71. lemma OAI.Tachikawa.completeHomMap_add line 694
  72. lemma OAI.Tachikawa.completeHomMap_injective line 699
  73. lemma OAI.Tachikawa.completeHomMap_exact line 706
  74. lemma OAI.Tachikawa.completeHomMap_surjective line 721
  75. lemma OAI.Tachikawa.completeHom_projective_zero line 740
  76. abbrev OAI.Tachikawa.completeHmap line 751
  77. lemma OAI.Tachikawa.completeHmap_comp line 754
  78. lemma OAI.Tachikawa.completeHmap_id line 757
  79. lemma OAI.Tachikawa.completeHmap_add line 760
  80. lemma OAI.Tachikawa.completeHmap_zero line 763
  81. def OAI.Tachikawa.completeHomIso line 767
  82. def OAI.Tachikawa.completeFunctorHom line 786
  83. lemma OAI.Tachikawa.completeFunctorHom_homotopic line 798
  84. lemma OAI.Tachikawa.completeFunctorHom_natural line 841