OAI/RingTheory/Tachikawa/Coinduction.lean

GitHub source file

190 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Tachikawa.C.z_fixed_e line 11
2. lemma OAI.Tachikawa.C.v_fixed_e line 17
3. def OAI.Tachikawa.C.rightDualZ line 23
4. def OAI.Tachikawa.C.rightDualV line 26
5. lemma OAI.Tachikawa.C.rightDualZ_ec line 29
6. lemma OAI.Tachikawa.C.rightDualV_ec line 33
7. def OAI.Tachikawa.C.rightDualAug line 37
8. lemma OAI.Tachikawa.C.rightDualAug_surjective line 40
9. lemma OAI.Tachikawa.C.rightDualAug_apply line 52
10. lemma OAI.Tachikawa.C.rightDualAug_eq_zero_iff line 60
11. def OAI.Tachikawa.C.rightDualD₁ line 88
12. lemma OAI.Tachikawa.C.exact_rightDualAug line 93
13. def OAI.Tachikawa.C.rightDualResObj line 125
14. def OAI.Tachikawa.C.rightDualResD line 131
15. lemma OAI.Tachikawa.C.rightDualResD_exact line 136
16. def OAI.Tachikawa.C.rightDualProjectiveResolution line 159
17. lemma OAI.Tachikawa.C.rightDual_projectiveDimension line 166
18. instance OAI.Tachikawa.Construction.(instance at line 195) line 195
19. instance OAI.Tachikawa.Construction.(instance at line 197) line 197
20. instance OAI.Tachikawa.Construction.(instance at line 199) line 199
21. instance OAI.Tachikawa.Construction.(instance at line 201) line 201
22. instance OAI.Tachikawa.Construction.(instance at line 203) line 203
23. instance OAI.Tachikawa.Construction.(instance at line 206) line 206
24. def OAI.Tachikawa.Construction.TLeftObj line 210
25. def OAI.Tachikawa.Construction.TRightObj line 211
26. def OAI.Tachikawa.Construction.tLeftResolution line 213
27. def OAI.Tachikawa.Construction.tRightResolution line 218
28. lemma OAI.Tachikawa.Construction.tLeftResolution_finiteC line 223
29. lemma OAI.Tachikawa.Construction.tRightResolution_finiteC line 241
30. lemma OAI.Tachikawa.Construction.tLeftResolution_finite line 259
31. lemma OAI.Tachikawa.Construction.tRightResolution_finite line 264
32. lemma OAI.Tachikawa.Construction.tLeftResolution_above line 269
33. lemma OAI.Tachikawa.Construction.tRightResolution_above line 280
34. abbrev OAI.Tachikawa.Construction.ELeftObj line 291
35. abbrev OAI.Tachikawa.Construction.ERightObj line 292
36. def OAI.Tachikawa.Construction.eLeftResolution line 295
37. def OAI.Tachikawa.Construction.eRightResolution line 299
38. lemma OAI.Tachikawa.Construction.eLeftResolution_above line 303
39. lemma OAI.Tachikawa.Construction.eRightResolution_above line 307
40. abbrev OAI.Tachikawa.Construction.inclusionC line 320
41. abbrev OAI.Tachikawa.Construction.inclusionB line 322
42. def OAI.Tachikawa.Construction.tLeftUnderlying line 324
43. lemma OAI.Tachikawa.Construction.tLeftUnderlying_smul line 335
44. def OAI.Tachikawa.Construction.eLeftTensorEquiv line 344
45. lemma OAI.Tachikawa.Construction.eLeftTensorEquiv_action line 347
46. lemma OAI.Tachikawa.Construction.eLeftTensorEquiv_smul line 370
47. def OAI.Tachikawa.Construction.eLeftRestrictionIso line 374
48. lemma OAI.Tachikawa.Construction.cResObj_finite line 396
49. abbrev OAI.Tachikawa.Construction.bSimpleTensor line 407
50. def OAI.Tachikawa.Construction.bSimpleTensorResolution line 411
51. def OAI.Tachikawa.Construction.bEvaluatedComparison line 417
52. def OAI.Tachikawa.Construction.inducedBEvaluatedComparison line 423
53. def OAI.Tachikawa.HomBimodule.representationLinear line 440
54. def OAI.Tachikawa.HomBimodule.representation line 448
55. lemma OAI.Tachikawa.HomBimodule.representation_apply line 455
56. lemma OAI.Tachikawa.Construction.homBase_smul line 465
57. abbrev OAI.Tachikawa.Construction.U line 471
58. abbrev OAI.Tachikawa.Construction.S line 472
59. def OAI.Tachikawa.Construction.socleBimoduleLinear line 474
60. def OAI.Tachikawa.Construction.socleBimoduleMap line 484
61. lemma OAI.Tachikawa.Construction.representation_socle line 499
62. lemma OAI.Tachikawa.Construction.socleBimoduleMap_ne_zero line 507
63. def OAI.Tachikawa.LeftCoinduced.J line 524
64. def OAI.Tachikawa.LeftCoinduced.unit line 527
65. instance OAI.Tachikawa.LeftCoinduced.coextend_additive line 530
66. instance OAI.Tachikawa.LeftCoinduced.(instance at line 541) line 541
67. lemma OAI.Tachikawa.LeftCoinduced.unit_injective line 544
68. instance OAI.Tachikawa.LeftCoinduced.(instance at line 549) line 549
69. instance OAI.Tachikawa.LeftCoinduced.(instance at line 551) line 551
70. instance OAI.Tachikawa.LeftCoinduced.coextend_preservesInjective line 553
71. instance OAI.Tachikawa.LeftCoinduced.(instance at line 558) line 558
72. def OAI.Tachikawa.LeftCoinduced.C line 564
73. instance OAI.Tachikawa.LeftCoinduced.(instance at line 566) line 566
74. def OAI.Tachikawa.LeftCoinduced.π line 576
75. instance OAI.Tachikawa.LeftCoinduced.(instance at line 578) line 578
76. lemma OAI.Tachikawa.LeftCoinduced.unit_π line 581
77. def OAI.Tachikawa.LeftCoinduced.short line 584
78. lemma OAI.Tachikawa.LeftCoinduced.short_exact line 586
79. def OAI.Tachikawa.LeftCoinduced.iterate line 591
80. lemma OAI.Tachikawa.LeftCoinduced.c_dimension line 595
81. lemma OAI.Tachikawa.LeftCoinduced.iterate_dimension line 601
82. lemma OAI.Tachikawa.LeftCoinduced.iterate_injective line 610
83. def OAI.Tachikawa.moduleCatObj line 625
84. def OAI.Tachikawa.moduleCatUnderlyingEquiv line 627
85. lemma OAI.Tachikawa.moduleCatFinite line 637
86. def OAI.Tachikawa.LeftCoinduced.restrictRegularEquiv line 649
87. def OAI.Tachikawa.LeftCoinduced.underlying line 660
88. instance OAI.Tachikawa.LeftCoinduced.J_finite line 677
89. instance OAI.Tachikawa.LeftCoinduced.C_finite line 680
90. instance OAI.Tachikawa.LeftCoinduced.iterate_finite line 685
91. def OAI.Tachikawa.Enveloping.Coind line 700
92. instance OAI.Tachikawa.Enveloping.Coind.(instance at line 704) line 704
93. instance OAI.Tachikawa.Enveloping.Coind.(instance at line 705) line 705
94. instance OAI.Tachikawa.Enveloping.Coind.(instance at line 706) line 706
95. instance OAI.Tachikawa.Enveloping.Coind.(instance at line 707) line 707
96. instance OAI.Tachikawa.Enveloping.Coind.(instance at line 708) line 708
97. instance OAI.Tachikawa.Enveloping.Coind.(instance at line 709) line 709
98. instance OAI.Tachikawa.Enveloping.Coind.(instance at line 711) line 711
99. instance OAI.Tachikawa.Enveloping.Coind.(instance at line 722) line 722
100. instance OAI.Tachikawa.Enveloping.Coind.(instance at line 727) line 727
101. instance OAI.Tachikawa.Enveloping.Coind.(instance at line 730) line 730
102. def OAI.Tachikawa.Enveloping.coindObj line 735
103. def OAI.Tachikawa.Enveloping.coindUnderlying line 738
104. instance OAI.Tachikawa.Enveloping.(instance at line 750) line 750
105. def OAI.Tachikawa.Enveloping.coindEvaluate line 756
106. def OAI.Tachikawa.Enveloping.coindExtendLeft line 767
107. lemma OAI.Tachikawa.Enveloping.coindExtendLeft_right line 779
108. def OAI.Tachikawa.Enveloping.coindExtend line 785
109. lemma OAI.Tachikawa.Enveloping.coindEvaluate_extend line 788
110. lemma OAI.Tachikawa.Enveloping.coindExtend_evaluate line 794
111. def OAI.Tachikawa.Enveloping.coindHomEquiv line 805
112. lemma OAI.Tachikawa.Enveloping.coindEvaluate_natural line 818
113. def OAI.Tachikawa.Enveloping.coindMap line 831
114. lemma OAI.Tachikawa.Enveloping.coindMap_apply line 839
115. def OAI.Tachikawa.Enveloping.coindFunctor line 843
116. instance OAI.Tachikawa.Enveloping.(instance at line 849) line 849
117. def OAI.Tachikawa.Enveloping.coindEndo line 852
118. instance OAI.Tachikawa.Enveloping.(instance at line 854) line 854
119. def OAI.Tachikawa.Enveloping.coindUnit line 857
120. lemma OAI.Tachikawa.Enveloping.coindUnit_apply line 860
121. lemma OAI.Tachikawa.Enveloping.coindUnit_injective line 863
122. instance OAI.Tachikawa.Enveloping.(instance at line 871) line 871
123. def OAI.Tachikawa.Enveloping.coindUnitNat line 874
124. def OAI.Tachikawa.Enveloping.coindCoker line 882
125. instance OAI.Tachikawa.Enveloping.(instance at line 885) line 885
126. def OAI.Tachikawa.Enveloping.coindIterate line 895
127. instance OAI.Tachikawa.Enveloping.(instance at line 899) line 899
128. instance OAI.Tachikawa.Enveloping.(instance at line 907) line 907
129. def OAI.Tachikawa.Enveloping.coindπ line 912
130. instance OAI.Tachikawa.Enveloping.(instance at line 916) line 916
131. lemma OAI.Tachikawa.Enveloping.coindUnit_π line 919
132. def OAI.Tachikawa.Enveloping.coindShort line 923
133. lemma OAI.Tachikawa.Enveloping.coindShort_exact line 926
134. lemma OAI.Tachikawa.Enveloping.coindπ_surjective line 932
135. lemma OAI.Tachikawa.Enveloping.coind_exact line 935
136. instance OAI.Tachikawa.Enveloping.coindObj_finite line 940
137. instance OAI.Tachikawa.Enveloping.rightFunctor_finite line 944
138. instance OAI.Tachikawa.Enveloping.coindEndo_finite line 948
139. instance OAI.Tachikawa.Enveloping.coindCoker_finite line 952
140. instance OAI.Tachikawa.Enveloping.coindIterate_finite line 956
141. def OAI.Tachikawa.Enveloping.coindTerm line 963
142. def OAI.Tachikawa.Enveloping.coindStep line 966
143. lemma OAI.Tachikawa.Enveloping.coindStep_exact line 970
144. lemma OAI.Tachikawa.Enveloping.coind_start_exact line 989
145. lemma OAI.Tachikawa.Enveloping.coind_finish_exact line 1004
146. def OAI.Tachikawa.Enveloping.rightRegularObj line 1024
147. def OAI.Tachikawa.Enveloping.rightRegularOne line 1026
148. def OAI.Tachikawa.Enveloping.rightFreeFunctor line 1028
149. instance OAI.Tachikawa.Enveloping.(instance at line 1031) line 1031
150. abbrev OAI.Tachikawa.Enveloping.rightFreeObj line 1034
151. def OAI.Tachikawa.Enveloping.rightFreeEvaluate line 1037
152. def OAI.Tachikawa.Enveloping.rightFreeBilinear line 1048
153. def OAI.Tachikawa.Enveloping.rightFreeExtend line 1061
154. lemma OAI.Tachikawa.Enveloping.rightFreeEvaluate_extend line 1079
155. lemma OAI.Tachikawa.Enveloping.rightFreeExtend_evaluate line 1085
156. def OAI.Tachikawa.Enveloping.rightFreeHomEquiv line 1101
157. lemma OAI.Tachikawa.Enveloping.rightFreeEvaluate_natural line 1109
158. def OAI.Tachikawa.Enveloping.rightFreeUnderlying line 1126
159. def OAI.Tachikawa.Enveloping.rightFreeRestrictionUnderlying line 1131
160. def OAI.Tachikawa.Enveloping.coindTensorUnderlying line 1138
161. lemma OAI.Tachikawa.Enveloping.coindTensorUnderlying_tmul line 1147
162. def OAI.Tachikawa.Enveloping.coindTensorEquiv line 1156
163. def OAI.Tachikawa.Enveloping.coindTensorIso line 1200
164. lemma OAI.Tachikawa.Enveloping.coindTensor_unit line 1205
165. def OAI.Tachikawa.Enveloping.leftResolution line 1234
166. def OAI.Tachikawa.Enveloping.rightResolution line 1243
167. lemma OAI.Tachikawa.Enveloping.coind_ext_zero line 1262
168. lemma OAI.Tachikawa.Enveloping.regular_coind_ext_zero line 1299
169. def OAI.Tachikawa.Enveloping.dualLeftObj line 1320
170. def OAI.Tachikawa.Enveloping.dualLeftUnderlying line 1322
171. instance OAI.Tachikawa.Enveloping.(instance at line 1325) line 1325
172. instance OAI.Tachikawa.Enveloping.(instance at line 1327) line 1327
173. def OAI.Tachikawa.Enveloping.dualRegularObj line 1330
174. def OAI.Tachikawa.Enveloping.dualRegularLeftEquiv line 1333
175. instance OAI.Tachikawa.Enveloping.dualRegularLeftInjective line 1343
176. def OAI.Tachikawa.Enveloping.dualOuterUnderlying line 1349
177. lemma OAI.Tachikawa.Enveloping.dualOuterUnderlying_tmul line 1355
178. def OAI.Tachikawa.Enveloping.dualOuterEquiv line 1358
179. instance OAI.Tachikawa.Enveloping.rightRegularProjective line 1389
180. instance OAI.Tachikawa.Enveloping.rightRegularFinite line 1391
181. lemma OAI.Tachikawa.Enveloping.rightFree_map_exact line 1395
182. lemma OAI.Tachikawa.Enveloping.rightFree_map_surjective line 1403
183. def OAI.Tachikawa.Enveloping.rightFreeResolution line 1410
184. lemma OAI.Tachikawa.Enveloping.rightFreeResolution_d line 1425
185. lemma OAI.Tachikawa.Enveloping.rightFree_ext_zero line 1431
186. def OAI.Tachikawa.Enveloping.ordinaryOuterObj line 1470
187. lemma OAI.Tachikawa.Enveloping.regular_outer_ext_zero line 1473
188. def OAI.Tachikawa.Enveloping.dualLeftFinite line 1481
189. lemma OAI.Tachikawa.Enveloping.outer_dual_ext_zero line 1483
190. theorem OAI.Tachikawa.Enveloping.two_orthogonalities line 1487