OAI/RingTheory/Tachikawa/Tensor.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Tachikawa.BalancedTensor.relations line 18
2. abbrev OAI.Tachikawa.BalancedTensor.T line 22
3. def OAI.Tachikawa.BalancedTensor.mk line 24
4. lemma OAI.Tachikawa.BalancedTensor.balance line 28
5. def OAI.Tachikawa.BalancedTensor.lift line 39
6. lemma OAI.Tachikawa.BalancedTensor.lift_mk line 50
7. theorem OAI.Tachikawa.BalancedTensor.induction_on line 54
8. theorem OAI.Tachikawa.BalancedTensor.hom_ext line 68
9. instance OAI.Tachikawa.BalancedTensor.(instance at line 77) line 77
10. def OAI.Tachikawa.BalancedTensor.mapRightBilinear line 100
11. lemma OAI.Tachikawa.BalancedTensor.mapRightBilinear_balanced line 104
12. def OAI.Tachikawa.BalancedTensor.mapRight line 110
13. lemma OAI.Tachikawa.BalancedTensor.mapRight_mk line 115
14. lemma OAI.Tachikawa.BalancedTensor.mapRight_id line 118
15. lemma OAI.Tachikawa.BalancedTensor.mapRight_comp line 124
16. lemma OAI.Tachikawa.BalancedTensor.mapRight_add line 131
17. lemma OAI.Tachikawa.BalancedTensor.mapRight_zero line 137
18. lemma OAI.Tachikawa.BalancedTensor.mapRight_surjective line 142
19. lemma OAI.Tachikawa.BalancedTensor.mapRight_split line 155
20. def OAI.Tachikawa.BalancedTensor.rightUnit line 161
21. lemma OAI.Tachikawa.BalancedTensor.rightUnit_mk line 176
22. def OAI.Tachikawa.BalancedTensor.rightUnitInv line 179
23. def OAI.Tachikawa.BalancedTensor.rightUnitEquiv line 184
24. def OAI.Tachikawa.BalancedTensor.mapLeft line 206
25. lemma OAI.Tachikawa.BalancedTensor.mapLeft_mk line 215
26. lemma OAI.Tachikawa.BalancedTensor.mapLeft_id line 219
27. lemma OAI.Tachikawa.BalancedTensor.mapLeft_comp line 225
28. lemma OAI.Tachikawa.BalancedTensor.mapLeft_add line 234
29. lemma OAI.Tachikawa.BalancedTensor.mapLeft_zero line 244
30. lemma OAI.Tachikawa.BalancedTensor.fieldRelations_smul_mem line 261
31. lemma OAI.Tachikawa.BalancedTensor.relations_restrictScalars line 278
32. def OAI.Tachikawa.BalancedTensor.restrictEquiv line 294
33. lemma OAI.Tachikawa.BalancedTensor.restrictEquiv_mk line 301
34. def OAI.Tachikawa.BalancedTensor.leftUnit line 314
35. lemma OAI.Tachikawa.BalancedTensor.leftUnit_mk line 320
36. def OAI.Tachikawa.BalancedTensor.leftUnitEquiv line 322
37. def OAI.Tachikawa.BalancedTensor.freeEval line 335
38. lemma OAI.Tachikawa.BalancedTensor.freeEval_mk line 346
39. def OAI.Tachikawa.BalancedTensor.freeInv line 349
40. lemma OAI.Tachikawa.BalancedTensor.freeEval_freeInv line 353
41. lemma OAI.Tachikawa.BalancedTensor.freeInv_freeEval line 358
42. def OAI.Tachikawa.BalancedTensor.freeEquiv line 373
43. lemma OAI.Tachikawa.BalancedTensor.freeEquiv_mapRight line 378
44. lemma OAI.Tachikawa.BalancedTensor.mapLeft_mapRight line 404
45. lemma OAI.Tachikawa.BalancedTensor.restrictEquiv_mapRight line 413
46. def OAI.Tachikawa.BalancedTensor.oppositeFree line 422
47. lemma OAI.Tachikawa.BalancedTensor.free_mapRight_exact line 430
48. lemma OAI.Tachikawa.BalancedTensor.field_mapRight_exact line 453
49. lemma OAI.Tachikawa.BalancedTensor.mapRight_exact line 494
50. def OAI.Tachikawa.BalancedTensor.rightFreeEval line 523
51. lemma OAI.Tachikawa.BalancedTensor.rightFreeEval_mk line 528
52. def OAI.Tachikawa.BalancedTensor.rightFreeInv line 531
53. lemma OAI.Tachikawa.BalancedTensor.rightFreeEval_inv line 535
54. lemma OAI.Tachikawa.BalancedTensor.rightFreeInv_eval line 546
55. def OAI.Tachikawa.BalancedTensor.rightFreeEquiv line 561
56. lemma OAI.Tachikawa.BalancedTensor.map_projective line 569
57. def OAI.Tachikawa.BalancedTensor.functor line 590
58. instance OAI.Tachikawa.BalancedTensor.(instance at line 596) line 596
59. instance OAI.Tachikawa.BalancedTensor.(instance at line 602) line 602
60. def OAI.Tachikawa.OuterTensor.Obj line 621
61. instance OAI.Tachikawa.OuterTensor.(instance at line 623) line 623
62. instance OAI.Tachikawa.OuterTensor.(instance at line 625) line 625
63. def OAI.Tachikawa.OuterTensor.action line 628
64. instance OAI.Tachikawa.OuterTensor.(instance at line 638) line 638
65. instance OAI.Tachikawa.OuterTensor.(instance at line 641) line 641
66. lemma OAI.Tachikawa.OuterTensor.tmul_smul_tmul line 648
67. lemma OAI.Tachikawa.OuterTensor.map_action line 653
68. def OAI.Tachikawa.OuterTensor.map line 668
69. lemma OAI.Tachikawa.OuterTensor.map_tmul line 674
70. lemma OAI.Tachikawa.OuterTensor.map_comp line 678
71. lemma OAI.Tachikawa.OuterTensor.map_id line 686
72. def OAI.Tachikawa.OuterTensor.bifunctor line 693
73. def OAI.Tachikawa.SymmetrizingForm.tensorTrace line 730
74. lemma OAI.Tachikawa.SymmetrizingForm.tensorTrace_tmul line 733
75. lemma OAI.Tachikawa.SymmetrizingForm.tensorTrace_comm line 736
76. def OAI.Tachikawa.SymmetrizingForm.tensorDualEquiv line 748
77. lemma OAI.Tachikawa.SymmetrizingForm.tensorDualEquiv_apply line 752
78. def OAI.Tachikawa.SymmetrizingForm.tensor line 765
79. abbrev OAI.Tachikawa.Enveloping.Alg line 786
80. def OAI.Tachikawa.Enveloping.Obj line 790
81. instance OAI.Tachikawa.Enveloping.(instance at line 791) line 791
82. instance OAI.Tachikawa.Enveloping.(instance at line 793) line 793
83. instance OAI.Tachikawa.Enveloping.(instance at line 795) line 795
84. instance OAI.Tachikawa.Enveloping.(instance at line 797) line 797
85. instance OAI.Tachikawa.Enveloping.(instance at line 799) line 799
86. instance OAI.Tachikawa.Enveloping.(instance at line 801) line 801
87. instance OAI.Tachikawa.Enveloping.(instance at line 803) line 803
88. instance OAI.Tachikawa.Enveloping.(instance at line 808) line 808
89. instance OAI.Tachikawa.Enveloping.(instance at line 813) line 813
90. def OAI.Tachikawa.Enveloping.leftMap line 820
91. def OAI.Tachikawa.Enveloping.rightMap line 825
92. lemma OAI.Tachikawa.Enveloping.leftMap_apply line 830
93. lemma OAI.Tachikawa.Enveloping.rightMap_apply line 832
94. lemma OAI.Tachikawa.Enveloping.tmul_smul line 835
95. def OAI.Tachikawa.SymmetrizingForm.op line 845
96. instance OAI.Tachikawa.Enveloping.objFinite line 867
97. def OAI.Tachikawa.Enveloping.leftFunctor line 870
98. def OAI.Tachikawa.Enveloping.rightFunctor line 874
99. instance OAI.Tachikawa.Enveloping.(instance at line 878) line 878
100. instance OAI.Tachikawa.Enveloping.(instance at line 880) line 880
101. def OAI.Tachikawa.Enveloping.freeLeftEquiv line 883
102. def OAI.Tachikawa.Enveloping.freeRightEquiv line 898
103. lemma OAI.Tachikawa.Enveloping.freeLeftProjective line 918
104. lemma OAI.Tachikawa.Enveloping.freeRightProjective line 922
105. lemma OAI.Tachikawa.Enveloping.projective_left line 926
106. lemma OAI.Tachikawa.Enveloping.projective_right line 937