OAI/MathematicalPhysics/BFSS/ColorLie.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Color Lie algebra, skew adjoints and commutators.

  1. abbrev OAI.BFSSQuantum.AlgebraData.ColorVector line 14
  2. def OAI.BFSSQuantum.AlgebraData.colorEmbed line 16
  3. lemma OAI.BFSSQuantum.AlgebraData.colorEmbed_injective line 25
  4. lemma OAI.BFSSQuantum.AlgebraData.colorEmbed_inner line 31
  5. def OAI.BFSSQuantum.AlgebraData.colorLie line 37
  6. lemma OAI.BFSSQuantum.AlgebraData.colorEmbed_lie line 40
  7. lemma OAI.BFSSQuantum.AlgebraData.bracket_add_left line 44
  8. lemma OAI.BFSSQuantum.AlgebraData.bracket_add_right line 48
  9. lemma OAI.BFSSQuantum.AlgebraData.bracket_neg_swap line 52
  10. lemma OAI.BFSSQuantum.AlgebraData.bracket_real_smul_right line 56
  11. lemma OAI.BFSSQuantum.AlgebraData.bracket_real_smul_left line 60
  12. lemma OAI.BFSSQuantum.AlgebraData.bracket_jacobi line 64
  13. lemma OAI.BFSSQuantum.AlgebraData.bracket_trace_skew line 71
  14. lemma OAI.BFSSQuantum.AlgebraData.colorLie_add_left line 81
  15. lemma OAI.BFSSQuantum.AlgebraData.colorLie_add_right line 85
  16. lemma OAI.BFSSQuantum.AlgebraData.colorLie_smul_left line 89
  17. lemma OAI.BFSSQuantum.AlgebraData.colorLie_smul_right line 93
  18. lemma OAI.BFSSQuantum.AlgebraData.colorLie_swap line 97
  19. lemma OAI.BFSSQuantum.AlgebraData.colorLie_jacobi line 101
  20. lemma OAI.BFSSQuantum.AlgebraData.colorLie_skew line 106
  21. def OAI.BFSSQuantum.AlgebraData.colorAd line 113
  22. lemma OAI.BFSSQuantum.AlgebraData.colorAd_skew line 118
  23. lemma OAI.BFSSQuantum.AlgebraData.colorAd_commutator line 121