OAI/Algebra/MarkedTensor/ReferenceWords.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Finite rational reference words whose adjoint actions span all endomorphisms.

  1. def OAI.BoundaryOnly.Holonomy.referenceGenerator line 17
  2. def OAI.BoundaryOnly.Holonomy.referenceRho line 22
  3. def OAI.BoundaryOnly.Holonomy.shortWords line 25
  4. def OAI.BoundaryOnly.Holonomy.spanningWord line 27
  5. lemma OAI.BoundaryOnly.Holonomy.spanningWord_mem line 32
  6. def OAI.BoundaryOnly.Holonomy.spanningMatrix line 37
  7. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_at_0 line 48
  8. lemma OAI.BoundaryOnly.Holonomy.spanningWord_at_0 line 49
  9. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_at_1 line 50
  10. lemma OAI.BoundaryOnly.Holonomy.spanningWord_at_1 line 51
  11. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_at_2 line 52
  12. lemma OAI.BoundaryOnly.Holonomy.spanningWord_at_2 line 53
  13. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_at_3 line 54
  14. lemma OAI.BoundaryOnly.Holonomy.spanningWord_at_3 line 55
  15. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_at_4 line 56
  16. lemma OAI.BoundaryOnly.Holonomy.spanningWord_at_4 line 57
  17. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_at_5 line 58
  18. lemma OAI.BoundaryOnly.Holonomy.spanningWord_at_5 line 59
  19. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_at_6 line 60
  20. lemma OAI.BoundaryOnly.Holonomy.spanningWord_at_6 line 61
  21. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_at_7 line 62
  22. lemma OAI.BoundaryOnly.Holonomy.spanningWord_at_7 line 63
  23. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_at_8 line 64
  24. lemma OAI.BoundaryOnly.Holonomy.spanningWord_at_8 line 65
  25. lemma OAI.BoundaryOnly.Holonomy.referenceRho_of line 67
  26. lemma OAI.BoundaryOnly.Holonomy.reference_mat_0 line 69
  27. lemma OAI.BoundaryOnly.Holonomy.reference_mat_1 line 70
  28. lemma OAI.BoundaryOnly.Holonomy.reference_mat_2 line 71
  29. lemma OAI.BoundaryOnly.Holonomy.reference_mat_inv line 72
  30. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_0 line 74
  31. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_1 line 83
  32. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_2 line 93
  33. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_3 line 104
  34. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_4 line 114
  35. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_5 line 124
  36. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_6 line 135
  37. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_7 line 146
  38. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_8 line 157
  39. lemma OAI.BoundaryOnly.Holonomy.spanningMatrix_eq line 168
  40. lemma OAI.BoundaryOnly.Holonomy.matrixUnit_00 line 181
  41. lemma OAI.BoundaryOnly.Holonomy.matrixUnit_01 line 188
  42. lemma OAI.BoundaryOnly.Holonomy.matrixUnit_02 line 196
  43. lemma OAI.BoundaryOnly.Holonomy.matrixUnit_10 line 203
  44. lemma OAI.BoundaryOnly.Holonomy.matrixUnit_11 line 211
  45. lemma OAI.BoundaryOnly.Holonomy.matrixUnit_12 line 218
  46. lemma OAI.BoundaryOnly.Holonomy.matrixUnit_20 line 226
  47. lemma OAI.BoundaryOnly.Holonomy.matrixUnit_21 line 233
  48. lemma OAI.BoundaryOnly.Holonomy.matrixUnit_22 line 241
  49. lemma OAI.BoundaryOnly.Holonomy.shortWords_finite line 250
  50. lemma OAI.BoundaryOnly.Holonomy.one_mem_shortWords line 263
  51. lemma OAI.BoundaryOnly.Holonomy.inv_mem_shortWords line 266
  52. def OAI.BoundaryOnly.Holonomy.reverseWord line 271
  53. lemma OAI.BoundaryOnly.Holonomy.reverse_mem_shortWords line 274
  54. lemma OAI.BoundaryOnly.Holonomy.reference_matrix_span line 281
  55. theorem OAI.BoundaryOnly.Holonomy.finite_reference_adjoint_span line 324