OAI/RingTheory/Tachikawa/Nakayama.lean

GitHub source file

149 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Tachikawa.homologyMap_eq_of_component line 11
2. lemma OAI.Tachikawa.homologyMap_eq_scalar line 20
3. lemma OAI.Tachikawa.homologyMap_scalar_of_conjugate line 32
4. instance OAI.Tachikawa.VectorSplit.tensorFunctor_linear line 47
5. lemma OAI.Tachikawa.VectorSplit.tensor_conjugate_component line 56
6. lemma OAI.Tachikawa.VectorSplit.tensor_homology_scalar line 83
7. lemma OAI.Tachikawa.resolutionHomologyExtAll_quotient line 104
8. lemma OAI.Tachikawa.resolutionTwistHom_scalar line 121
9. lemma OAI.Tachikawa.component_scalar_of_homologyMap line 163
10. lemma OAI.Tachikawa.conjugate_scalar_of_homologyMap line 176
11. lemma OAI.Tachikawa.homologyMap_scalar_of_intertwine line 185
12. lemma OAI.Tachikawa.extTwist_scalar_of_homologyMap line 207
13. def OAI.Tachikawa.rightMultiply line 245
14. lemma OAI.Tachikawa.rightMultiply_apply line 250
15. def OAI.Tachikawa.Nakayama line 252
16. instance OAI.Tachikawa.Nakayama.(instance at line 256) line 256
17. instance OAI.Tachikawa.Nakayama.(instance at line 257) line 257
18. instance OAI.Tachikawa.Nakayama.(instance at line 258) line 258
19. instance OAI.Tachikawa.Nakayama.(instance at line 259) line 259
20. lemma OAI.Tachikawa.Nakayama.ext line 260
21. def OAI.Tachikawa.Nakayama.homRight line 262
22. lemma OAI.Tachikawa.Nakayama.homRight_apply line 267
23. instance OAI.Tachikawa.Nakayama.(instance at line 269) line 269
24. lemma OAI.Tachikawa.Nakayama.action_apply line 294
25. lemma OAI.Tachikawa.Nakayama.add_apply line 296
26. lemma OAI.Tachikawa.Nakayama.zero_apply line 297
27. lemma OAI.Tachikawa.Nakayama.smul_apply line 298
28. instance OAI.Tachikawa.Nakayama.(instance at line 300) line 300
29. def OAI.Tachikawa.Nakayama.evaluationBilinear line 313
30. lemma OAI.Tachikawa.Nakayama.evaluationBilinear_apply line 332
31. lemma OAI.Tachikawa.Nakayama.evaluation_balanced line 335
32. def OAI.Tachikawa.Nakayama.evaluation line 340
33. lemma OAI.Tachikawa.Nakayama.evaluation_mk line 344
34. def OAI.Tachikawa.Nakayama.map line 349
35. lemma OAI.Tachikawa.Nakayama.map_apply line 364
36. lemma OAI.Tachikawa.Nakayama.evaluation_natural line 368
37. def OAI.Tachikawa.Nakayama.paired line 378
38. def OAI.Tachikawa.Nakayama.transposeFun line 395
39. lemma OAI.Tachikawa.Nakayama.transposeFun_eval line 398
40. def OAI.Tachikawa.Nakayama.transpose line 402
41. lemma OAI.Tachikawa.Nakayama.transpose_evaluation line 420
42. lemma OAI.Tachikawa.Nakayama.evaluation_injective line 427
43. lemma OAI.Tachikawa.Nakayama.evaluation_surjective line 437
44. def OAI.Tachikawa.Nakayama.evaluationEquiv line 462
45. def OAI.Tachikawa.Nakayama.rankOne line 475
46. lemma OAI.Tachikawa.Nakayama.rankOne_apply line 480
47. def OAI.Tachikawa.Nakayama.coevaluation line 482
48. lemma OAI.Tachikawa.Nakayama.coevaluation_apply line 516
49. lemma OAI.Tachikawa.Nakayama.decomposed line 523
50. lemma OAI.Tachikawa.Nakayama.rankOne_sum line 531
51. def OAI.Tachikawa.Nakayama.homPair line 537
52. lemma OAI.Tachikawa.Nakayama.homPair_coevaluation line 550
53. lemma OAI.Tachikawa.Nakayama.coevaluation_homPair line 557
54. lemma OAI.Tachikawa.Nakayama.coevaluation_bijective line 569
55. def OAI.Tachikawa.Nakayama.homDualEquiv line 576
56. lemma OAI.Tachikawa.exact_dual line 589
57. def OAI.Tachikawa.homPrecomp line 604
58. lemma OAI.Tachikawa.homPrecomp_apply line 609
59. lemma OAI.Tachikawa.Nakayama.coevaluation_natural_left line 613
60. lemma OAI.Tachikawa.Nakayama.coevaluation_natural_right line 618
61. lemma OAI.Tachikawa.Nakayama.coevaluation_homDualEquiv line 627
62. lemma OAI.Tachikawa.Nakayama.homDualEquiv_coevaluation line 631
63. lemma OAI.Tachikawa.Nakayama.homDualEquiv_natural_left line 635
64. instance OAI.Tachikawa.Nakayama.injective line 642
65. lemma OAI.Tachikawa.Nakayama.map_id line 668
66. lemma OAI.Tachikawa.Nakayama.map_zero line 672
67. lemma OAI.Tachikawa.Nakayama.map_comp line 677
68. def OAI.Tachikawa.Nakayama.functor line 693
69. instance OAI.Tachikawa.Nakayama.(instance at line 699) line 699
70. def OAI.Tachikawa.Nakayama.complex line 707
71. lemma OAI.Tachikawa.Nakayama.complex_exact line 710
72. lemma OAI.Tachikawa.Nakayama.homPrecomp_exact line 731
73. lemma OAI.Tachikawa.Nakayama.map_exact line 751
74. lemma OAI.Tachikawa.Nakayama.map_surjective line 756
75. def OAI.Tachikawa.TrivialInduction.Obj line 776
76. instance OAI.Tachikawa.TrivialInduction.(instance at line 779) line 779
77. instance OAI.Tachikawa.TrivialInduction.(instance at line 780) line 780
78. instance OAI.Tachikawa.TrivialInduction.(instance at line 781) line 781
79. instance OAI.Tachikawa.TrivialInduction.(instance at line 782) line 782
80. def OAI.Tachikawa.TrivialInduction.act line 784
81. instance OAI.Tachikawa.TrivialInduction.(instance at line 787) line 787
82. lemma OAI.Tachikawa.TrivialInduction.inl_smul line 830
83. instance OAI.Tachikawa.TrivialInduction.(instance at line 838) line 838
84. def OAI.Tachikawa.TrivialInduction.unit line 843
85. def OAI.Tachikawa.TrivialInduction.first line 844
86. def OAI.Tachikawa.TrivialInduction.second line 845
87. lemma OAI.Tachikawa.TrivialInduction.unit_apply line 848
88. lemma OAI.Tachikawa.TrivialInduction.first_apply line 850
89. lemma OAI.Tachikawa.TrivialInduction.second_apply line 852
90. def OAI.Tachikawa.TrivialInduction.map line 854
91. lemma OAI.Tachikawa.TrivialInduction.map_apply line 866
92. lemma OAI.Tachikawa.TrivialInduction.map_surjective line 869
93. lemma OAI.Tachikawa.TrivialInduction.map_exact line 876
94. def OAI.Tachikawa.TrivialInduction.coordinateHom line 898
95. lemma OAI.Tachikawa.TrivialInduction.coordinateHom_apply line 903
96. lemma OAI.Tachikawa.TrivialInduction.sum_coordinateHom line 906
97. def OAI.Tachikawa.TrivialInduction.freeMap line 916
98. lemma OAI.Tachikawa.TrivialInduction.freeMap_first line 921
99. lemma OAI.Tachikawa.TrivialInduction.freeMap_second line 929
100. lemma OAI.Tachikawa.TrivialInduction.freeMap_second_apply line 938
101. def OAI.Tachikawa.TrivialInduction.freeInv line 944
102. lemma OAI.Tachikawa.TrivialInduction.freeMap_freeInv line 947
103. lemma OAI.Tachikawa.TrivialInduction.freeInv_freeMap line 956
104. def OAI.Tachikawa.TrivialInduction.freeEquiv line 967
105. instance OAI.Tachikawa.TrivialInduction.(instance at line 971) line 971
106. lemma OAI.Tachikawa.TrivialInduction.map_id line 976
107. lemma OAI.Tachikawa.TrivialInduction.map_comp line 982
108. instance OAI.Tachikawa.TrivialInduction.inducedProjective line 987
109. def OAI.Tachikawa.TrivialInduction.restrict line 1004
110. lemma OAI.Tachikawa.TrivialInduction.restrict_apply line 1011
111. def OAI.Tachikawa.TrivialInduction.lift line 1014
112. lemma OAI.Tachikawa.TrivialInduction.lift_unit line 1042
113. lemma OAI.Tachikawa.TrivialInduction.restrict_lift line 1048
114. lemma OAI.Tachikawa.TrivialInduction.hom_ext line 1054
115. lemma OAI.Tachikawa.TrivialInduction.lift_restrict line 1082
116. lemma OAI.Tachikawa.TrivialInduction.restrict_injective line 1085
117. lemma OAI.Tachikawa.TrivialInduction.map_unit line 1092
118. lemma OAI.Tachikawa.TrivialInduction.restrict_comp line 1098
119. lemma OAI.Tachikawa.Nakayama.hom_map_exact line 1121
120. def OAI.Tachikawa.Nakayama.cokerEquiv line 1141
121. def OAI.Tachikawa.Nakayama.injectiveTail line 1151
122. lemma OAI.Tachikawa.Nakayama.injectiveTail_d line 1180
123. lemma OAI.Tachikawa.Nakayama.ext_negative line 1188
124. lemma OAI.Tachikawa.boundaries_of_ext_subsingleton line 1220
125. lemma OAI.Tachikawa.ext_subsingleton_target_iso line 1227
126. instance OAI.Tachikawa.TrivialInduction.nakayamaFinite line 1245
127. instance OAI.Tachikawa.TrivialInduction.inducedFinite line 1252
128. lemma OAI.Tachikawa.TrivialInduction.projective_of_inducedProjective line 1255
129. def OAI.Tachikawa.TrivialInduction.inducedResolution line 1267
130. lemma OAI.Tachikawa.TrivialInduction.inducedResolution_d line 1288
131. theorem OAI.Tachikawa.TrivialInduction.transfer line 1295
132. def OAI.Tachikawa.TrivialInflation line 1352
133. instance OAI.Tachikawa.TrivialInflation.(instance at line 1358) line 1358
134. instance OAI.Tachikawa.TrivialInflation.(instance at line 1359) line 1359
135. instance OAI.Tachikawa.TrivialInflation.(instance at line 1360) line 1360
136. instance OAI.Tachikawa.TrivialInflation.(instance at line 1361) line 1361
137. instance OAI.Tachikawa.TrivialInflation.(instance at line 1362) line 1362
138. instance OAI.Tachikawa.TrivialInflation.(instance at line 1364) line 1364
139. instance OAI.Tachikawa.TrivialInflation.(instance at line 1368) line 1368
140. lemma OAI.Tachikawa.TrivialInflation.smul_def line 1372
141. lemma OAI.Tachikawa.TrivialInflation.inl_smul line 1376
142. lemma OAI.Tachikawa.TrivialInflation.inr_smul line 1380
143. def OAI.Tachikawa.TrivialInflation.map line 1383
144. def OAI.Tachikawa.TrivialInflation.restrict line 1388
145. def OAI.Tachikawa.TrivialInflation.lift line 1395
146. lemma OAI.Tachikawa.TrivialInflation.restrict_lift line 1401
147. lemma OAI.Tachikawa.TrivialInflation.lift_restrict line 1404
148. def OAI.Tachikawa.TrivialInflation.homEquiv line 1431
149. lemma OAI.Tachikawa.TrivialInflation.restrict_comp line 1441