OAI/Algebra/Drinfeld/Descent.lean

GitHub source file

132 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DeligneDrinfeld.RationalDescent.factor_of_kernel line 14
  2. theorem OAI.DeligneDrinfeld.RationalDescent.nonvanishing line 27
  3. abbrev OAI.DeligneDrinfeld.RationalScalar.T line 49
  4. def OAI.DeligneDrinfeld.RationalScalar.one line 50
  5. def OAI.DeligneDrinfeld.RationalScalar.base line 56
  6. theorem OAI.DeligneDrinfeld.RationalScalar.base_tmul line 72
  7. def OAI.DeligneDrinfeld.RationalScalar.free line 74
  8. theorem OAI.DeligneDrinfeld.RationalScalar.free_of line 76
  9. theorem OAI.DeligneDrinfeld.RationalScalar.free_tree line 77
  10. theorem OAI.DeligneDrinfeld.RationalScalar.cast_tree line 81
  11. theorem OAI.DeligneDrinfeld.RationalScalar.tree_coefficient line 86
  12. def OAI.DeligneDrinfeld.RationalScalar.coefficient line 91
  13. def OAI.DeligneDrinfeld.RationalScalar.realCoefficient line 93
  14. theorem OAI.DeligneDrinfeld.RationalScalar.realCoefficient_tmul line 96
  15. theorem OAI.DeligneDrinfeld.RationalScalar.coefficient_free line 98
  16. theorem OAI.DeligneDrinfeld.RationalScalar.realCoefficient_tensor line 110
  17. def OAI.DeligneDrinfeld.RationalScalar.realT4 line 122
  18. theorem OAI.DeligneDrinfeld.RationalScalar.realT4_t line 127
  19. theorem OAI.DeligneDrinfeld.RationalScalar.eval_natural line 129
  20. def OAI.DeligneDrinfeld.RationalScalar.antiMap line 138
  21. def OAI.DeligneDrinfeld.RationalScalar.cyclicMap line 139
  22. def OAI.DeligneDrinfeld.RationalScalar.pentagonMap line 140
  23. theorem OAI.DeligneDrinfeld.RationalScalar.tensor_add line 143
  24. theorem OAI.DeligneDrinfeld.RationalScalar.tensor_sub line 149
  25. theorem OAI.DeligneDrinfeld.RationalScalar.tensor_id line 155
  26. theorem OAI.DeligneDrinfeld.RationalScalar.eval_tensor line 156
  27. theorem OAI.DeligneDrinfeld.RationalScalar.free_x line 158
  28. theorem OAI.DeligneDrinfeld.RationalScalar.free_y line 159
  29. theorem OAI.DeligneDrinfeld.RationalScalar.equations line 160
  30. theorem OAI.DeligneDrinfeld.RationalScalar.homogeneous_tensor line 179
  31. theorem OAI.DeligneDrinfeld.RationalScalar.tensor_prod line 201
  32. def OAI.DeligneDrinfeld.RationalScalar.system line 212
  33. theorem OAI.DeligneDrinfeld.RationalScalar.descend line 214
  34. def OAI.DeligneDrinfeld.BraidSix.total line 236
  35. def OAI.DeligneDrinfeld.BraidSix.matrix line 238
  36. structure OAI.DeligneDrinfeld.BraidSix.Relations line 241
  37. theorem OAI.DeligneDrinfeld.BraidSix.bf line 252
  38. theorem OAI.DeligneDrinfeld.BraidSix.dK line 259
  39. theorem OAI.DeligneDrinfeld.BraidSix.eL line 264
  40. theorem OAI.DeligneDrinfeld.BraidSix.aM line 269
  41. theorem OAI.DeligneDrinfeld.BraidSix.eM line 275
  42. theorem OAI.DeligneDrinfeld.BraidSix.fM line 283
  43. theorem OAI.DeligneDrinfeld.BraidSix.dP line 288
  44. theorem OAI.DeligneDrinfeld.BraidSix.cP line 294
  45. theorem OAI.DeligneDrinfeld.BraidSix.fP line 302
  46. theorem OAI.DeligneDrinfeld.BraidSix.matrix_self line 307
  47. theorem OAI.DeligneDrinfeld.BraidSix.matrix_symm line 310
  48. theorem OAI.DeligneDrinfeld.BraidSix.matrix_disjoint_0 line 313
  49. theorem OAI.DeligneDrinfeld.BraidSix.matrix_disjoint_1 line 325
  50. theorem OAI.DeligneDrinfeld.BraidSix.matrix_disjoint_2 line 337
  51. theorem OAI.DeligneDrinfeld.BraidSix.matrix_disjoint_3 line 349
  52. theorem OAI.DeligneDrinfeld.BraidSix.matrix_disjoint line 361
  53. theorem OAI.DeligneDrinfeld.BraidSix.matrix_three_0 line 370
  54. theorem OAI.DeligneDrinfeld.BraidSix.matrix_three_1 line 388
  55. theorem OAI.DeligneDrinfeld.BraidSix.matrix_three_2 line 406
  56. theorem OAI.DeligneDrinfeld.BraidSix.matrix_three_3 line 424
  57. theorem OAI.DeligneDrinfeld.BraidSix.matrix_three line 442
  58. def OAI.DeligneDrinfeld.T4Basic.a line 456
  59. def OAI.DeligneDrinfeld.T4Basic.b line 457
  60. def OAI.DeligneDrinfeld.T4Basic.c line 458
  61. def OAI.DeligneDrinfeld.T4Basic.d line 459
  62. def OAI.DeligneDrinfeld.T4Basic.e line 460
  63. def OAI.DeligneDrinfeld.T4Basic.f line 461
  64. theorem OAI.DeligneDrinfeld.T4Basic.induction line 463
  65. theorem OAI.DeligneDrinfeld.T4Basic.hom_ext line 478
  66. theorem OAI.DeligneDrinfeld.T4Basic.matrix_t line 489
  67. theorem OAI.DeligneDrinfeld.T4Basic.central_a line 492
  68. theorem OAI.DeligneDrinfeld.T4Basic.central_b line 502
  69. theorem OAI.DeligneDrinfeld.T4Basic.central_c line 512
  70. theorem OAI.DeligneDrinfeld.T4Basic.central_d line 522
  71. theorem OAI.DeligneDrinfeld.T4Basic.central_e line 532
  72. theorem OAI.DeligneDrinfeld.T4Basic.central_f line 542
  73. theorem OAI.DeligneDrinfeld.T4Basic.central line 552
  74. theorem OAI.DeligneDrinfeld.T4Basic.relations line 568
  75. structure OAI.DeligneDrinfeld.TangentBraid.Data line 594
  76. theorem OAI.DeligneDrinfeld.TangentBraid.crossing line 612
  77. theorem OAI.DeligneDrinfeld.TangentBraid.inner_pair line 622
  78. theorem OAI.DeligneDrinfeld.TangentBraid.commute_lie line 627
  79. def OAI.DeligneDrinfeld.TangentBraid.va line 630
  80. def OAI.DeligneDrinfeld.TangentBraid.vb line 631
  81. def OAI.DeligneDrinfeld.TangentBraid.vc line 632
  82. def OAI.DeligneDrinfeld.TangentBraid.vd line 633
  83. def OAI.DeligneDrinfeld.TangentBraid.ve line 634
  84. def OAI.DeligneDrinfeld.TangentBraid.vf line 635
  85. theorem OAI.DeligneDrinfeld.TangentBraid.vd_tangent line 637
  86. theorem OAI.DeligneDrinfeld.TangentBraid.bC line 640
  87. theorem OAI.DeligneDrinfeld.TangentBraid.ve_tangent line 646
  88. theorem OAI.DeligneDrinfeld.TangentBraid.gauge_difference line 653
  89. theorem OAI.DeligneDrinfeld.TangentBraid.crossing_de line 658
  90. theorem OAI.DeligneDrinfeld.TangentBraid.velocity_K line 663
  91. theorem OAI.DeligneDrinfeld.TangentBraid.velocity_L line 664
  92. theorem OAI.DeligneDrinfeld.TangentBraid.velocity_b line 670
  93. theorem OAI.DeligneDrinfeld.TangentBraid.velocity_c line 672
  94. theorem OAI.DeligneDrinfeld.TangentBraid.velocity_total line 677
  95. def OAI.DeligneDrinfeld.TangentBraid.ja line 682
  96. def OAI.DeligneDrinfeld.TangentBraid.jb line 683
  97. def OAI.DeligneDrinfeld.TangentBraid.jc line 684
  98. def OAI.DeligneDrinfeld.TangentBraid.jd line 685
  99. def OAI.DeligneDrinfeld.TangentBraid.je line 686
  100. def OAI.DeligneDrinfeld.TangentBraid.jf line 687
  101. theorem OAI.DeligneDrinfeld.TangentBraid.relations line 689
  102. theorem OAI.DeligneDrinfeld.TriangleSolutions.third line 739
  103. theorem OAI.DeligneDrinfeld.TriangleSolutions.shift_u line 745
  104. theorem OAI.DeligneDrinfeld.TriangleSolutions.shift_v line 752
  105. theorem OAI.DeligneDrinfeld.TriangleSolutions.cyclic line 759
  106. theorem OAI.DeligneDrinfeld.TriangleSolutions.special line 766
  107. def OAI.DeligneDrinfeld.T4SolutionData.A line 784
  108. def OAI.DeligneDrinfeld.T4SolutionData.B line 785
  109. def OAI.DeligneDrinfeld.T4SolutionData.C line 786
  110. def OAI.DeligneDrinfeld.T4SolutionData.D line 787
  111. def OAI.DeligneDrinfeld.T4SolutionData.E line 788
  112. def OAI.DeligneDrinfeld.T4SolutionData.H line 789
  113. def OAI.DeligneDrinfeld.T4SolutionData.I line 790
  114. def OAI.DeligneDrinfeld.T4SolutionData.J line 791
  115. def OAI.DeligneDrinfeld.T4SolutionData.P line 792
  116. def OAI.DeligneDrinfeld.T4SolutionData.Q line 793
  117. theorem OAI.DeligneDrinfeld.T4SolutionData.pentagon line 795
  118. theorem OAI.DeligneDrinfeld.T4SolutionData.permuted line 801
  119. theorem OAI.DeligneDrinfeld.T4SolutionData.data line 811
  120. def OAI.DeligneDrinfeld.T4Derivation.jets line 842
  121. theorem OAI.DeligneDrinfeld.T4Derivation.jets_base line 846
  122. def OAI.DeligneDrinfeld.T4Derivation.lift line 850
  123. theorem OAI.DeligneDrinfeld.T4Derivation.lift_t line 856
  124. theorem OAI.DeligneDrinfeld.T4Derivation.lift_base line 859
  125. def OAI.DeligneDrinfeld.T4Derivation.derivation line 868
  126. theorem OAI.DeligneDrinfeld.T4Derivation.derivation_t line 876
  127. theorem OAI.DeligneDrinfeld.T4Derivation.derivation_a line 881
  128. theorem OAI.DeligneDrinfeld.T4Derivation.derivation_b line 883
  129. theorem OAI.DeligneDrinfeld.T4Derivation.derivation_c line 885
  130. theorem OAI.DeligneDrinfeld.T4Derivation.derivation_d line 887
  131. theorem OAI.DeligneDrinfeld.T4Derivation.derivation_e line 889
  132. theorem OAI.DeligneDrinfeld.T4Derivation.derivation_f line 892