OAI/RingTheory/Tachikawa/RightInduction.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Tachikawa.Enveloping.rightEvaluation line 13
2. instance OAI.Tachikawa.Enveloping.(instance at line 28) line 28
3. def OAI.Tachikawa.Enveloping.rightObjEquiv line 37
4. def OAI.Tachikawa.Enveloping.rightEvaluationEquiv line 46
5. lemma OAI.Tachikawa.Enveloping.rightEvaluationEquiv_mk line 71
6. def OAI.Tachikawa.Enveloping.evalScalarEquiv line 76
7. def OAI.Tachikawa.Enveloping.rightEvaluationComparisonIso line 87
8. def OAI.Tachikawa.Enveloping.rightEvaluationComparison line 92
9. def OAI.Tachikawa.Enveloping.regularEvalBilinear line 119
10. def OAI.Tachikawa.Enveloping.regularEval line 130
11. lemma OAI.Tachikawa.Enveloping.regularTensor_move line 136
12. def OAI.Tachikawa.Enveloping.regularEvalInv line 151
13. def OAI.Tachikawa.Enveloping.regularEvalIso line 167
14. abbrev OAI.Tachikawa.Enveloping.leftIndObj line 193
15. def OAI.Tachikawa.Enveloping.leftIndMap line 197
16. def OAI.Tachikawa.Enveloping.leftIndFunctor line 210
17. instance OAI.Tachikawa.Enveloping.(instance at line 234) line 234
18. def OAI.Tachikawa.Enveloping.leftIndUnderlyingIso line 250
19. def OAI.Tachikawa.Enveloping.RightObj line 277
20. instance OAI.Tachikawa.Enveloping.(instance at line 278) line 278
21. instance OAI.Tachikawa.Enveloping.(instance at line 280) line 280
22. instance OAI.Tachikawa.Enveloping.(instance at line 282) line 282
23. instance OAI.Tachikawa.Enveloping.(instance at line 284) line 284
24. instance OAI.Tachikawa.Enveloping.(instance at line 286) line 286
25. instance OAI.Tachikawa.Enveloping.(instance at line 288) line 288
26. instance OAI.Tachikawa.Enveloping.(instance at line 290) line 290
27. def OAI.Tachikawa.Enveloping.rightObjMap line 296
28. def OAI.Tachikawa.Enveloping.rightObjLeftMap line 299
29. def OAI.Tachikawa.BalancedTensor.commutingAction line 316
30. def OAI.Tachikawa.Enveloping.RightIndType line 339
31. instance OAI.Tachikawa.Enveloping.(instance at line 343) line 343
32. instance OAI.Tachikawa.Enveloping.(instance at line 346) line 346
33. instance OAI.Tachikawa.Enveloping.(instance at line 349) line 349
34. instance OAI.Tachikawa.Enveloping.(instance at line 352) line 352
35. instance OAI.Tachikawa.Enveloping.(instance at line 355) line 355
36. instance OAI.Tachikawa.Enveloping.(instance at line 360) line 360
37. instance OAI.Tachikawa.Enveloping.(instance at line 374) line 374
38. abbrev OAI.Tachikawa.Enveloping.rightIndObj line 383
39. abbrev OAI.Tachikawa.Enveloping.rightEnvelopingMap line 386
40. lemma OAI.Tachikawa.Enveloping.rightInd_smul_mk line 392
41. lemma OAI.Tachikawa.Enveloping.rightInd_smul_tmul line 397
42. def OAI.Tachikawa.Enveloping.rightIndUnit line 401
43. def OAI.Tachikawa.Enveloping.rightIndMapLinear line 431
44. def OAI.Tachikawa.Enveloping.rightIndMap line 454
45. lemma OAI.Tachikawa.Enveloping.rightInd_hom_ext line 461
46. def OAI.Tachikawa.Enveloping.rightIndFunctor line 476
47. instance OAI.Tachikawa.Enveloping.(instance at line 482) line 482
48. def OAI.Tachikawa.Enveloping.rightIndUnderlyingIso line 489
49. def OAI.Tachikawa.Enveloping.rightIndUnderlyingComparison line 502
50. def OAI.Tachikawa.Enveloping.rightIndResMap line 509
51. lemma OAI.Tachikawa.Enveloping.rightIndResMap_left line 522
52. def OAI.Tachikawa.Enveloping.rightIndExtendRightLinear line 532
53. lemma OAI.Tachikawa.Enveloping.rightIndExtendRightLinear_left line 537
54. def OAI.Tachikawa.Enveloping.rightIndExtendLinear line 559
55. def OAI.Tachikawa.Enveloping.rightReassembleIso line 566
56. def OAI.Tachikawa.Enveloping.rightIndExtend line 582
57. def OAI.Tachikawa.Enveloping.rightIndComparisonHom line 591
58. def OAI.Tachikawa.Enveloping.rightIndComparisonInv line 596
59. lemma OAI.Tachikawa.Enveloping.rightIndComparison_inv_unit line 603
60. lemma OAI.Tachikawa.Enveloping.rightIndComparison_hom_unit line 610
61. lemma OAI.Tachikawa.Enveloping.rightIndComparison_hom_inv line 616
62. lemma OAI.Tachikawa.Enveloping.rightIndComparison_inv_hom line 626
63. def OAI.Tachikawa.Enveloping.rightIndComparisonIso line 646
64. def OAI.Tachikawa.Enveloping.rightIndComparison line 653
65. lemma OAI.Tachikawa.exact_prodMap line 673
66. lemma OAI.Tachikawa.ProjectiveResolution.function_exact_succ line 695
67. lemma OAI.Tachikawa.ProjectiveResolution.function_exact_zero line 699
68. def OAI.Tachikawa.ProjectiveResolution.prod line 702
69. def OAI.Tachikawa.ProjectiveResolution.simpleTerm line 728
70. def OAI.Tachikawa.ProjectiveResolution.simpleAug line 732
71. def OAI.Tachikawa.ProjectiveResolution.simpleSelf line 734
72. lemma OAI.Tachikawa.ProjectiveResolution.simpleSelf_above line 745
73. lemma OAI.Tachikawa.ProjectiveResolution.simpleSelf_finite line 752
74. lemma OAI.Tachikawa.ProjectiveResolution.prod_above line 762
75. lemma OAI.Tachikawa.ProjectiveResolution.prod_finite line 771
76. def OAI.Tachikawa.Enveloping.leftResolutionOf line 789
77. def OAI.Tachikawa.Enveloping.rightResolutionOf line 802
78. lemma OAI.Tachikawa.map_resolution_quasiIso line 825
79. lemma OAI.Tachikawa.quasiIso_map_natIso line 843
80. instance OAI.Tachikawa.Enveloping.regular_right_projective line 860
81. instance OAI.Tachikawa.Enveloping.regular_left_projective line 864
82. instance OAI.Tachikawa.Enveloping.rightFunctor_reflectsIsomorphisms line 867
83. instance OAI.Tachikawa.Enveloping.leftFunctor_reflectsIsomorphisms line 872
84. lemma OAI.Tachikawa.Enveloping.right_induction_regular_quasiIso line 878
85. def OAI.Tachikawa.Enveloping.rightInducedResolution line 909
86. lemma OAI.Tachikawa.Enveloping.regular_evaluation_quasiIso line 935
87. def OAI.Tachikawa.Enveloping.evaluatedRegularResolution line 971
88. def OAI.Tachikawa.Enveloping.evaluatedRegularComparison line 995
89. def OAI.Tachikawa.Enveloping.inductionEvaluation line 1009
90. def OAI.Tachikawa.Enveloping.evaluatedInducedRegularIso line 1021
91. def OAI.Tachikawa.Enveloping.evaluatedInducedRegularComparison line 1028