OAI/RingTheory/Tachikawa/Period.lean

GitHub source file

146 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Tachikawa.TrivialInduction.map_zero line 13
  2. def OAI.Tachikawa.TrivialInduction.functor line 22
  3. instance OAI.Tachikawa.TrivialInduction.(instance at line 28) line 28
  4. abbrev OAI.Tachikawa.C.T line 44
  5. abbrev OAI.Tachikawa.C.TSimple line 45
  6. def OAI.Tachikawa.C.inducedObj line 47
  7. def OAI.Tachikawa.C.inducedD line 49
  8. lemma OAI.Tachikawa.C.inducedD_comp line 52
  9. def OAI.Tachikawa.C.inducedComplex line 58
  10. lemma OAI.Tachikawa.C.inducedComplex_d line 61
  11. lemma OAI.Tachikawa.C.inducedObj_projective line 65
  12. lemma OAI.Tachikawa.C.inducedObj_finite line 77
  13. lemma OAI.Tachikawa.C.induced_positive_hom_zero line 98
  14. lemma OAI.Tachikawa.C.inducedD_exact line 106
  15. def OAI.Tachikawa.C.inducedAug line 110
  16. lemma OAI.Tachikawa.C.inducedAug_surjective line 114
  17. lemma OAI.Tachikawa.C.inducedAug_exact line 120
  18. def OAI.Tachikawa.TrivialExtension.scaleDual line 138
  19. lemma OAI.Tachikawa.TrivialExtension.scaleDual_fst line 167
  20. lemma OAI.Tachikawa.TrivialExtension.scaleDual_snd line 169
  21. lemma OAI.Tachikawa.TrivialExtension.scaleDual_inl line 171
  22. lemma OAI.Tachikawa.TrivialExtension.scaleDual_inr line 176
  23. abbrev OAI.Tachikawa.TrivialInduction.inverseTwist line 189
  24. def OAI.Tachikawa.TrivialInduction.twistComparison line 192
  25. lemma OAI.Tachikawa.TrivialInduction.twistComparison_natural line 206
  26. def OAI.Tachikawa.extShiftEquiv line 226
  27. def OAI.Tachikawa.extQuotientEquiv line 240
  28. def OAI.Tachikawa.linearShortComplex line 272
  29. lemma OAI.Tachikawa.linearShortExact line 277
  30. def OAI.Tachikawa.kernelRangeComplex line 284
  31. lemma OAI.Tachikawa.kernelRange_shortExact line 293
  32. def OAI.Tachikawa.kernelSurjectiveComplex line 302
  33. lemma OAI.Tachikawa.kernelSurjective_shortExact line 305
  34. abbrev OAI.Tachikawa.C.InducedBoundaries line 318
  35. abbrev OAI.Tachikawa.C.inducedBoundaryObj line 319
  36. def OAI.Tachikawa.C.inducedBoundaryResolution line 321
  37. lemma OAI.Tachikawa.C.inducedBoundary_ext_zero line 337
  38. def OAI.Tachikawa.RightCorner.homEquivScalar line 368
  39. lemma OAI.Tachikawa.RightCorner.homEquivScalar_apply line 373
  40. lemma OAI.Tachikawa.RightCorner.homEquivScalar_precomp line 376
  41. def OAI.Tachikawa.C.v line 389
  42. lemma OAI.Tachikawa.C.e_mul_v line 391
  43. def OAI.Tachikawa.C.vHom line 393
  44. lemma OAI.Tachikawa.C.vHom_generator line 396
  45. lemma OAI.Tachikawa.C.homEquiv_vHom line 400
  46. def OAI.Tachikawa.C.nuTwoAug line 403
  47. def OAI.Tachikawa.C.nuTwoCycle line 408
  48. lemma OAI.Tachikawa.C.nuTwoCycle_aug line 414
  49. lemma OAI.Tachikawa.C.vHom_rhoEll line 419
  50. lemma OAI.Tachikawa.C.lambdaEll_one_six line 427
  51. lemma OAI.Tachikawa.C.hom_comp_rhoEll_one_six line 432
  52. lemma OAI.Tachikawa.C.nuTwoCycle_closed line 438
  53. lemma OAI.Tachikawa.C.dual_vHom_rhoEll line 442
  54. lemma OAI.Tachikawa.C.nuTwoAug_boundary line 447
  55. lemma OAI.Tachikawa.C.dualTwoCycle_decompose line 451
  56. lemma OAI.Tachikawa.C.hom_cycle_decompose line 467
  57. lemma OAI.Tachikawa.C.dual_vHom_boundary_iff line 503
  58. lemma OAI.Tachikawa.C.nuTwo_boundary_iff line 515
  59. lemma OAI.Tachikawa.C.homRight_vHom_six line 522
  60. lemma OAI.Tachikawa.C.dual_vHom_action line 529
  61. lemma OAI.Tachikawa.C.nuTwoAug_smul line 543
  62. lemma OAI.Tachikawa.C.exact_rhoEll_one line 559
  63. abbrev OAI.Tachikawa.C.InducedTwoCycles line 565
  64. lemma OAI.Tachikawa.C.twoCycles_first line 568
  65. lemma OAI.Tachikawa.C.twoCycles_second line 572
  66. lemma OAI.Tachikawa.C.vHom_twoCycles line 576
  67. def OAI.Tachikawa.C.inducedTwoAug line 582
  68. def OAI.Tachikawa.C.inducedTwoBoundary line 596
  69. lemma OAI.Tachikawa.C.inducedTwoAug_surjective line 604
  70. lemma OAI.Tachikawa.C.inducedD_two_apply line 617
  71. lemma OAI.Tachikawa.C.inducedTwoAug_exact line 622
  72. def OAI.Tachikawa.C.inducedTwoHomologyEquiv line 641
  73. abbrev OAI.Tachikawa.C.InducedRange line 658
  74. abbrev OAI.Tachikawa.C.inducedRangeObj line 659
  75. abbrev OAI.Tachikawa.C.initialShortComplex line 661
  76. lemma OAI.Tachikawa.C.initial_shortExact line 673
  77. abbrev OAI.Tachikawa.C.middleShortComplex line 677
  78. lemma OAI.Tachikawa.C.middle_shortExact line 690
  79. def OAI.Tachikawa.C.upperInclusion line 696
  80. def OAI.Tachikawa.C.upperRangeMap line 701
  81. lemma OAI.Tachikawa.C.upper_exact line 705
  82. abbrev OAI.Tachikawa.C.upperShortComplex line 720
  83. lemma OAI.Tachikawa.C.upper_shortExact line 724
  84. def OAI.Tachikawa.C.boundaryInclusion line 729
  85. abbrev OAI.Tachikawa.C.homologyShortComplex line 738
  86. lemma OAI.Tachikawa.C.homology_shortExact line 752
  87. lemma OAI.Tachikawa.C.induced_positive_ext_zero line 762
  88. abbrev OAI.Tachikawa.C.simpleObj line 782
  89. lemma OAI.Tachikawa.C.inducedRange_hom_zero line 786
  90. lemma OAI.Tachikawa.C.inducedRange_ext_zero_zero line 796
  91. lemma OAI.Tachikawa.C.simple_ext_one_zero line 803
  92. lemma OAI.Tachikawa.C.firstRange_ext_one_zero line 817
  93. lemma OAI.Tachikawa.C.simple_ext_two_zero line 827
  94. def OAI.Tachikawa.C.upperShiftEquiv line 838
  95. def OAI.Tachikawa.C.middleShiftEquiv line 847
  96. def OAI.Tachikawa.C.initialShiftEquiv line 856
  97. def OAI.Tachikawa.C.threeShiftEquiv line 868
  98. def OAI.Tachikawa.C.simpleExtPeriod line 874
  99. lemma OAI.Tachikawa.extShiftEquiv_apply line 888
  100. lemma OAI.Tachikawa.extShiftEquiv_comp line 893
  101. lemma OAI.Tachikawa.extQuotientEquiv_apply line 902
  102. lemma OAI.Tachikawa.extQuotientEquiv_comp line 906
  103. def OAI.Tachikawa.C.initialClass line 924
  104. def OAI.Tachikawa.C.middleClass line 927
  105. def OAI.Tachikawa.C.upperClass line 930
  106. def OAI.Tachikawa.C.homologyClass line 933
  107. lemma OAI.Tachikawa.C.simpleExtPeriod_apply line 937
  108. def OAI.Tachikawa.C.tau line 946
  109. lemma OAI.Tachikawa.C.simpleExtPeriod_eq_tau_comp line 950
  110. def OAI.Tachikawa.C.simpleEndEquiv line 960
  111. def OAI.Tachikawa.C.simpleExtZeroEquiv line 979
  112. def OAI.Tachikawa.C.simpleExtMultiple line 994
  113. lemma OAI.Tachikawa.C.simpleExt_zero_off_multiples line 1002
  114. lemma OAI.Tachikawa.C.simple_nonprojective_T line 1020
  115. abbrev OAI.Tachikawa.C.tTwist line 1036
  116. def OAI.Tachikawa.C.simpleTwistComparison line 1039
  117. def OAI.Tachikawa.C.inducedTwistComparison line 1046
  118. lemma OAI.Tachikawa.C.inducedTwist_d line 1051
  119. def OAI.Tachikawa.C.rangeTwistComparison line 1057
  120. def OAI.Tachikawa.C.cyclesTwistComparison line 1070
  121. def OAI.Tachikawa.C.twistInitialHom line 1083
  122. def OAI.Tachikawa.C.twistMiddleHom line 1091
  123. def OAI.Tachikawa.C.twistUpperHom line 1104
  124. lemma OAI.Tachikawa.C.homology_twist_comparison line 1116
  125. lemma OAI.Tachikawa.ext_push_comparison line 1133
  126. lemma OAI.Tachikawa.C.initial_twist_naturality line 1153
  127. lemma OAI.Tachikawa.C.middle_twist_naturality line 1163
  128. lemma OAI.Tachikawa.C.upper_twist_naturality line 1174
  129. lemma OAI.Tachikawa.C.homology_twist_naturality line 1184
  130. lemma OAI.Tachikawa.C.tau_twist_naturality line 1193
  131. def OAI.Tachikawa.C.tauPower line 1214
  132. lemma OAI.Tachikawa.C.tauPower_zero line 1217
  133. lemma OAI.Tachikawa.C.tauPower_ne_zero line 1221
  134. lemma OAI.Tachikawa.C.tauPower_succ line 1227
  135. lemma OAI.Tachikawa.C.tauPower_comp_aux line 1237
  136. lemma OAI.Tachikawa.C.tauPower_comp line 1254
  137. lemma OAI.Tachikawa.C.eq_smul_tauPower line 1258
  138. lemma OAI.Tachikawa.C.tau_coordinates_comp line 1264
  139. lemma OAI.Tachikawa.extIso_comp line 1288
  140. def OAI.Tachikawa.C.simpleTwistIso line 1308
  141. def OAI.Tachikawa.C.simpleTwistExt line 1319
  142. lemma OAI.Tachikawa.C.simpleTwistExt_comp line 1325
  143. lemma OAI.Tachikawa.C.simpleTwist_mk₀_smul line 1335
  144. lemma OAI.Tachikawa.C.simpleTwist_tau line 1345
  145. lemma OAI.Tachikawa.C.simpleTwist_tauPower line 1368
  146. lemma OAI.Tachikawa.C.simpleTwist_weight line 1381