OAI/RingTheory/Tachikawa/Triangular.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Tachikawa.Triangular.Off line 12
2. instance OAI.Tachikawa.Triangular.(instance at line 13) line 13
3. instance OAI.Tachikawa.Triangular.(instance at line 15) line 15
4. instance OAI.Tachikawa.Triangular.(instance at line 17) line 17
5. instance OAI.Tachikawa.Triangular.(instance at line 19) line 19
6. instance OAI.Tachikawa.Triangular.(instance at line 21) line 21
7. instance OAI.Tachikawa.Triangular.(instance at line 23) line 23
8. instance OAI.Tachikawa.Triangular.(instance at line 25) line 25
9. instance OAI.Tachikawa.Triangular.(instance at line 27) line 27
10. instance OAI.Tachikawa.Triangular.(instance at line 29) line 29
11. abbrev OAI.Tachikawa.Triangular.Alg line 32
12. instance OAI.Tachikawa.Triangular.(instance at line 33) line 33
13. def OAI.Tachikawa.Triangular.upper line 39
14. def OAI.Tachikawa.Triangular.lower line 40
15. def OAI.Tachikawa.Triangular.off line 42
16. lemma OAI.Tachikawa.Triangular.upper_apply line 47
17. lemma OAI.Tachikawa.Triangular.lower_apply line 48
18. lemma OAI.Tachikawa.Triangular.off_apply line 49
19. lemma OAI.Tachikawa.Triangular.off_mul line 50
20. def OAI.Tachikawa.Triangular.e₀ line 53
21. def OAI.Tachikawa.Triangular.e₁ line 54
22. lemma OAI.Tachikawa.Triangular.idempotent_e₀ line 55
23. lemma OAI.Tachikawa.Triangular.idempotent_e₁ line 59
24. lemma OAI.Tachikawa.Triangular.e₀_add_e₁ line 63
25. lemma OAI.Tachikawa.BalancedTensor.mk_zero_left line 77
26. lemma OAI.Tachikawa.BalancedTensor.mk_add_left line 81
27. lemma OAI.Tachikawa.BalancedTensor.mk_smul_left line 85
28. def OAI.Tachikawa.Triangular.Triple line 101
29. instance OAI.Tachikawa.Triangular.(instance at line 103) line 103
30. instance OAI.Tachikawa.Triangular.(instance at line 104) line 104
31. instance OAI.Tachikawa.Triangular.(instance at line 105) line 105
32. instance OAI.Tachikawa.Triangular.(instance at line 154) line 154
33. def OAI.Tachikawa.Triangular.tripleObj line 162
34. lemma OAI.Tachikawa.Triangular.triple_smul_fst line 164
35. lemma OAI.Tachikawa.Triangular.triple_smul_snd line 166
36. instance OAI.Tachikawa.Triangular.(instance at line 169) line 169
37. lemma OAI.Tachikawa.Triangular.e₀_smul_triple line 183
38. lemma OAI.Tachikawa.Triangular.e₁_smul_triple line 189
39. lemma OAI.Tachikawa.Triangular.diagonal_smul_triple line 195
40. def OAI.Tachikawa.Triangular.tripleMap line 202
41. lemma OAI.Tachikawa.Triangular.hom_fst_e₁ line 218
42. lemma OAI.Tachikawa.Triangular.hom_snd_e₀ line 222
43. def OAI.Tachikawa.Triangular.homUpper line 227
44. def OAI.Tachikawa.Triangular.homLower line 240
45. lemma OAI.Tachikawa.Triangular.hom_pair line 253
46. lemma OAI.Tachikawa.Triangular.hom_compatible line 264
47. lemma OAI.Tachikawa.Triangular.tripleMap_hom line 276
48. lemma OAI.Tachikawa.Triangular.triple_hom_ext line 281
49. abbrev OAI.Tachikawa.Triangular.tensorObj line 298
50. abbrev OAI.Tachikawa.Triangular.tensorMap line 299
51. abbrev OAI.Tachikawa.Triangular.zeroObj line 301
52. def OAI.Tachikawa.Triangular.D₀Obj line 303
53. def OAI.Tachikawa.Triangular.D₁Obj line 305
54. def OAI.Tachikawa.Triangular.D₀Map line 308
55. def OAI.Tachikawa.Triangular.D₁Map line 310
56. def OAI.Tachikawa.Triangular.D₀ line 313
57. def OAI.Tachikawa.Triangular.D₁ line 332
58. instance OAI.Tachikawa.Triangular.(instance at line 350) line 350
59. instance OAI.Tachikawa.Triangular.(instance at line 358) line 358
60. def OAI.Tachikawa.Triangular.diagonal₀ line 369
61. def OAI.Tachikawa.Triangular.diagonal₁ line 390
62. lemma OAI.Tachikawa.Triangular.cross₀₁_zero line 410
63. def OAI.Tachikawa.Triangular.cross₁₀ line 420
64. lemma OAI.Tachikawa.Triangular.D₀Map_exact line 452
65. lemma OAI.Tachikawa.Triangular.D₁Map_exact line 469
66. lemma OAI.Tachikawa.Triangular.D₀_exact line 482
67. lemma OAI.Tachikawa.Triangular.D₁_exact line 488
68. instance OAI.Tachikawa.Triangular.(instance at line 493) line 493
69. instance OAI.Tachikawa.Triangular.(instance at line 496) line 496
70. instance OAI.Tachikawa.Triangular.(instance at line 501) line 501
71. instance OAI.Tachikawa.Triangular.(instance at line 505) line 505
72. def OAI.Tachikawa.Triangular.freeObj line 519
73. def OAI.Tachikawa.Triangular.freeUnderlying line 520
74. def OAI.Tachikawa.Triangular.freeTensorEval line 522
75. def OAI.Tachikawa.Triangular.freeTensorInv line 526
76. lemma OAI.Tachikawa.Triangular.freeTensorEval_mk line 531
77. lemma OAI.Tachikawa.Triangular.freeTensorEval_inv line 534
78. lemma OAI.Tachikawa.Triangular.freeTensorInv_eval line 544
79. def OAI.Tachikawa.Triangular.freeTensorEquiv line 550
80. def OAI.Tachikawa.Triangular.D₀FreeInclusion line 559
81. def OAI.Tachikawa.Triangular.D₀FreeProjection line 584
82. lemma OAI.Tachikawa.Triangular.D₀Free_retract line 606
83. def OAI.Tachikawa.Triangular.D₁FreeInclusion line 613
84. def OAI.Tachikawa.Triangular.D₁FreeProjection line 634
85. lemma OAI.Tachikawa.Triangular.D₁Free_retract line 651
86. lemma OAI.Tachikawa.Triangular.D₀Free_projective line 658
87. lemma OAI.Tachikawa.Triangular.D₁Free_projective line 660
88. lemma OAI.Tachikawa.Triangular.D₀_projective line 673
89. lemma OAI.Tachikawa.Triangular.D₁_projective line 687
90. instance OAI.Tachikawa.Triangular.(instance at line 701) line 701
91. instance OAI.Tachikawa.Triangular.(instance at line 709) line 709
92. abbrev OAI.Tachikawa.Triangular.D₀Complex line 721
93. abbrev OAI.Tachikawa.Triangular.D₁Complex line 723
94. lemma OAI.Tachikawa.Triangular.diagonal₀_pre line 726
95. lemma OAI.Tachikawa.Triangular.diagonal₁_pre line 735
96. lemma OAI.Tachikawa.Triangular.cross₁₀_pre line 738
97. lemma OAI.Tachikawa.Triangular.cross₁₀_post line 741
98. lemma OAI.Tachikawa.Triangular.D₀_boundaries line 748
99. lemma OAI.Tachikawa.Triangular.D₁_boundaries line 759
100. lemma OAI.Tachikawa.Triangular.cross_boundaries line 770
101. def OAI.Tachikawa.Triangular.crossMap line 783