OAI/RingTheory/Tachikawa/HomProfile.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Tachikawa.SourceField.Base line 8
  2. abbrev OAI.Tachikawa.SourceField.K line 9
  3. def OAI.Tachikawa.SourceField.parameter line 11
  4. def OAI.Tachikawa.SourceField.q line 12
  5. def OAI.Tachikawa.SourceField.H₁ line 13
  6. def OAI.Tachikawa.SourceField.H₂ line 14
  7. lemma OAI.Tachikawa.SourceField.parameter_ne_zero line 16
  8. lemma OAI.Tachikawa.SourceField.one_add_q_pow_ne_zero line 22
  9. lemma OAI.Tachikawa.SourceField.distinct_parameter_powers line 33
  10. lemma OAI.Tachikawa.SourceField.H_powers_distinct line 44
  11. lemma OAI.Tachikawa.SourceField.H_inverse_powers_distinct line 47
  12. def OAI.Tachikawa.MissingYProfile.finiteYX line 60
  13. def OAI.Tachikawa.MissingYProfile.shift line 64
  14. abbrev OAI.Tachikawa.MissingYProfile.W line 68
  15. def OAI.Tachikawa.MissingYProfile.profile line 71
  16. def OAI.Tachikawa.MissingYProfile.sourceProfile line 75
  17. theorem OAI.Tachikawa.MissingYProfile.W_zero_nontrivial line 77
  18. theorem OAI.Tachikawa.MissingYProfile.source_W_zero_nontrivial line 84
  19. abbrev OAI.Tachikawa.Construction.evalK line 98
  20. lemma OAI.Tachikawa.Construction.evalK_finite line 102
  21. lemma OAI.Tachikawa.Construction.evalK_projective line 108
  22. lemma OAI.Tachikawa.Construction.natJJ_finite line 113
  23. lemma OAI.Tachikawa.Construction.natJJ_projective line 117
  24. def OAI.Tachikawa.Construction.evalFiveFiberStableEquiv line 121
  25. lemma OAI.Tachikawa.exact_square_difference_inverse line 149
  26. def OAI.Tachikawa.StableEquiv.ofExactSquares line 166
  27. def OAI.Tachikawa.StableEquiv.down line 190
  28. theorem OAI.Tachikawa.exists_exact_square_up line 206
  29. def OAI.Tachikawa.StableEquiv.up line 223
  30. lemma OAI.Tachikawa.Enveloping.evalFree_finite line 264
  31. def OAI.Tachikawa.Enveloping.evalCosyCokerStableEquiv line 269
  32. def OAI.Tachikawa.Construction.evalNegativeFiveFiberStableEquiv line 304
  33. def OAI.Tachikawa.Construction.yxFiberStableEquiv line 326
  34. def OAI.Tachikawa.cosyCokerStableEquiv line 342
  35. def OAI.Tachikawa.syzyCokerStableEquiv line 355
  36. def OAI.Tachikawa.negativeCokerStableEquiv line 368
  37. def OAI.Tachikawa.positiveCokerStableEquiv line 381
  38. def OAI.Tachikawa.stablePostEquiv line 404
  39. def OAI.Tachikawa.finiteCoker line 435
  40. def OAI.Tachikawa.completeCokerDuality line 441
  41. def OAI.Tachikawa.C.homCfSimpleEquiv line 461
  42. def OAI.Tachikawa.C.inducedFHomEquiv line 471
  43. lemma OAI.Tachikawa.C.forwardJ_hom_zero line 492
  44. lemma OAI.Tachikawa.C.reverseJ_hom_zero line 501
  45. def OAI.Tachikawa.piSupportedEquiv line 521
  46. lemma OAI.Tachikawa.OuterTensor.hom_zero_left line 541
  47. lemma OAI.Tachikawa.OuterTensor.hom_zero_right line 549
  48. lemma OAI.Tachikawa.OuterTensor.total_hom_zero line 557
  49. def OAI.Tachikawa.OuterTensor.totalHomSupported line 575
  50. lemma OAI.Tachikawa.Construction.forwardJJ_hom_zero line 615
  51. lemma OAI.Tachikawa.Construction.reverseJJ_hom_zero line 628
  52. def OAI.Tachikawa.Construction.forwardJJHomEquiv line 641
  53. def OAI.Tachikawa.Construction.reverseJJHomEquiv line 658
  54. def OAI.Tachikawa.Construction.jjFiberHomEquiv line 675
  55. lemma OAI.Tachikawa.Construction.jjFiber_hom_zero line 682
  56. def OAI.Tachikawa.Construction.jjFiberHomZeroEquiv line 691
  57. def OAI.Tachikawa.Construction.jjFiberHomThreeEquiv line 700
  58. lemma OAI.Tachikawa.stableCoker_subsingleton line 719
  59. def OAI.Tachikawa.cokerHomIsolated line 732
  60. def OAI.Tachikawa.stableCokerIsolatedEquiv line 747
  61. theorem OAI.Tachikawa.Construction.jjFiber_stable_zero line 784
  62. def OAI.Tachikawa.Construction.jjFiberStableZeroEquiv line 790
  63. def OAI.Tachikawa.Construction.jjFiberStableThreeEquiv line 799
  64. theorem OAI.Tachikawa.Construction.jjFiber_stable_profile line 808
  65. def OAI.Tachikawa.Construction.yxShiftFiberStableEquiv line 830
  66. def OAI.Tachikawa.Construction.WFiberDualEquiv line 845
  67. theorem OAI.Tachikawa.Construction.y_profile line 858
  68. theorem OAI.Tachikawa.Construction.source_y_profile line 876
  69. def OAI.Tachikawa.cokerKernelEquiv line 889
  70. def OAI.Tachikawa.cokerStableHomSucc line 905
  71. def OAI.Tachikawa.cokerStableHomNat line 922
  72. def OAI.Tachikawa.cokerStableHomTranslate line 934
  73. def OAI.Tachikawa.Construction.finiteX line 956
  74. abbrev OAI.Tachikawa.Construction.xComplete line 960
  75. def OAI.Tachikawa.Construction.completeYStableEquiv line 962
  76. def OAI.Tachikawa.Construction.completeYHomologyEquiv line 980
  77. lemma OAI.Tachikawa.Construction.completeYHomology_zero line 989
  78. lemma OAI.Tachikawa.CompleteHom.equiv_quotient line 1007
  79. lemma OAI.Tachikawa.CompleteHom.equiv_natural line 1012
  80. def OAI.Tachikawa.CompleteHom.zeroEquiv line 1026
  81. lemma OAI.Tachikawa.CompleteHom.zeroEquiv_natural line 1031
  82. lemma OAI.Tachikawa.linear_surjective_to_line line 1052
  83. abbrev OAI.Tachikawa.CompleteStableExt.Q line 1072
  84. def OAI.Tachikawa.CompleteStableExt.cycles line 1074
  85. def OAI.Tachikawa.CompleteStableExt.toExt line 1087
  86. lemma OAI.Tachikawa.CompleteStableExt.toExt_surjective line 1091
  87. lemma OAI.Tachikawa.CompleteStableExt.toExt_kernel line 1104
  88. def OAI.Tachikawa.CompleteStableExt.equiv line 1140
  89. abbrev OAI.Tachikawa.Construction.selfHom line 1159
  90. def OAI.Tachikawa.Construction.positiveSelfHomExt line 1161
  91. lemma OAI.Tachikawa.Construction.positiveSelfHom_zero line 1172
  92. def OAI.Tachikawa.Construction.selfHomDual line 1179
  93. lemma OAI.Tachikawa.Construction.selfHom_zero_of_dual line 1201
  94. lemma OAI.Tachikawa.Construction.selfHom_zero_near line 1213
  95. lemma OAI.Tachikawa.Construction.XEnd_scalar line 1222
  96. def OAI.Tachikawa.Construction.stableXEndEquiv line 1235
  97. def OAI.Tachikawa.Construction.selfHomZeroEquiv line 1252
  98. abbrev OAI.Tachikawa.Construction.xTwistHom line 1266
  99. lemma OAI.Tachikawa.Construction.xTwistHom_positive line 1270
  100. lemma OAI.Tachikawa.Construction.xTwistHom_negative line 1276