OAI/RingTheory/Tachikawa/CompleteTensor.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Tachikawa.FiniteModule line 12
  2. instance OAI.Tachikawa.FiniteModule.(instance at line 17) line 17
  3. instance OAI.Tachikawa.FiniteModule.(instance at line 18) line 18
  4. instance OAI.Tachikawa.FiniteModule.(instance at line 19) line 19
  5. instance OAI.Tachikawa.FiniteModule.(instance at line 20) line 20
  6. instance OAI.Tachikawa.FiniteModule.(instance at line 21) line 21
  7. instance OAI.Tachikawa.FiniteModule.(instance at line 22) line 22
  8. instance OAI.Tachikawa.FiniteModule.(instance at line 23) line 23
  9. def OAI.Tachikawa.FiniteModule.cover line 27
  10. def OAI.Tachikawa.FiniteModule.syzygy line 29
  11. def OAI.Tachikawa.FiniteModule.embed line 37
  12. lemma OAI.Tachikawa.FiniteModule.embed_injective line 38
  13. def OAI.Tachikawa.FiniteModule.cosyzygy line 40
  14. def OAI.Tachikawa.FiniteModule.positive line 44
  15. def OAI.Tachikawa.FiniteModule.negative line 48
  16. abbrev OAI.Tachikawa.FiniteModule.posTerm line 52
  17. abbrev OAI.Tachikawa.FiniteModule.negTerm line 53
  18. def OAI.Tachikawa.FiniteModule.posDifferential line 55
  19. def OAI.Tachikawa.FiniteModule.negDifferential line 58
  20. def OAI.Tachikawa.FiniteModule.middle line 61
  21. lemma OAI.Tachikawa.FiniteModule.pos_exact line 63
  22. lemma OAI.Tachikawa.FiniteModule.neg_exact line 74
  23. lemma OAI.Tachikawa.FiniteModule.middle_exact_left line 89
  24. lemma OAI.Tachikawa.FiniteModule.middle_exact_right line 100
  25. def OAI.Tachikawa.FiniteModule.term line 113
  26. def OAI.Tachikawa.FiniteModule.differential line 117
  27. lemma OAI.Tachikawa.FiniteModule.differential_exact line 126
  28. def OAI.Tachikawa.FiniteModule.complete line 139
  29. lemma OAI.Tachikawa.FiniteModule.complete_exact line 143
  30. lemma OAI.Tachikawa.FiniteModule.complete_projective line 155
  31. lemma OAI.Tachikawa.FiniteModule.complete_finite line 158
  32. lemma OAI.Tachikawa.FiniteModule.complete_d line 161
  33. def OAI.Tachikawa.FiniteModule.augmentation line 164
  34. lemma OAI.Tachikawa.FiniteModule.augmentation_surjective line 171
  35. lemma OAI.Tachikawa.FiniteModule.augmentation_injective line 176
  36. def OAI.Tachikawa.FiniteModule.cokerEquiv line 188
  37. lemma OAI.Tachikawa.FiniteModule.complete_totallyAcyclic line 192
  38. lemma OAI.Tachikawa.FiniteModule.pos_augmentation_exact line 215
  39. def OAI.Tachikawa.FiniteModule.projectiveResolution line 224
  40. instance OAI.Tachikawa.FiniteModule.(instance at line 229) line 229
  41. instance OAI.Tachikawa.FiniteModule.(instance at line 233) line 233
  42. abbrev OAI.Tachikawa.Enveloping.tensorFunctor line 246
  43. abbrev OAI.Tachikawa.Enveloping.tensorComplex line 249
  44. lemma OAI.Tachikawa.Enveloping.tensorComplex_exact line 252
  45. lemma OAI.Tachikawa.Enveloping.tensorComplex_finite line 259
  46. lemma OAI.Tachikawa.Enveloping.tensorComplex_projective line 268
  47. lemma OAI.Tachikawa.Enveloping.tensor_augmentation_exact line 280
  48. lemma OAI.Tachikawa.Enveloping.tensor_map_surjective line 290
  49. def OAI.Tachikawa.Enveloping.tensorAugmentationEquiv line 294
  50. def OAI.Tachikawa.Enveloping.action line 315
  51. def OAI.Tachikawa.Enveloping.ofBimodule line 321
  52. def OAI.Tachikawa.BalancedTensor.rightAction line 337
  53. instance OAI.Tachikawa.BalancedTensor.rightModule line 350
  54. lemma OAI.Tachikawa.BalancedTensor.right_smul_mk line 353
  55. instance OAI.Tachikawa.BalancedTensor.rightTower line 356
  56. instance OAI.Tachikawa.BalancedTensor.rightComm line 365
  57. lemma OAI.Tachikawa.Enveloping.ofBimodule_tmul_smul line 385
  58. def OAI.Tachikawa.Enveloping.ofBimoduleHom line 389
  59. def OAI.Tachikawa.Enveloping.reassembleIso line 408
  60. abbrev OAI.Tachikawa.Enveloping.evalType line 434
  61. def OAI.Tachikawa.Enveloping.evalObj line 437
  62. def OAI.Tachikawa.Enveloping.evalMap line 439
  63. lemma OAI.Tachikawa.Enveloping.evalMap_mk line 443
  64. def OAI.Tachikawa.Enveloping.evaluation line 446
  65. instance OAI.Tachikawa.Enveloping.(instance at line 460) line 460
  66. def OAI.Tachikawa.Enveloping.tensorNatTrans line 480
  67. lemma OAI.Tachikawa.Enveloping.exists_tensorCompleteLift line 495
  68. def OAI.Tachikawa.Enveloping.tensorCompleteLift line 516
  69. lemma OAI.Tachikawa.Enveloping.tensorCompleteLift_aug line 518
  70. def OAI.Tachikawa.GoodComponent line 532
  71. lemma OAI.Tachikawa.goodComponent_up line 535
  72. lemma OAI.Tachikawa.goodComponent_down line 575
  73. def OAI.Tachikawa.CompleteNull.State line 607
  74. def OAI.Tachikawa.CompleteNull.stateMap line 609
  75. lemma OAI.Tachikawa.CompleteNull.stateMap_self line 613
  76. def OAI.Tachikawa.CompleteNull.Step line 615
  77. def OAI.Tachikawa.CompleteNull.up line 622
  78. lemma OAI.Tachikawa.CompleteNull.up_step line 626
  79. def OAI.Tachikawa.CompleteNull.down line 629
  80. lemma OAI.Tachikawa.CompleteNull.down_step line 634
  81. def OAI.Tachikawa.CompleteNull.component line 641
  82. lemma OAI.Tachikawa.CompleteNull.component_up line 645
  83. lemma OAI.Tachikawa.CompleteNull.component_down line 650
  84. lemma OAI.Tachikawa.CompleteNull.hasStep_down line 655
  85. lemma OAI.Tachikawa.CompleteNull.hasStep line 663
  86. def OAI.Tachikawa.CompleteNull.homotopy line 672
  87. lemma OAI.Tachikawa.exists_good_component_zero line 688
  88. theorem OAI.Tachikawa.nullhomotopic_of_coker_factors line 727
  89. lemma OAI.Tachikawa.coker_factors_of_nullhomotopic line 734
  90. theorem OAI.Tachikawa.nullhomotopic_iff_coker_factors line 752
  91. lemma OAI.Tachikawa.complete_homotopy_of_augmentation line 773