OAI/Algebra/Drinfeld/Ihara.lean

GitHub source file

171 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DeligneDrinfeld.WordGrading.homogeneous_lie line 15
  2. theorem OAI.DeligneDrinfeld.WordGrading.above_lie line 20
  3. theorem OAI.DeligneDrinfeld.WordGrading.piece_of_difference_high line 25
  4. theorem OAI.DeligneDrinfeld.WordGrading.leading_lie line 31
  5. theorem OAI.DeligneDrinfeld.WordGrading.leading_deriv line 43
  6. abbrev OAI.DeligneDrinfeld.IharaLeading.K line 63
  7. def OAI.DeligneDrinfeld.IharaLeading.action line 68
  8. def OAI.DeligneDrinfeld.IharaLeading.lowAction line 70
  9. theorem OAI.DeligneDrinfeld.IharaLeading.delta_above line 73
  10. theorem OAI.DeligneDrinfeld.IharaLeading.action_above line 79
  11. theorem OAI.DeligneDrinfeld.IharaLeading.lowAction_homogeneous line 92
  12. theorem OAI.DeligneDrinfeld.IharaLeading.delta_low_difference line 105
  13. theorem OAI.DeligneDrinfeld.IharaLeading.action_difference line 114
  14. theorem OAI.DeligneDrinfeld.IharaLeading.leading_action line 131
  15. theorem OAI.DeligneDrinfeld.AssociativeElimination.deriv_naturality line 144
  16. theorem OAI.DeligneDrinfeld.AssociativeElimination.deriv_inner_right line 153
  17. theorem OAI.DeligneDrinfeld.IharaLeading.erase_low line 169
  18. theorem OAI.DeligneDrinfeld.IharaLeading.erase_lowAction_inner line 174
  19. def OAI.DeligneDrinfeld.IharaLeading.ihara line 190
  20. theorem OAI.DeligneDrinfeld.IharaLeading.ihara_above line 192
  21. theorem OAI.DeligneDrinfeld.IharaLeading.leading_ihara line 200
  22. theorem OAI.DeligneDrinfeld.IharaLeading.actual_leading_ihara line 211
  23. def OAI.DeligneDrinfeld.GenericIhara.D line 233
  24. def OAI.DeligneDrinfeld.GenericIhara.ihara line 235
  25. def OAI.DeligneDrinfeld.GenericIhara.assocD line 236
  26. def OAI.DeligneDrinfeld.GenericIhara.assocIhara line 238
  27. theorem OAI.DeligneDrinfeld.GenericIhara.embed_D line 240
  28. theorem OAI.DeligneDrinfeld.GenericIhara.embed_ihara line 248
  29. theorem OAI.DeligneDrinfeld.GenericIhara.rational_D line 251
  30. theorem OAI.DeligneDrinfeld.GenericIhara.rational_ihara line 262
  31. theorem OAI.DeligneDrinfeld.IharaLeading.quad_action line 273
  32. theorem OAI.DeligneDrinfeld.IharaLeading.quad_ihara line 287
  33. def OAI.DeligneDrinfeld.IharaLeading.deltaLie line 290
  34. theorem OAI.DeligneDrinfeld.IharaLeading.embed_deltaLie line 295
  35. def OAI.DeligneDrinfeld.IharaLeading.actionLie line 303
  36. theorem OAI.DeligneDrinfeld.IharaLeading.embed_actionLie line 308
  37. def OAI.DeligneDrinfeld.IharaLeading.iharaLie line 317
  38. theorem OAI.DeligneDrinfeld.IharaLeading.embed_iharaLie line 319
  39. theorem OAI.DeligneDrinfeld.IharaLeading.actual_ihara_representation line 322
  40. def OAI.DeligneDrinfeld.GenericIhara.depth line 337
  41. theorem OAI.DeligneDrinfeld.GenericIhara.assocD_above line 339
  42. theorem OAI.DeligneDrinfeld.GenericIhara.assocIhara_above line 348
  43. theorem OAI.DeligneDrinfeld.GenericIhara.ihara_above line 355
  44. theorem OAI.DeligneDrinfeld.GenericIhara.assocD_homogeneous line 361
  45. theorem OAI.DeligneDrinfeld.GenericIhara.ihara_homogeneous line 370
  46. theorem OAI.DeligneDrinfeld.GenericIhara.D_zero line 386
  47. theorem OAI.DeligneDrinfeld.GenericIhara.D_add line 391
  48. theorem OAI.DeligneDrinfeld.GenericIhara.D_smul line 396
  49. def OAI.DeligneDrinfeld.GenericIhara.Dlinear line 401
  50. theorem OAI.DeligneDrinfeld.GenericIhara.D_of_false line 406
  51. theorem OAI.DeligneDrinfeld.GenericIhara.D_of_true line 407
  52. theorem OAI.DeligneDrinfeld.GenericIhara.D_ihara line 409
  53. abbrev OAI.DeligneDrinfeld.GenericIhara.Ambient line 420
  54. def OAI.DeligneDrinfeld.GenericIhara.graph line 423
  55. abbrev OAI.DeligneDrinfeld.GenericIhara.Algebra line 442
  56. def OAI.DeligneDrinfeld.GenericIhara.erase line 444
  57. theorem OAI.DeligneDrinfeld.GenericIhara.erase_lie line 457
  58. def OAI.DeligneDrinfeld.GenericIhara.lift line 466
  59. def OAI.DeligneDrinfeld.GenericIhara.evalIhara line 469
  60. theorem OAI.DeligneDrinfeld.GenericIhara.evalIhara_of line 471
  61. theorem OAI.DeligneDrinfeld.GenericIhara.evalIhara_lie line 474
  62. def OAI.DeligneDrinfeld.LatticeDimension.cast line 486
  63. theorem OAI.DeligneDrinfeld.LatticeDimension.cast_apply line 491
  64. def OAI.DeligneDrinfeld.LatticeDimension.lattice line 493
  65. theorem OAI.DeligneDrinfeld.LatticeDimension.mem_lattice line 496
  66. theorem OAI.DeligneDrinfeld.LatticeDimension.saturated line 499
  67. instance OAI.DeligneDrinfeld.LatticeDimension.quotient_torsionFree line 507
  68. theorem OAI.DeligneDrinfeld.LatticeDimension.exists_retraction line 522
  69. def OAI.DeligneDrinfeld.LatticeDimension.scalarMap line 543
  70. theorem OAI.DeligneDrinfeld.LatticeDimension.scalarMap_tmul line 547
  71. theorem OAI.DeligneDrinfeld.LatticeDimension.scalarMap_injective line 552
  72. def OAI.DeligneDrinfeld.LatticeDimension.reduction line 563
  73. theorem OAI.DeligneDrinfeld.LatticeDimension.rational_range line 566
  74. theorem OAI.DeligneDrinfeld.LatticeDimension.finrank_reduction line 594
  75. abbrev OAI.DeligneDrinfeld.LieDimension.Words line 612
  76. def OAI.DeligneDrinfeld.LieDimension.toWords line 614
  77. def OAI.DeligneDrinfeld.LieDimension.coordinates line 618
  78. theorem OAI.DeligneDrinfeld.LieDimension.coordinates_apply line 621
  79. theorem OAI.DeligneDrinfeld.LieDimension.coordinates_injective line 624
  80. def OAI.DeligneDrinfeld.LieDimension.image line 631
  81. theorem OAI.DeligneDrinfeld.LieDimension.words_space line 635
  82. theorem OAI.DeligneDrinfeld.LieDimension.words_space_reflect line 644
  83. def OAI.DeligneDrinfeld.LieDimension.castHom line 652
  84. theorem OAI.DeligneDrinfeld.LieDimension.coordinates_castHom line 657
  85. theorem OAI.DeligneDrinfeld.LieDimension.lattice_image line 661
  86. theorem OAI.DeligneDrinfeld.LieDimension.cast_eval line 689
  87. theorem OAI.DeligneDrinfeld.LieDimension.reduction_image line 697
  88. instance OAI.DeligneDrinfeld.LieDimension.homogeneous_finite line 747
  89. theorem OAI.DeligneDrinfeld.LieDimension.finrank_homogeneous line 750
  90. theorem OAI.DeligneDrinfeld.LieGrading.piece_add line 765
  91. theorem OAI.DeligneDrinfeld.LieGrading.piece_smul line 770
  92. def OAI.DeligneDrinfeld.LieGrading.projection line 775
  93. theorem OAI.DeligneDrinfeld.LieGrading.piece_homogeneous line 780
  94. def OAI.DeligneDrinfeld.LieGrading.biPiece line 786
  95. def OAI.DeligneDrinfeld.LieGrading.components line 789
  96. def OAI.DeligneDrinfeld.LieGrading.assemble line 797
  97. theorem OAI.DeligneDrinfeld.LieGrading.components_assemble line 803
  98. theorem OAI.DeligneDrinfeld.LieGrading.assemble_components line 815
  99. def OAI.DeligneDrinfeld.LieGrading.decomposition line 838
  100. theorem OAI.DeligneDrinfeld.LieGrading.finrank_decomposition line 847
  101. theorem OAI.DeligneDrinfeld.FiltrationDimension.step line 863
  102. theorem OAI.DeligneDrinfeld.FiltrationDimension.telescoping line 880
  103. theorem OAI.DeligneDrinfeld.FiltrationDimension.bound line 890
  104. theorem OAI.DeligneDrinfeld.FiltrationDimension.range_step line 898
  105. theorem OAI.DeligneDrinfeld.FiltrationDimension.surjective_of_equality line 914
  106. def OAI.DeligneDrinfeld.BaseChangeEquations.antisymmetryMap line 948
  107. def OAI.DeligneDrinfeld.BaseChangeEquations.specialMap line 951
  108. def OAI.DeligneDrinfeld.BaseChangeEquations.pentagonMap line 955
  109. theorem OAI.DeligneDrinfeld.BaseChangeEquations.antisymmetryMap_apply line 961
  110. theorem OAI.DeligneDrinfeld.BaseChangeEquations.specialMap_apply line 962
  111. theorem OAI.DeligneDrinfeld.BaseChangeEquations.pentagonMap_apply line 963
  112. abbrev OAI.DeligneDrinfeld.ReducedDimension.K line 970
  113. instance OAI.DeligneDrinfeld.ReducedDimension.finite_boolWords line 972
  114. instance OAI.DeligneDrinfeld.ReducedDimension.finite_oddWords line 975
  115. def OAI.DeligneDrinfeld.ReducedDimension.solutions line 985
  116. theorem OAI.DeligneDrinfeld.ReducedDimension.solutions_hom line 989
  117. theorem OAI.DeligneDrinfeld.ReducedDimension.solutions_anti line 992
  118. theorem OAI.DeligneDrinfeld.ReducedDimension.solutions_special line 994
  119. theorem OAI.DeligneDrinfeld.ReducedDimension.solutions_pentagon line 996
  120. instance OAI.DeligneDrinfeld.ReducedDimension.finite_solutions line 998
  121. def OAI.DeligneDrinfeld.ReducedDimension.representation line 1002
  122. theorem OAI.DeligneDrinfeld.ReducedDimension.representation_under line 1005
  123. def OAI.DeligneDrinfeld.ReducedDimension.representationMap line 1009
  124. theorem OAI.DeligneDrinfeld.ReducedDimension.representation_injective line 1020
  125. def OAI.DeligneDrinfeld.ReducedDimension.filtration line 1026
  126. def OAI.DeligneDrinfeld.ReducedDimension.oddPiece line 1029
  127. instance OAI.DeligneDrinfeld.ReducedDimension.finite_oddPiece line 1032
  128. def OAI.DeligneDrinfeld.ReducedDimension.inclusion line 1035
  129. theorem OAI.DeligneDrinfeld.ReducedDimension.inclusion_injective line 1038
  130. def OAI.DeligneDrinfeld.ReducedDimension.leadingMap line 1041
  131. theorem OAI.DeligneDrinfeld.ReducedDimension.leadingMap_apply line 1045
  132. theorem OAI.DeligneDrinfeld.ReducedDimension.leading_in_range line 1048
  133. def OAI.DeligneDrinfeld.ReducedDimension.gradedMap line 1054
  134. theorem OAI.DeligneDrinfeld.ReducedDimension.gradedMap_spec line 1058
  135. def OAI.DeligneDrinfeld.ReducedDimension.restore line 1064
  136. theorem OAI.DeligneDrinfeld.ReducedDimension.restore_erase line 1067
  137. theorem OAI.DeligneDrinfeld.ReducedDimension.graded_kernel line 1075
  138. theorem OAI.DeligneDrinfeld.ReducedDimension.filtration_zero line 1095
  139. theorem OAI.DeligneDrinfeld.ReducedDimension.filtration_terminal line 1102
  140. theorem OAI.DeligneDrinfeld.ReducedDimension.odd_length_bound line 1121
  141. theorem OAI.DeligneDrinfeld.ReducedDimension.finrank_bound line 1128
  142. theorem OAI.DeligneDrinfeld.ReducedDimension.rational_finrank_bound line 1138
  143. theorem OAI.DeligneDrinfeld.LieGrading.weightedWord_tree line 1151
  144. theorem OAI.DeligneDrinfeld.LieGrading.tree_weightedWord line 1160
  145. theorem OAI.DeligneDrinfeld.LieGrading.weightPiece_eq line 1165
  146. abbrev OAI.DeligneDrinfeld.RationalBound.wt line 1178
  147. abbrev OAI.DeligneDrinfeld.RationalBound.Words line 1179
  148. def OAI.DeligneDrinfeld.RationalBound.toHom line 1181
  149. def OAI.DeligneDrinfeld.RationalBound.coordinates line 1186
  150. theorem OAI.DeligneDrinfeld.RationalBound.coordinates_injective line 1189
  151. instance OAI.DeligneDrinfeld.RationalBound.finite_Wn line 1194
  152. def OAI.DeligneDrinfeld.RationalBound.image line 1197
  153. def OAI.DeligneDrinfeld.RationalBound.reducedCoordinates line 1199
  154. theorem OAI.DeligneDrinfeld.RationalBound.reducedCoordinates_injective line 1202
  155. def OAI.DeligneDrinfeld.RationalBound.reducedImage line 1207
  156. theorem OAI.DeligneDrinfeld.RationalBound.lattice_lift line 1209
  157. def OAI.DeligneDrinfeld.RationalBound.reduceLattice line 1228
  158. theorem OAI.DeligneDrinfeld.RationalBound.reduction_le line 1239
  159. theorem OAI.DeligneDrinfeld.RationalBound.finrank_Wn_le line 1259
  160. theorem OAI.DeligneDrinfeld.LowWeight.treeDegree_pos line 1278
  161. theorem OAI.DeligneDrinfeld.LowWeight.tree_degree_one line 1284
  162. theorem OAI.DeligneDrinfeld.LowWeight.weight_zero line 1294
  163. theorem OAI.DeligneDrinfeld.LowWeight.weight_one_form line 1303
  164. def OAI.DeligneDrinfeld.LowWeight.edgeValue line 1323
  165. def OAI.DeligneDrinfeld.LowWeight.detector line 1326
  166. theorem OAI.DeligneDrinfeld.LowWeight.detector_t line 1340
  167. theorem OAI.DeligneDrinfeld.LowWeight.weight_one_zero line 1343
  168. def OAI.DeligneDrinfeld.LowWeight.cyclic line 1354
  169. theorem OAI.DeligneDrinfeld.LowWeight.cyclic_weight_two line 1356
  170. theorem OAI.DeligneDrinfeld.LowWeight.weight_two_zero line 1375
  171. theorem OAI.DeligneDrinfeld.LowWeight.Wn_eq_bot line 1380