OAI/RingTheory/Tachikawa/Bimodule.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Tachikawa.ModuleFiber.obj line 14
2. def OAI.Tachikawa.ModuleFiber.differential line 16
3. lemma OAI.Tachikawa.ModuleFiber.differential_apply line 22
4. lemma OAI.Tachikawa.ModuleFiber.differential_comp line 26
5. def OAI.Tachikawa.ModuleFiber.complex line 47
6. lemma OAI.Tachikawa.ModuleFiber.complex_d line 50
7. lemma OAI.Tachikawa.ModuleFiber.differential_exact line 53
8. lemma OAI.Tachikawa.ModuleFiber.exact line 97
9. lemma OAI.Tachikawa.ModuleFiber.totallyAcyclic line 103
10. lemma OAI.Tachikawa.Construction.forwardJ_finite line 124
11. lemma OAI.Tachikawa.Construction.forwardJ_projective line 135
12. lemma OAI.Tachikawa.Construction.reverseObj_finite line 144
13. lemma OAI.Tachikawa.Construction.reverseObj_projective line 165
14. lemma OAI.Tachikawa.Construction.reverseJ_finite line 175
15. lemma OAI.Tachikawa.Construction.reverseJ_projective line 186
16. lemma OAI.Tachikawa.Construction.forwardJ_below line 194
17. lemma OAI.Tachikawa.Construction.reverseJ_above line 202
18. lemma OAI.Tachikawa.Construction.forwardJJ_finite line 215
19. lemma OAI.Tachikawa.Construction.reverseJJ_finite line 220
20. lemma OAI.Tachikawa.Construction.forwardJJ_projective line 225
21. lemma OAI.Tachikawa.Construction.reverseJJ_projective line 233
22. def OAI.Tachikawa.Construction.jjFiber line 241
23. lemma OAI.Tachikawa.Construction.jjFiber_totallyAcyclic line 244
24. lemma OAI.Tachikawa.Construction.jjFiber_finite line 250
25. lemma OAI.Tachikawa.Construction.jjFiber_projective line 256
26. def OAI.Tachikawa.HomBimodule.Base line 274
27. instance OAI.Tachikawa.HomBimodule.(instance at line 275) line 275
28. instance OAI.Tachikawa.HomBimodule.(instance at line 276) line 276
29. instance OAI.Tachikawa.HomBimodule.(instance at line 277) line 277
30. instance OAI.Tachikawa.HomBimodule.(instance at line 278) line 278
31. instance OAI.Tachikawa.HomBimodule.(instance at line 279) line 279
32. def OAI.Tachikawa.HomBimodule.rightAction line 282
33. instance OAI.Tachikawa.HomBimodule.(instance at line 313) line 313
34. instance OAI.Tachikawa.HomBimodule.(instance at line 314) line 314
35. instance OAI.Tachikawa.HomBimodule.(instance at line 316) line 316
36. def OAI.Tachikawa.HomBimodule.obj line 324
37. lemma OAI.Tachikawa.HomBimodule.tmul_smul_apply line 327
38. lemma OAI.Tachikawa.HomBimodule.left_smul_apply line 331
39. lemma OAI.Tachikawa.HomBimodule.right_smul_apply line 336
40. lemma OAI.Tachikawa.HomBimodule.k_smul_apply line 341
41. def OAI.Tachikawa.BimoduleTensorHom.uncurryLinear line 357
42. lemma OAI.Tachikawa.BimoduleTensorHom.uncurryLinear_balanced line 368
43. def OAI.Tachikawa.BimoduleTensorHom.uncurry line 375
44. lemma OAI.Tachikawa.BimoduleTensorHom.uncurry_mk line 378
45. def OAI.Tachikawa.BimoduleTensorHom.curryLinear line 382
46. lemma OAI.Tachikawa.BimoduleTensorHom.curryLinear_right line 400
47. def OAI.Tachikawa.BimoduleTensorHom.curry line 407
48. lemma OAI.Tachikawa.BimoduleTensorHom.curry_apply line 411
49. lemma OAI.Tachikawa.BimoduleTensorHom.uncurry_curry line 414
50. lemma OAI.Tachikawa.BimoduleTensorHom.curry_uncurry line 420
51. def OAI.Tachikawa.BimoduleTensorHom.equiv line 428
52. lemma OAI.Tachikawa.BimoduleTensorHom.uncurry_precompose line 444
53. def OAI.Tachikawa.HomBimodule.postLinear line 463
54. def OAI.Tachikawa.HomBimodule.postMap line 474
55. lemma OAI.Tachikawa.HomBimodule.postMap_apply line 477
56. lemma OAI.Tachikawa.HomBimodule.postMap_surjective line 480
57. instance OAI.Tachikawa.HomBimodule.(instance at line 488) line 488
58. lemma OAI.Tachikawa.BimoduleTensorHom.uncurry_postcompose line 502
59. instance OAI.Tachikawa.Enveloping.evaluation_projective line 514
60. def OAI.Tachikawa.homBimoduleFunctor line 533
61. def OAI.Tachikawa.evaluationAdjunction line 539
62. lemma OAI.Tachikawa.projective_cokernel_of_injective line 565
63. abbrev OAI.Tachikawa.Enveloping.envelopingForm line 590
64. lemma OAI.Tachikawa.Enveloping.cosyzygy_left_projective line 592
65. lemma OAI.Tachikawa.Enveloping.cosyzygy_right_projective line 610
66. theorem OAI.Tachikawa.Enveloping.negative_side_projective line 628
67. abbrev OAI.Tachikawa.NatCoker.C line 650
68. def OAI.Tachikawa.NatCoker.π line 652
69. def OAI.Tachikawa.NatCoker.ι line 654
70. lemma OAI.Tachikawa.NatCoker.projective_of_contraction line 659
71. lemma OAI.Tachikawa.NatCoker.projective_of_homotopy line 675
72. abbrev OAI.Tachikawa.Enveloping.envelopingMap line 703
73. def OAI.Tachikawa.Enveloping.inducedRegularComplex line 706
74. instance OAI.Tachikawa.Enveloping.inducedRegularComplex_finite line 710
75. instance OAI.Tachikawa.Enveloping.inducedRegularComplex_finiteAlg line 718
76. instance OAI.Tachikawa.Enveloping.inducedRegularComplex_projective line 722
77. instance OAI.Tachikawa.Enveloping.inducedRegularComplex_leftProjective line 728
78. instance OAI.Tachikawa.Enveloping.inducedRegularComplex_rightProjective line 731
79. def OAI.Tachikawa.Enveloping.inducedCokerFive line 734
80. def OAI.Tachikawa.Enveloping.inducedY line 738
81. def OAI.Tachikawa.restrictionUnderlyingEquiv line 751
82. def OAI.Tachikawa.homBimoduleRestrictionEquiv line 762
83. def OAI.Tachikawa.homBimoduleRestrictionIso line 786
84. def OAI.Tachikawa.homBimoduleRestriction line 791
85. def OAI.Tachikawa.AlgebraInduction.adjunction line 813
86. def OAI.Tachikawa.AlgebraInduction.compositionIso line 827
87. lemma OAI.Tachikawa.Enveloping.leftFunctor_eq line 842
88. lemma OAI.Tachikawa.Enveloping.rightFunctor_eq line 844
89. lemma OAI.Tachikawa.Enveloping.leftFunctor_map_exact line 847
90. lemma OAI.Tachikawa.Enveloping.rightFunctor_map_exact line 851
91. instance OAI.Tachikawa.Enveloping.(instance at line 856) line 856
92. instance OAI.Tachikawa.Enveloping.(instance at line 860) line 860
93. instance OAI.Tachikawa.Enveloping.(instance at line 864) line 864
94. instance OAI.Tachikawa.Enveloping.(instance at line 868) line 868