OAI/RingTheory/Tachikawa/FiniteCoinduction.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Tachikawa.dualTensorUnderlying line 14
  2. lemma OAI.Tachikawa.dualTensorUnderlying_tmul line 21
  3. def OAI.Tachikawa.dualTensorLeftEquiv line 27
  4. def OAI.Tachikawa.dualRightObj line 55
  5. def OAI.Tachikawa.dualRightUnderlying line 57
  6. def OAI.Tachikawa.dualRightTensorUnderlying line 60
  7. lemma OAI.Tachikawa.dualRightTensorUnderlying_tmul line 67
  8. lemma OAI.Tachikawa.dualRightTensor_action line 73
  9. def OAI.Tachikawa.dualRightTensorRestriction line 89
  10. def OAI.Tachikawa.dualRightTensorIso line 92
  11. instance OAI.Tachikawa.dualRightTensorRestriction_additive line 108
  12. instance OAI.Tachikawa.dualRightTensorRestriction_isEquivalence line 112
  13. lemma OAI.Tachikawa.Construction.cDualLeft_finite line 125
  14. lemma OAI.Tachikawa.Construction.cDualRight_finite line 134
  15. lemma OAI.Tachikawa.Construction.cDualLeft_above line 143
  16. lemma OAI.Tachikawa.Construction.cDualRight_above line 149
  17. def OAI.Tachikawa.Construction.bDualLeftResolution line 155
  18. def OAI.Tachikawa.Construction.bDualRightResolution line 162
  19. lemma OAI.Tachikawa.Construction.bDualLeft_above line 170
  20. lemma OAI.Tachikawa.Construction.bDualRight_above line 174
  21. lemma OAI.Tachikawa.Construction.bDualLeft_dimension line 179
  22. lemma OAI.Tachikawa.Construction.bDualRight_dimension line 188
  23. def OAI.Tachikawa.LeftDual line 206
  24. instance OAI.Tachikawa.LeftDual.(instance at line 209) line 209
  25. instance OAI.Tachikawa.LeftDual.(instance at line 210) line 210
  26. instance OAI.Tachikawa.LeftDual.(instance at line 211) line 211
  27. instance OAI.Tachikawa.LeftDual.(instance at line 212) line 212
  28. lemma OAI.Tachikawa.LeftDual.ext line 213
  29. instance OAI.Tachikawa.LeftDual.(instance at line 214) line 214
  30. lemma OAI.Tachikawa.LeftDual.smul_apply line 222
  31. instance OAI.Tachikawa.LeftDual.(instance at line 223) line 223
  32. instance OAI.Tachikawa.LeftDual.(instance at line 225) line 225
  33. instance OAI.Tachikawa.LeftDual.(instance at line 227) line 227
  34. def OAI.Tachikawa.LeftDual.map line 229
  35. lemma OAI.Tachikawa.LeftDual.map_apply line 233
  36. lemma OAI.Tachikawa.LeftDual.exact line 234
  37. lemma OAI.Tachikawa.LeftDual.map_injective line 236
  38. def OAI.Tachikawa.RightDual line 243
  39. instance OAI.Tachikawa.RightDual.(instance at line 246) line 246
  40. instance OAI.Tachikawa.RightDual.(instance at line 247) line 247
  41. instance OAI.Tachikawa.RightDual.(instance at line 248) line 248
  42. instance OAI.Tachikawa.RightDual.(instance at line 249) line 249
  43. lemma OAI.Tachikawa.RightDual.ext line 250
  44. instance OAI.Tachikawa.RightDual.(instance at line 251) line 251
  45. lemma OAI.Tachikawa.RightDual.smul_apply line 259
  46. instance OAI.Tachikawa.RightDual.(instance at line 260) line 260
  47. instance OAI.Tachikawa.RightDual.(instance at line 262) line 262
  48. def OAI.Tachikawa.RightDual.map line 265
  49. lemma OAI.Tachikawa.RightDual.map_apply line 269
  50. lemma OAI.Tachikawa.RightDual.map_surjective line 270
  51. def OAI.Tachikawa.dualTranspose line 277
  52. def OAI.Tachikawa.dualUntranspose line 293
  53. instance OAI.Tachikawa.leftDual_injective line 309
  54. def OAI.Tachikawa.leftDualObj line 337
  55. def OAI.Tachikawa.dualResolution line 339
  56. lemma OAI.Tachikawa.leftDualObj_isZero line 355
  57. lemma OAI.Tachikawa.dualResolution_above line 369
  58. lemma OAI.Tachikawa.dualResolution_ext_zero line 374
  59. def OAI.Tachikawa.doubleDualRegularEquiv line 393
  60. def OAI.Tachikawa.doubleDualRegularIso line 401
  61. lemma OAI.Tachikawa.Construction.b_regular_ext_zero line 407
  62. lemma OAI.Tachikawa.finite_injective_retract_dual line 427
  63. lemma OAI.Tachikawa.finiteInjective_inAdd line 445
  64. def OAI.Tachikawa.Construction.bRegularLeftObj line 463
  65. instance OAI.Tachikawa.Construction.(instance at line 465) line 465
  66. lemma OAI.Tachikawa.Construction.b_injectiveDimension line 468
  67. lemma OAI.Tachikawa.Construction.b_iterate_injective line 474
  68. lemma OAI.Tachikawa.Construction.b_iterate_inAdd line 479
  69. lemma OAI.Tachikawa.Construction.b_coindTerm_inAdd line 486
  70. instance OAI.Tachikawa.Enveloping.rightFree_preservesFiniteColimits line 503
  71. instance OAI.Tachikawa.Enveloping.rightFree_preservesFiniteLimits line 505
  72. def OAI.Tachikawa.Enveloping.coindCokerTensorIso line 508
  73. def OAI.Tachikawa.Enveloping.coindIterateTensorIso line 522
  74. def OAI.Tachikawa.Enveloping.coindTermTensorIso line 529
  75. def OAI.Tachikawa.Enveloping.leftRegularObj line 545
  76. def OAI.Tachikawa.Enveloping.leftRegularUnderlying line 547
  77. def OAI.Tachikawa.Enveloping.rightRegularUnderlying line 550
  78. def OAI.Tachikawa.Enveloping.regularOuterUnderlying line 553
  79. lemma OAI.Tachikawa.Enveloping.regularOuterUnderlying_tmul line 559
  80. def OAI.Tachikawa.Enveloping.regularOuterEquiv line 562
  81. def OAI.Tachikawa.Enveloping.regularOuterIso line 578
  82. lemma OAI.Tachikawa.Enveloping.finiteProjective_inAdd_outer line 582
  83. lemma OAI.Tachikawa.InAdd.trans line 599
  84. lemma OAI.Tachikawa.Construction.b_outerCoindTerm_inAdd line 627
  85. lemma OAI.Tachikawa.Construction.b_outerIterate_inAdd line 634
  86. theorem OAI.Tachikawa.Construction.b_projective_coinduced_terms line 641
  87. theorem OAI.Tachikawa.Construction.b_add_two_orthogonalities line 659
  88. def OAI.Tachikawa.shortExactReplacementMap line 678
  89. lemma OAI.Tachikawa.shortExactReplacementMap_quasiIso line 687
  90. lemma OAI.Tachikawa.InAdd.biproduct line 718
  91. lemma OAI.Tachikawa.InAdd.biprod line 737
  92. structure OAI.Tachikawa.Enveloping.CoindReplacement line 756
  93. def OAI.Tachikawa.Enveloping.coindReplacement line 763
  94. def OAI.Tachikawa.Enveloping.CoindGoodTerms line 773
  95. lemma OAI.Tachikawa.Enveloping.mappingCocone_inAdd line 778
  96. lemma OAI.Tachikawa.Enveloping.coindReplacement_terms line 787
  97. lemma OAI.Tachikawa.Enveloping.mappingCocone_isZero_X line 803
  98. lemma OAI.Tachikawa.Enveloping.coindReplacement_bounded line 811
  99. lemma OAI.Tachikawa.Construction.b_coindGoodTerms line 834
  100. theorem OAI.Tachikawa.Construction.b_bounded_ordinary_replacement line 850
  101. theorem OAI.Tachikawa.Construction.b_ordinary_factorization line 873