OAI/RingTheory/Tachikawa/ReverseResolution.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Tachikawa.C.dualCoeff line 11
  2. lemma OAI.Tachikawa.C.dualCoeff_apply line 13
  3. lemma OAI.Tachikawa.C.e_fixed_z line 15
  4. lemma OAI.Tachikawa.C.e_fixed_j line 21
  5. def OAI.Tachikawa.C.leftDualZ line 27
  6. def OAI.Tachikawa.C.leftDualJ line 30
  7. lemma OAI.Tachikawa.C.leftDualZ_ce line 33
  8. lemma OAI.Tachikawa.C.leftDualJ_ce line 37
  9. def OAI.Tachikawa.C.leftDualAug line 41
  10. lemma OAI.Tachikawa.C.leftDualAug_surjective line 44
  11. def OAI.Tachikawa.C.leftDualD₁ line 56
  12. def OAI.Tachikawa.C.t line 59
  13. lemma OAI.Tachikawa.C.t_mul_e line 60
  14. def OAI.Tachikawa.C.rhoT line 62
  15. lemma OAI.Tachikawa.C.rhoT_cf line 64
  16. lemma OAI.Tachikawa.C.rhoT_injective line 71
  17. lemma OAI.Tachikawa.C.leftDualAug_apply line 80
  18. lemma OAI.Tachikawa.C.leftDualAug_eq_zero_iff line 90
  19. lemma OAI.Tachikawa.C.exact_leftDualAug line 120
  20. lemma OAI.Tachikawa.C.exact_rhoT line 147
  21. def OAI.Tachikawa.C.leftDualResObj line 177
  22. def OAI.Tachikawa.C.leftDualResD line 183
  23. lemma OAI.Tachikawa.C.leftDualResD_exact line 188
  24. def OAI.Tachikawa.C.leftDualProjectiveResolution line 211
  25. lemma OAI.Tachikawa.C.leftDual_projectiveDimension line 218
  26. def OAI.Tachikawa.C.j line 246
  27. def OAI.Tachikawa.C.x line 247
  28. lemma OAI.Tachikawa.C.j_mul_e line 248
  29. lemma OAI.Tachikawa.C.x_mul_e line 249
  30. lemma OAI.Tachikawa.C.v_mul_f line 250
  31. def OAI.Tachikawa.C.rhoJ line 252
  32. def OAI.Tachikawa.C.rhoX line 253
  33. def OAI.Tachikawa.C.rhoV line 254
  34. lemma OAI.Tachikawa.C.rhoJ_cf line 256
  35. lemma OAI.Tachikawa.C.rhoX_ce line 262
  36. lemma OAI.Tachikawa.C.rhoV_ce line 268
  37. def OAI.Tachikawa.C.reverseCoeff line 274
  38. lemma OAI.Tachikawa.C.reverseCoeff_step line 276
  39. lemma OAI.Tachikawa.C.one_add_inv_power_ne_zero line 282
  40. lemma OAI.Tachikawa.C.reverseCoeff_nonexceptional line 290
  41. lemma OAI.Tachikawa.C.reverseD_exact line 302
  42. lemma OAI.Tachikawa.C.reverseD_comp line 312
  43. lemma OAI.Tachikawa.C.comparison_one line 318
  44. lemma OAI.Tachikawa.C.comparison_two line 333
  45. lemma OAI.Tachikawa.C.comparison_bottom line 346
  46. lemma OAI.Tachikawa.C.comparison_top line 353
  47. def OAI.Tachikawa.C.forwardObj line 367
  48. def OAI.Tachikawa.C.forwardD line 371
  49. lemma OAI.Tachikawa.C.forwardD_comp line 376
  50. def OAI.Tachikawa.C.forwardComplex line 386
  51. def OAI.Tachikawa.C.reverseObj line 390
  52. def OAI.Tachikawa.C.reverseD line 397
  53. lemma OAI.Tachikawa.C.reverseD_comp_zero line 404
  54. def OAI.Tachikawa.C.reverseComplex line 418
  55. def OAI.Tachikawa.C.comparisonComponent line 421
  56. lemma OAI.Tachikawa.C.comparison_comm line 429
  57. def OAI.Tachikawa.C.reverseComparison line 456
  58. lemma OAI.Tachikawa.shortComplex_quasiIso_of_cycles line 475
  59. lemma OAI.Tachikawa.shortComplex_cycles_of_quasiIso line 527
  60. lemma OAI.Tachikawa.C.comparison_injective_cycles line 585
  61. lemma OAI.Tachikawa.C.comparison_surjective_cycles line 599
  62. lemma OAI.Tachikawa.C.forwardComplex_exactAt line 624
  63. lemma OAI.Tachikawa.C.reverseComplex_exactAt line 641
  64. lemma OAI.Tachikawa.C.reverseComparison_quasiIso line 665
  65. lemma OAI.Tachikawa.C.f_mul_t line 690
  66. def OAI.Tachikawa.C.lambdaT line 692
  67. lemma OAI.Tachikawa.C.lambdaT_ec line 694
  68. lemma OAI.Tachikawa.C.exact_lambdaT line 703
  69. lemma OAI.Tachikawa.C.hom_exact_rhoEll_general line 728
  70. lemma OAI.Tachikawa.C.hom_exact_rhoT line 754
  71. lemma OAI.Tachikawa.C.nu_reverseEll_exact line 780
  72. lemma OAI.Tachikawa.C.nu_reverseTop_exact line 789
  73. def OAI.Tachikawa.C.fHom line 802
  74. lemma OAI.Tachikawa.C.homEquiv_fHom line 805
  75. lemma OAI.Tachikawa.C.fHom_rhoV line 809
  76. def OAI.Tachikawa.C.nuTopCycle line 819
  77. lemma OAI.Tachikawa.C.nuV_nuTwoCycle line 825
  78. lemma OAI.Tachikawa.C.homTop_decompose line 838
  79. lemma OAI.Tachikawa.C.nuTopCycle_description line 869
  80. lemma OAI.Tachikawa.C.nuV_cycles_injective line 879
  81. lemma OAI.Tachikawa.C.nuV_cycles_surjective line 890
  82. lemma OAI.Tachikawa.C.nuForward_exactAt line 908
  83. lemma OAI.Tachikawa.C.nuReverse_exactAt line 928
  84. lemma OAI.Tachikawa.C.nuReverseComparison_quasiIso line 951
  85. lemma OAI.Tachikawa.TrivialInduction.quasiIso_map line 994
  86. def OAI.Tachikawa.C.inducedReverseComparison line 1027
  87. lemma OAI.Tachikawa.C.inducedReverseComparison_quasiIso line 1032
  88. instance OAI.Tachikawa.downIntTensorSigns line 1045
  89. lemma OAI.Tachikawa.zeroDifferential_isIso_of_quasiIso line 1066
  90. lemma OAI.Tachikawa.vectorTensor_quasiIso_int line 1090
  91. lemma OAI.Tachikawa.OuterTensor.quasiIso_int line 1130
  92. abbrev OAI.Tachikawa.Construction.forwardJ line 1148
  93. abbrev OAI.Tachikawa.Construction.reverseJ line 1152
  94. abbrev OAI.Tachikawa.Construction.forwardJJ line 1156
  95. abbrev OAI.Tachikawa.Construction.reverseJJ line 1160
  96. def OAI.Tachikawa.Construction.jjReverseComparison line 1164
  97. lemma OAI.Tachikawa.Construction.jjReverseComparison_quasiIso line 1169
  98. lemma OAI.Tachikawa.OuterTensor.map_id_underlying line 1183
  99. lemma OAI.Tachikawa.OuterTensor.map_id_right_underlying line 1186
  100. instance OAI.Tachikawa.OuterTensor.(instance at line 1189) line 1189
  101. lemma OAI.Tachikawa.OuterTensor.exact_map_left line 1192
  102. lemma OAI.Tachikawa.OuterTensor.exact_map_right line 1198
  103. instance OAI.Tachikawa.OuterTensor.(instance at line 1204) line 1204
  104. instance OAI.Tachikawa.OuterTensor.(instance at line 1212) line 1212
  105. instance OAI.Tachikawa.OuterTensor.(instance at line 1219) line 1219
  106. instance OAI.Tachikawa.OuterTensor.(instance at line 1227) line 1227
  107. instance OAI.Tachikawa.OuterTensor.objFinite line 1243
  108. lemma OAI.Tachikawa.OuterTensor.isZero_obj_left line 1249
  109. lemma OAI.Tachikawa.OuterTensor.isZero_obj_right line 1253
  110. lemma OAI.Tachikawa.OuterTensor.total_isZero_above line 1256
  111. lemma OAI.Tachikawa.OuterTensor.total_finite line 1270
  112. def OAI.Tachikawa.coproductSupportIso line 1295
  113. lemma OAI.Tachikawa.coproduct_finite_of_support line 1314
  114. lemma OAI.Tachikawa.OuterTensor.total_projective_int line 1332
  115. lemma OAI.Tachikawa.OuterTensor.total_isZero_below_int line 1350
  116. lemma OAI.Tachikawa.OuterTensor.total_isZero_above_int line 1363
  117. lemma OAI.Tachikawa.OuterTensor.total_finite_below_int line 1376
  118. lemma OAI.Tachikawa.OuterTensor.total_finite_above_int line 1412