OAI/Algebra/Drinfeld/Coefficients.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RealDeligneDrinfeld.KZHomogeneous.V line 10
  2. def OAI.RealDeligneDrinfeld.KZHomogeneous.q line 11
  3. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.q_homogeneous line 12
  4. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.q_embed line 18
  5. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.normal_mem line 21
  6. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.normal_below line 27
  7. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.quotient_normal line 29
  8. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.value_above line 36
  9. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.q_embed_zero line 40
  10. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.piece_drop line 44
  11. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.q_embed_any line 51
  12. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.residual_above line 60
  13. structure OAI.DeligneDrinfeld.CategoryGauge.Data line 84
  14. def OAI.DeligneDrinfeld.CategoryGauge.unit line 88
  15. def OAI.DeligneDrinfeld.CategoryGauge.loop line 90
  16. theorem OAI.DeligneDrinfeld.CategoryGauge.loop_apply line 93
  17. theorem OAI.DeligneDrinfeld.CategoryGauge.unit_cocycle line 99
  18. theorem OAI.DeligneDrinfeld.CategoryGauge.loop_change line 103
  19. def OAI.DeligneDrinfeld.CategoryGauge.commutator line 108
  20. theorem OAI.DeligneDrinfeld.CategoryGauge.loop_commutator line 112
  21. theorem OAI.DeligneDrinfeld.CategoryGauge.unit_commutator line 121
  22. def OAI.DeligneDrinfeld.CategoryGauge.Compatible line 128
  23. theorem OAI.DeligneDrinfeld.CategoryGauge.compatible_commutator line 132
  24. def OAI.DeligneDrinfeld.CategoryGauge.zero line 143
  25. def OAI.DeligneDrinfeld.CategoryGauge.add line 144
  26. def OAI.DeligneDrinfeld.CategoryGauge.smul line 145
  27. theorem OAI.DeligneDrinfeld.CategoryGauge.zero_unit line 147
  28. theorem OAI.DeligneDrinfeld.CategoryGauge.zero_loop line 148
  29. theorem OAI.DeligneDrinfeld.CategoryGauge.add_unit line 149
  30. theorem OAI.DeligneDrinfeld.CategoryGauge.add_loop line 151
  31. theorem OAI.DeligneDrinfeld.CategoryGauge.smul_unit line 153
  32. theorem OAI.DeligneDrinfeld.CategoryGauge.smul_loop line 155
  33. theorem OAI.DeligneDrinfeld.CategoryGauge.compatible_zero line 158
  34. theorem OAI.DeligneDrinfeld.CategoryGauge.compatible_add line 161
  35. theorem OAI.DeligneDrinfeld.CategoryGauge.compatible_smul line 169
  36. theorem OAI.DeligneDrinfeld.CategoryGauge.commutator_zero_unit line 176
  37. theorem OAI.DeligneDrinfeld.CategoryGauge.commutator_zero_loop line 180
  38. def OAI.DeligneDrinfeld.CategoryGauge.EdgeCompatible line 191
  39. theorem OAI.DeligneDrinfeld.CategoryGauge.edge_target line 195
  40. theorem OAI.DeligneDrinfeld.CategoryGauge.edge_commutator line 200
  41. theorem OAI.DeligneDrinfeld.CategoryGauge.edge_zero line 210
  42. theorem OAI.DeligneDrinfeld.CategoryGauge.edge_add line 214
  43. theorem OAI.DeligneDrinfeld.CategoryGauge.edge_smul line 222
  44. theorem OAI.DeligneDrinfeld.CategoryGauge.commutator_kills line 229
  45. def OAI.RealDeligneDrinfeld.CategoricalValues.swapObjects line 238
  46. def OAI.RealDeligneDrinfeld.CategoricalValues.rotateObjects line 239
  47. def OAI.RealDeligneDrinfeld.CategoricalValues.swapLie line 240
  48. def OAI.RealDeligneDrinfeld.CategoricalValues.rotateLie line 241
  49. structure OAI.RealDeligneDrinfeld.CategoricalValues.Witness line 243
  50. def OAI.RealDeligneDrinfeld.CategoricalValues.value line 256
  51. theorem OAI.RealDeligneDrinfeld.CategoricalValues.value_anti line 258
  52. theorem OAI.RealDeligneDrinfeld.CategoricalValues.rotate_squared line 265
  53. theorem OAI.RealDeligneDrinfeld.CategoricalValues.value_cyclic line 273
  54. theorem OAI.RealDeligneDrinfeld.CategoricalValues.value_pentagon line 288
  55. theorem OAI.RealDeligneDrinfeld.CategoricalValues.value_mem line 297
  56. theorem OAI.RealDeligneDrinfeld.CategoricalValues.source_derivation line 300
  57. def OAI.RealDeligneDrinfeld.KZHomogeneous.assoc line 318
  58. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.assoc_atom line 319
  59. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.assoc_embed line 320
  60. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.assoc_homogeneous line 328
  61. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.piece_natural line 334
  62. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.swap_piece line 348
  63. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.rotate_piece line 356
  64. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.anti line 367
  65. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.cyclic line 374
  66. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.value_depth line 386
  67. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.normal_depth line 391
  68. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.q_depth line 396
  69. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.weight_one_form line 399
  70. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.q_one line 416
  71. def OAI.RealDeligneDrinfeld.KZHomogeneous.cyc line 434
  72. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.cyclic_weight_two line 435
  73. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.q_two line 453
  74. theorem OAI.RealDeligneDrinfeld.KZHomogeneous.q_low line 457
  75. theorem OAI.DeligneDrinfeld.TangentialCutoff.word_mem line 472
  76. theorem OAI.DeligneDrinfeld.TangentialCutoff.mem line 484
  77. theorem OAI.DeligneDrinfeld.TangentialCutoff.difference_mem line 494
  78. theorem OAI.DeligneDrinfeld.CutoffCategory.loop_natural line 529
  79. theorem OAI.DeligneDrinfeld.CutoffCategory.edge_natural line 545
  80. theorem OAI.DeligneDrinfeld.CutoffCategory.exp_edge line 555
  81. theorem OAI.DeligneDrinfeld.PresentedSubstitution.lift_word_mem line 572
  82. theorem OAI.DeligneDrinfeld.PresentedSubstitution.lift_mem line 579
  83. def OAI.DeligneDrinfeld.PresentedSubstitution.subst line 583
  84. theorem OAI.DeligneDrinfeld.PresentedSubstitution.subst_quotient line 589
  85. theorem OAI.DeligneDrinfeld.PresentedSubstitution.subst_gen line 592
  86. theorem OAI.DeligneDrinfeld.PresentedSubstitution.subst_mem line 595
  87. theorem OAI.DeligneDrinfeld.PresentedCutoff.raw_embed line 610
  88. theorem OAI.DeligneDrinfeld.PresentedCutoff.derivation_embed line 632