OAI/RingTheory/Tachikawa/Corner.lean

GitHub source file

165 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Tachikawa.LeftCorner line 9
  2. lemma OAI.Tachikawa.mem_leftCorner line 20
  3. def OAI.Tachikawa.LeftCorner.generator line 26
  4. def OAI.Tachikawa.LeftCorner.projection line 28
  5. lemma OAI.Tachikawa.LeftCorner.projection_apply line 33
  6. lemma OAI.Tachikawa.LeftCorner.projection_comp_inclusion line 35
  7. lemma OAI.Tachikawa.LeftCorner.projective line 40
  8. lemma OAI.Tachikawa.LeftCorner.hom_apply line 45
  9. def OAI.Tachikawa.LeftCorner.lift line 52
  10. lemma OAI.Tachikawa.LeftCorner.lift_apply line 57
  11. lemma OAI.Tachikawa.LeftCorner.lift_generator line 60
  12. lemma OAI.Tachikawa.LeftCorner.generator_fixed line 62
  13. lemma OAI.Tachikawa.LeftCorner.hom_ext line 67
  14. def OAI.Tachikawa.LeftCorner.mulRight line 74
  15. lemma OAI.Tachikawa.LeftCorner.mulRight_apply line 79
  16. abbrev OAI.Tachikawa.GroundField line 92
  17. def OAI.Tachikawa.parameter line 94
  18. abbrev OAI.Tachikawa.q line 97
  19. abbrev OAI.Tachikawa.H₁ line 98
  20. abbrev OAI.Tachikawa.H₂ line 99
  21. def OAI.Tachikawa.C line 101
  22. instance OAI.Tachikawa.C.(instance at line 107) line 107
  23. instance OAI.Tachikawa.C.(instance at line 108) line 108
  24. lemma OAI.Tachikawa.C.add_apply line 110
  25. lemma OAI.Tachikawa.C.zero_apply line 111
  26. lemma OAI.Tachikawa.C.neg_apply line 112
  27. lemma OAI.Tachikawa.C.smul_apply line 113
  28. def OAI.Tachikawa.C.mul line 115
  29. def OAI.Tachikawa.C.unit line 128
  30. lemma OAI.Tachikawa.C.ext line 131
  31. lemma OAI.Tachikawa.C.mul_assoc line 133
  32. lemma OAI.Tachikawa.C.unit_mul line 137
  33. lemma OAI.Tachikawa.C.mul_unit line 141
  34. lemma OAI.Tachikawa.C.mul_add line 145
  35. lemma OAI.Tachikawa.C.add_mul line 150
  36. instance OAI.Tachikawa.C.(instance at line 155) line 155
  37. lemma OAI.Tachikawa.C.smul_mul line 173
  38. lemma OAI.Tachikawa.C.mul_smul line 179
  39. instance OAI.Tachikawa.C.(instance at line 185) line 185
  40. instance OAI.Tachikawa.C.(instance at line 187) line 187
  41. def OAI.Tachikawa.C.basis line 201
  42. lemma OAI.Tachikawa.C.basis_apply line 203
  43. def OAI.Tachikawa.C.f line 207
  44. lemma OAI.Tachikawa.C.mul_f line 209
  45. lemma OAI.Tachikawa.C.trace_left_right_f line 214
  46. lemma OAI.Tachikawa.C.trace_left_right_f_eq_zero line 227
  47. def OAI.Tachikawa.C.e line 237
  48. def OAI.Tachikawa.C.u line 238
  49. def OAI.Tachikawa.C.ell line 239
  50. lemma OAI.Tachikawa.C.mul_e line 241
  51. lemma OAI.Tachikawa.C.e_idempotent line 246
  52. lemma OAI.Tachikawa.C.f_idempotent line 247
  53. lemma OAI.Tachikawa.C.u_mul_f line 248
  54. lemma OAI.Tachikawa.C.ell_mul_e line 249
  55. abbrev OAI.Tachikawa.C.Ce line 251
  56. abbrev OAI.Tachikawa.C.Cf line 252
  57. instance OAI.Tachikawa.C.(instance at line 254) line 254
  58. instance OAI.Tachikawa.C.(instance at line 255) line 255
  59. def OAI.Tachikawa.C.ce line 257
  60. def OAI.Tachikawa.C.cf line 259
  61. lemma OAI.Tachikawa.C.ce_eta line 262
  62. lemma OAI.Tachikawa.C.cf_eta line 266
  63. lemma OAI.Tachikawa.C.ce_eq_zero line 270
  64. lemma OAI.Tachikawa.C.cf_eq_zero line 282
  65. def OAI.Tachikawa.C.rhoU line 293
  66. def OAI.Tachikawa.C.rhoEll line 294
  67. lemma OAI.Tachikawa.C.rhoU_ce line 296
  68. lemma OAI.Tachikawa.C.rhoEll_ce line 303
  69. lemma OAI.Tachikawa.C.rhoEll_comp_zero line 315
  70. lemma OAI.Tachikawa.C.rhoU_comp_zero line 320
  71. lemma OAI.Tachikawa.C.exact_rhoEll line 324
  72. lemma OAI.Tachikawa.C.exact_rhoU line 343
  73. def OAI.Tachikawa.RightCorner line 368
  74. lemma OAI.Tachikawa.mem_rightCorner line 374
  75. def OAI.Tachikawa.RightCorner.generator line 380
  76. def OAI.Tachikawa.RightCorner.projection line 381
  77. lemma OAI.Tachikawa.RightCorner.projection_comp_inclusion line 386
  78. lemma OAI.Tachikawa.RightCorner.projective line 391
  79. def OAI.Tachikawa.RightCorner.homEquiv line 396
  80. lemma OAI.Tachikawa.RightCorner.homEquiv_apply line 404
  81. def OAI.Tachikawa.RightCorner.mulLeft line 407
  82. lemma OAI.Tachikawa.RightCorner.mulLeft_apply line 412
  83. lemma OAI.Tachikawa.RightCorner.homEquiv_precomp line 415
  84. def OAI.Tachikawa.RightCorner.lift line 433
  85. lemma OAI.Tachikawa.C.e_mul line 447
  86. lemma OAI.Tachikawa.C.f_mul line 452
  87. lemma OAI.Tachikawa.C.e_mul_u line 457
  88. lemma OAI.Tachikawa.C.e_mul_ell line 458
  89. abbrev OAI.Tachikawa.C.eC line 460
  90. abbrev OAI.Tachikawa.C.fC line 461
  91. instance OAI.Tachikawa.C.(instance at line 463) line 463
  92. instance OAI.Tachikawa.C.(instance at line 464) line 464
  93. def OAI.Tachikawa.C.ec line 466
  94. def OAI.Tachikawa.C.fc line 468
  95. lemma OAI.Tachikawa.C.ec_eta line 471
  96. lemma OAI.Tachikawa.C.fc_eta line 475
  97. lemma OAI.Tachikawa.C.ec_eq_zero line 479
  98. lemma OAI.Tachikawa.C.fc_eq_zero line 491
  99. def OAI.Tachikawa.C.lambdaU line 502
  100. def OAI.Tachikawa.C.lambdaEll line 503
  101. lemma OAI.Tachikawa.C.lambdaU_fc line 506
  102. lemma OAI.Tachikawa.C.lambdaEll_ec line 513
  103. lemma OAI.Tachikawa.C.lambdaU_injective line 520
  104. lemma OAI.Tachikawa.C.exact_lambdaU line 531
  105. lemma OAI.Tachikawa.C.exact_lambdaEll line 549
  106. abbrev OAI.Tachikawa.B line 581
  107. def OAI.Tachikawa.pf line 583
  108. lemma OAI.Tachikawa.trace_left_right_pf line 585
  109. lemma OAI.Tachikawa.end_expansion line 616
  110. lemma OAI.Tachikawa.outer_to_dual_formula line 625
  111. lemma OAI.Tachikawa.outer_central_is_mulLeft line 660
  112. lemma OAI.Tachikawa.outer_factorization_trace line 667
  113. def OAI.Tachikawa.C.character line 704
  114. lemma OAI.Tachikawa.C.character_f line 715
  115. def OAI.Tachikawa.characterB line 718
  116. lemma OAI.Tachikawa.characterB_pf line 720
  117. def OAI.Tachikawa.characterMapB line 723
  118. lemma OAI.Tachikawa.characterMapB_left line 726
  119. lemma OAI.Tachikawa.characterMapB_right line 731
  120. lemma OAI.Tachikawa.characterMapB_one_pf line 736
  121. lemma OAI.Tachikawa.ordinary_factorization_pf_zero line 741
  122. lemma OAI.Tachikawa.characterMapB_not_finite_sum line 758
  123. def OAI.Tachikawa.C.Simple line 787
  124. instance OAI.Tachikawa.C.(instance at line 788) line 788
  125. instance OAI.Tachikawa.C.(instance at line 789) line 789
  126. instance OAI.Tachikawa.C.(instance at line 790) line 790
  127. instance OAI.Tachikawa.C.(instance at line 791) line 791
  128. instance OAI.Tachikawa.C.(instance at line 796) line 796
  129. lemma OAI.Tachikawa.C.simple_smul line 798
  130. lemma OAI.Tachikawa.C.e_smul_simple line 800
  131. lemma OAI.Tachikawa.C.f_smul_simple line 804
  132. def OAI.Tachikawa.C.augmentation line 808
  133. lemma OAI.Tachikawa.C.augmentation_cf line 813
  134. lemma OAI.Tachikawa.C.augmentation_surjective line 815
  135. lemma OAI.Tachikawa.C.augmentation_rhoU line 818
  136. lemma OAI.Tachikawa.C.exact_augmentation line 823
  137. lemma OAI.Tachikawa.C.homCeSimple_zero line 836
  138. instance OAI.Tachikawa.C.(instance at line 842) line 842
  139. lemma OAI.Tachikawa.parameter_ne_zero line 850
  140. lemma OAI.Tachikawa.parameter_pow_ne_one line 856
  141. lemma OAI.Tachikawa.parameter_pow_ne line 866
  142. lemma OAI.Tachikawa.one_add_parameter_pow_ne_zero line 878
  143. def OAI.Tachikawa.C.resObj line 894
  144. def OAI.Tachikawa.C.resD line 898
  145. lemma OAI.Tachikawa.C.resD_exact line 902
  146. def OAI.Tachikawa.C.projectiveResolution line 918
  147. lemma OAI.Tachikawa.C.simple_positive_ext line 924
  148. def OAI.Tachikawa.C.RightSimple line 949
  149. instance OAI.Tachikawa.C.(instance at line 950) line 950
  150. instance OAI.Tachikawa.C.(instance at line 951) line 951
  151. def OAI.Tachikawa.C.rightCharacter line 952
  152. instance OAI.Tachikawa.C.(instance at line 960) line 960
  153. lemma OAI.Tachikawa.C.rightSimple_smul line 964
  154. lemma OAI.Tachikawa.C.dualTwoCycle_coords line 967
  155. def OAI.Tachikawa.C.dualTwoAug line 979
  156. def OAI.Tachikawa.C.dualTwoBoundary line 993
  157. lemma OAI.Tachikawa.C.dualTwoAug_surjective line 999
  158. lemma OAI.Tachikawa.C.exact_dualTwoAug line 1008
  159. def OAI.Tachikawa.C.dualTwoCohomologyEquiv line 1034
  160. lemma OAI.Tachikawa.C.dualComplex_exact line 1043
  161. lemma OAI.Tachikawa.C.hom_rhoU_injective line 1061
  162. lemma OAI.Tachikawa.C.hom_exact_rhoU line 1069
  163. lemma OAI.Tachikawa.C.hom_exact_rhoEll line 1091
  164. lemma OAI.Tachikawa.C.nu_rhoU_surjective line 1117
  165. lemma OAI.Tachikawa.C.nu_resD_exact line 1120