OAI/RingTheory/Tachikawa/Twisting.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Tachikawa.AlgebraInduction.Bimod line 12
  2. instance OAI.Tachikawa.AlgebraInduction.(instance at line 13) line 13
  3. instance OAI.Tachikawa.AlgebraInduction.(instance at line 14) line 14
  4. instance OAI.Tachikawa.AlgebraInduction.(instance at line 15) line 15
  5. instance OAI.Tachikawa.AlgebraInduction.(instance at line 16) line 16
  6. instance OAI.Tachikawa.AlgebraInduction.(instance at line 17) line 17
  7. instance OAI.Tachikawa.AlgebraInduction.(instance at line 19) line 19
  8. instance OAI.Tachikawa.AlgebraInduction.(instance at line 21) line 21
  9. instance OAI.Tachikawa.AlgebraInduction.(instance at line 25) line 25
  10. instance OAI.Tachikawa.AlgebraInduction.(instance at line 27) line 27
  11. abbrev OAI.Tachikawa.AlgebraInduction.functor line 31
  12. abbrev OAI.Tachikawa.AlgebraInduction.res line 33
  13. lemma OAI.Tachikawa.AlgebraInduction.mk_one_smul line 35
  14. def OAI.Tachikawa.AlgebraInduction.unit line 43
  15. def OAI.Tachikawa.AlgebraInduction.extend line 55
  16. lemma OAI.Tachikawa.AlgebraInduction.extend_mk line 78
  17. lemma OAI.Tachikawa.AlgebraInduction.unit_extend line 81
  18. lemma OAI.Tachikawa.AlgebraInduction.extend_unit line 87
  19. def OAI.Tachikawa.AlgebraInduction.homEquiv line 98
  20. lemma OAI.Tachikawa.AlgebraInduction.unit_naturality line 105
  21. instance OAI.Tachikawa.AlgebraInduction.(instance at line 110) line 110
  22. def OAI.Tachikawa.AlgebraInduction.underlyingEquiv line 113
  23. instance OAI.Tachikawa.AlgebraInduction.(instance at line 124) line 124
  24. def OAI.Tachikawa.Enveloping.regular line 136
  25. def OAI.Tachikawa.Enveloping.regularUnderlyingEquiv line 138
  26. def OAI.Tachikawa.Enveloping.regularLeftEquiv line 149
  27. def OAI.Tachikawa.Enveloping.regularRightEquiv line 159
  28. instance OAI.Tachikawa.Enveloping.(instance at line 169) line 169
  29. def OAI.Tachikawa.Enveloping.regularFinite line 174
  30. def OAI.Tachikawa.Enveloping.regularResolution line 177
  31. instance OAI.Tachikawa.Enveloping.(instance at line 180) line 180
  32. instance OAI.Tachikawa.Enveloping.(instance at line 185) line 185
  33. instance OAI.Tachikawa.Enveloping.(instance at line 189) line 189
  34. def OAI.Tachikawa.Enveloping.twistedRegular line 202
  35. def OAI.Tachikawa.Enveloping.twistedUnderlying line 205
  36. def OAI.Tachikawa.Enveloping.twistedLeftEquiv line 217
  37. def OAI.Tachikawa.Enveloping.twistedRightEquiv line 227
  38. instance OAI.Tachikawa.Enveloping.(instance at line 237) line 237
  39. instance OAI.Tachikawa.Enveloping.(instance at line 240) line 240
  40. instance OAI.Tachikawa.Enveloping.(instance at line 242) line 242
  41. lemma OAI.Tachikawa.Enveloping.twisted_left_smul line 247
  42. lemma OAI.Tachikawa.Enveloping.twisted_right_smul line 251
  43. def OAI.Tachikawa.Enveloping.twistedEvalBilinear line 266
  44. def OAI.Tachikawa.Enveloping.twistedEval line 280
  45. lemma OAI.Tachikawa.Enveloping.twistedTensor_move line 288
  46. def OAI.Tachikawa.Enveloping.twistedEvalInv line 307
  47. def OAI.Tachikawa.Enveloping.twistedEvalIso line 323
  48. abbrev OAI.Tachikawa.SymmetrizingForm.twistFunctor line 351
  49. def OAI.Tachikawa.SymmetrizingForm.freeTwistIso line 353
  50. def OAI.Tachikawa.SymmetrizingForm.twistToFree line 391
  51. def OAI.Tachikawa.SymmetrizingForm.twistFromFree line 395
  52. lemma OAI.Tachikawa.SymmetrizingForm.twistFromFree_single line 400
  53. lemma OAI.Tachikawa.SymmetrizingForm.freeHomDual_twist line 409
  54. abbrev OAI.Tachikawa.Enveloping.twistedTensorFunctor line 428
  55. lemma OAI.Tachikawa.Enveloping.twistedTensor_move_general line 431
  56. def OAI.Tachikawa.Enveloping.twistedTensorMap line 445
  57. def OAI.Tachikawa.Enveloping.twistedTensorInv line 471
  58. def OAI.Tachikawa.Enveloping.twistedTensorIso line 488
  59. def OAI.Tachikawa.Enveloping.twistedTensorNatIso line 507