OAI/Algebra/Drinfeld/Categories.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DeligneDrinfeld.CategoricalValues.swapObjects line 12
  2. def OAI.DeligneDrinfeld.CategoricalValues.rotateObjects line 13
  3. def OAI.DeligneDrinfeld.CategoricalValues.swapLie line 14
  4. def OAI.DeligneDrinfeld.CategoricalValues.rotateLie line 15
  5. structure OAI.DeligneDrinfeld.CategoricalValues.Witness line 17
  6. def OAI.DeligneDrinfeld.CategoricalValues.value line 30
  7. theorem OAI.DeligneDrinfeld.CategoricalValues.value_anti line 32
  8. theorem OAI.DeligneDrinfeld.CategoricalValues.rotate_squared line 39
  9. theorem OAI.DeligneDrinfeld.CategoricalValues.value_cyclic line 47
  10. theorem OAI.DeligneDrinfeld.CategoricalValues.value_pentagon line 62
  11. theorem OAI.DeligneDrinfeld.CategoricalValues.value_mem line 71
  12. theorem OAI.DeligneDrinfeld.CategoricalValues.source_derivation line 74
  13. def OAI.DeligneDrinfeld.CategoricalValues.zero line 84
  14. def OAI.DeligneDrinfeld.CategoricalValues.add line 97
  15. def OAI.DeligneDrinfeld.CategoricalValues.smul line 110
  16. def OAI.DeligneDrinfeld.CategoricalValues.bracket line 123
  17. theorem OAI.DeligneDrinfeld.CategoricalValues.value_bracket line 136
  18. def OAI.DeligneDrinfeld.CategoricalValues.values line 141
  19. theorem OAI.DeligneDrinfeld.GaugeCompatibility.intertwine line 155
  20. theorem OAI.DeligneDrinfeld.GaugeCompatibility.compatible line 171
  21. def OAI.DeligneDrinfeld.ThreeSolutionCategory.data line 190
  22. theorem OAI.DeligneDrinfeld.ThreeSolutionCategory.loop_zero line 193
  23. theorem OAI.DeligneDrinfeld.ThreeSolutionCategory.value line 196
  24. theorem OAI.DeligneDrinfeld.ThreeSolutionCategory.anti line 198
  25. theorem OAI.DeligneDrinfeld.ThreeSolutionCategory.rotating_anti line 201
  26. theorem OAI.DeligneDrinfeld.ThreeSolutionCategory.rotating_twice line 210
  27. theorem OAI.DeligneDrinfeld.ThreeSolutionCategory.swap line 217
  28. theorem OAI.DeligneDrinfeld.ThreeSolutionCategory.rotate line 236
  29. def OAI.DeligneDrinfeld.FourSolutionCategory.data line 268
  30. theorem OAI.DeligneDrinfeld.FourSolutionCategory.edge line 271
  31. theorem OAI.DeligneDrinfeld.FourSolutionCategory.AB line 282
  32. theorem OAI.DeligneDrinfeld.FourSolutionCategory.AD line 289
  33. theorem OAI.DeligneDrinfeld.FourSolutionCategory.DE line 297
  34. theorem OAI.DeligneDrinfeld.FourSolutionCategory.BC line 311
  35. theorem OAI.DeligneDrinfeld.FourSolutionCategory.CE line 335
  36. theorem OAI.DeligneDrinfeld.NormalizedFamily.length_zero_piece line 359
  37. theorem OAI.DeligneDrinfeld.NormalizedFamily.length_one_piece_le line 367
  38. theorem OAI.DeligneDrinfeld.NormalizedFamily.finrank_length_one_le line 386
  39. abbrev OAI.DeligneDrinfeld.NormalizedFamily.OldDomain line 392
  40. theorem OAI.DeligneDrinfeld.NormalizedFamily.finrank_odd_le line 394
  41. def OAI.DeligneDrinfeld.IntegralFamily.depthPiece line 436
  42. theorem OAI.DeligneDrinfeld.IntegralFamily.cast_depth line 441
  43. theorem OAI.DeligneDrinfeld.IntegralFamily.tree_depth_two line 444
  44. theorem OAI.DeligneDrinfeld.IntegralFamily.tree_reduced_depth_mem line 449
  45. theorem OAI.DeligneDrinfeld.IntegralFamily.bi_reduced_depth_mem line 472
  46. theorem OAI.DeligneDrinfeld.IntegralFamily.old_reduced_depth_mem line 494
  47. structure OAI.DeligneDrinfeld.IntegralFamily.Generator line 517
  48. def OAI.DeligneDrinfeld.IntegralFamily.partialFamily line 528
  49. def OAI.DeligneDrinfeld.IntegralFamily.partialData line 541
  50. theorem OAI.DeligneDrinfeld.IntegralFamily.oldMap_mem line 562
  51. def OAI.DeligneDrinfeld.IntegralFamily.oldToDepth line 570
  52. theorem OAI.DeligneDrinfeld.IntegralFamily.old_rank_le line 578
  53. theorem OAI.DeligneDrinfeld.IntegralFamily.depth_rank_lt line 586
  54. theorem OAI.DeligneDrinfeld.IntegralFamily.dimension_sharp line 596
  55. theorem OAI.DeligneDrinfeld.IntegralFamily.generator_of_sharp line 619
  56. def OAI.DeligneDrinfeld.IntegralFamily.OddValues line 639
  57. theorem OAI.DeligneDrinfeld.IntegralFamily.generators_exist line 642
  58. def OAI.DeligneDrinfeld.IntegralFamily.generators line 656
  59. def OAI.DeligneDrinfeld.IntegralFamily.normalizedFamily line 659
  60. def OAI.DeligneDrinfeld.IntegralFamily.normalizedData line 664