OAI/RingTheory/Tachikawa/OuterTensor.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Tachikawa.OuterTensor.map_add_left line 13
2. lemma OAI.Tachikawa.OuterTensor.map_add_right line 20
3. instance OAI.Tachikawa.OuterTensor.(instance at line 27) line 27
4. instance OAI.Tachikawa.OuterTensor.(instance at line 30) line 30
5. abbrev OAI.Tachikawa.TotalMap.map₂ line 48
6. instance OAI.Tachikawa.TotalMap.sourceHasCoproduct line 53
7. instance OAI.Tachikawa.TotalMap.targetHasCoproduct line 57
8. abbrev OAI.Tachikawa.TotalMap.compareX line 61
9. lemma OAI.Tachikawa.TotalMap.ι_compareX line 65
10. lemma OAI.Tachikawa.TotalMap.ιOrZero_compareX line 73
11. lemma OAI.Tachikawa.TotalMap.d₁_compareX line 80
12. lemma OAI.Tachikawa.TotalMap.d₂_compareX line 89
13. def OAI.Tachikawa.TotalMap.comparison line 98
14. instance OAI.Tachikawa.TotalMap.(instance at line 110) line 110
15. instance OAI.Tachikawa.TotalMap.(instance at line 117) line 117
16. def OAI.Tachikawa.TotalMap.iso line 122
17. abbrev OAI.Tachikawa.OuterTensor.forgetA line 135
18. abbrev OAI.Tachikawa.OuterTensor.forgetB line 136
19. abbrev OAI.Tachikawa.OuterTensor.forgetE line 137
20. abbrev OAI.Tachikawa.OuterTensor.tensorF line 138
21. def OAI.Tachikawa.OuterTensor.forgetObjIso line 140
22. lemma OAI.Tachikawa.OuterTensor.forgetObjIso_natural line 156
23. lemma OAI.Tachikawa.OuterTensor.forgetBifunctor_natural line 171
24. abbrev OAI.Tachikawa.OuterTensor.outerBicomplex line 197
25. abbrev OAI.Tachikawa.OuterTensor.vectorBicomplex line 198
26. def OAI.Tachikawa.OuterTensor.forgetBicomplexIso line 202
27. def OAI.Tachikawa.OuterTensor.forgetTotalIso line 235
28. lemma OAI.Tachikawa.OuterTensor.ι_forgetTotalIso line 244
29. lemma OAI.Tachikawa.OuterTensor.forgetTotalIso_natural line 272
30. lemma OAI.Tachikawa.AlgebraInduction.res_map_exact line 309
31. instance OAI.Tachikawa.AlgebraInduction.(instance at line 314) line 314
32. instance OAI.Tachikawa.AlgebraInduction.(instance at line 317) line 317
33. def OAI.Tachikawa.OuterTensor.freeObj line 330
34. def OAI.Tachikawa.OuterTensor.underlyingFree line 332
35. def OAI.Tachikawa.OuterTensor.freeEquivLinear line 343
36. lemma OAI.Tachikawa.OuterTensor.freeEquivLinear_tmul line 350
37. lemma OAI.Tachikawa.OuterTensor.freeEquivLinear_action line 354
38. def OAI.Tachikawa.OuterTensor.freeEquiv line 369
39. instance OAI.Tachikawa.OuterTensor.freeProjective line 375
40. lemma OAI.Tachikawa.OuterTensor.projective line 380
41. def OAI.Tachikawa.OuterTensor.morphism line 408
42. lemma OAI.Tachikawa.OuterTensor.map_smul_left line 412
43. lemma OAI.Tachikawa.OuterTensor.map_smul_right line 430
44. def OAI.Tachikawa.OuterTensor.homMap line 448
45. lemma OAI.Tachikawa.OuterTensor.homMap_tmul line 458
46. def OAI.Tachikawa.OuterTensor.restrictHom line 461
47. lemma OAI.Tachikawa.OuterTensor.restrictHom_injective line 466
48. def OAI.Tachikawa.OuterTensor.underlyingHom line 470
49. lemma OAI.Tachikawa.OuterTensor.homMap_underlying line 481
50. lemma OAI.Tachikawa.OuterTensor.homMap_injective line 492
51. def OAI.Tachikawa.AlgebraInduction.unitLinear line 511
52. lemma OAI.Tachikawa.AlgebraInduction.unitLinear_smul line 521
53. abbrev OAI.Tachikawa.OuterTensor.inductionTarget line 533
54. def OAI.Tachikawa.OuterTensor.inductionUnit line 536
55. def OAI.Tachikawa.OuterTensor.inductionComparison line 561
56. lemma OAI.Tachikawa.OuterTensor.inductionComparison_pure line 566
57. lemma OAI.Tachikawa.OuterTensor.inductionComparison_surjective line 574
58. lemma OAI.Tachikawa.OuterTensor.inductionComparison_natural line 607
59. def OAI.Tachikawa.BalancedTensor.liftGround line 647
60. lemma OAI.Tachikawa.BalancedTensor.liftGround_mk line 652
61. theorem OAI.Tachikawa.BalancedTensor.hom_ext_ground line 658
62. lemma OAI.Tachikawa.BalancedTensor.liftGround_add line 668
63. lemma OAI.Tachikawa.BalancedTensor.liftGround_smul line 677
64. abbrev OAI.Tachikawa.OuterTensor.inductionSource line 696
65. def OAI.Tachikawa.OuterTensor.underlyingEquiv line 699
66. def OAI.Tachikawa.OuterTensor.inductionSourceMk line 709
67. def OAI.Tachikawa.OuterTensor.inductionPure line 717
68. lemma OAI.Tachikawa.OuterTensor.inductionPure_balance_left line 764
69. lemma OAI.Tachikawa.OuterTensor.inductionPure_balance_right line 783
70. def OAI.Tachikawa.OuterTensor.inductionLeftLift line 803
71. lemma OAI.Tachikawa.OuterTensor.inductionLeftLift_mk line 808
72. lemma OAI.Tachikawa.OuterTensor.inductionLeftLift_balance line 813
73. def OAI.Tachikawa.OuterTensor.inductionRightLift line 822
74. lemma OAI.Tachikawa.OuterTensor.inductionRightLift_add line 829
75. lemma OAI.Tachikawa.OuterTensor.inductionRightLift_smul line 837
76. def OAI.Tachikawa.OuterTensor.inductionInverseBilinear line 844
77. def OAI.Tachikawa.OuterTensor.inductionInverseLinear line 852
78. lemma OAI.Tachikawa.OuterTensor.inductionInverseLinear_pure line 859
79. lemma OAI.Tachikawa.OuterTensor.inductionInverse_comparison_pure line 866
80. lemma OAI.Tachikawa.OuterTensor.inductionInverse_comparison line 885
81. lemma OAI.Tachikawa.OuterTensor.inductionComparison_injective line 917
82. def OAI.Tachikawa.OuterTensor.inductionIso line 923
83. lemma OAI.Tachikawa.OuterTensor.inductionIso_hom line 927
84. abbrev OAI.Tachikawa.OuterTensor.algebraTwist line 939
85. def OAI.Tachikawa.OuterTensor.restrictionGround line 942
86. def OAI.Tachikawa.OuterTensor.twistObjIso line 954
87. lemma OAI.Tachikawa.OuterTensor.twistObjIso_natural line 982
88. abbrev OAI.Tachikawa.OuterTensor.twistComplex line 1006
89. def OAI.Tachikawa.OuterTensor.twistBicomplexIso line 1010
90. def OAI.Tachikawa.OuterTensor.twistTotalIso line 1043
91. lemma OAI.Tachikawa.OuterTensor.ι_twistTotalIso line 1050
92. def OAI.Tachikawa.OuterTensor.freeBasis line 1076
93. def OAI.Tachikawa.OuterTensor.freeTensorBasis line 1078
94. def OAI.Tachikawa.OuterTensor.freeAt line 1081
95. lemma OAI.Tachikawa.OuterTensor.freeAt_single line 1089
96. def OAI.Tachikawa.OuterTensor.freeValue line 1098
97. def OAI.Tachikawa.OuterTensor.freeLift line 1103
98. lemma OAI.Tachikawa.OuterTensor.freeLift_single_component line 1110
99. lemma OAI.Tachikawa.OuterTensor.homMap_freeLift_single line 1131
100. lemma OAI.Tachikawa.OuterTensor.freeEquiv_single line 1155
101. lemma OAI.Tachikawa.OuterTensor.freeHom_ext line 1163
102. lemma OAI.Tachikawa.OuterTensor.homMap_freeLift line 1190
103. lemma OAI.Tachikawa.OuterTensor.homMap_free_surjective line 1195
104. lemma OAI.Tachikawa.OuterTensor.morphism_comp line 1208
105. lemma OAI.Tachikawa.OuterTensor.morphism_id line 1213
106. def OAI.Tachikawa.OuterTensor.precompose line 1217
107. lemma OAI.Tachikawa.OuterTensor.homMap_precompose line 1222
108. lemma OAI.Tachikawa.OuterTensor.homMap_surjective line 1232
109. def OAI.Tachikawa.OuterTensor.homEquiv line 1251