OAI/RingTheory/Tachikawa/DerivedDescent.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Tachikawa.projective_dimension_of_bounded_resolution line 12
  2. lemma OAI.Tachikawa.InAdd.projectiveDimension line 25
  3. lemma OAI.Tachikawa.InAdd.map line 43
  4. lemma OAI.Tachikawa.InAdd.iso line 48
  5. lemma OAI.Tachikawa.InAdd.retract line 52
  6. lemma OAI.Tachikawa.finiteProjective_inAdd line 66
  7. lemma OAI.Tachikawa.Construction.restrictedLeftResolution_finite line 84
  8. lemma OAI.Tachikawa.Construction.restrictedRightResolution_finite line 89
  9. def OAI.Tachikawa.Construction.restrictedBimoduleResolution line 114
  10. lemma OAI.Tachikawa.Construction.restrictedBimoduleResolution_above line 124
  11. lemma OAI.Tachikawa.Construction.restrictedBimodule_pd line 130
  12. lemma OAI.Tachikawa.Construction.restrictedProjective_pd line 139
  13. def OAI.Tachikawa.freeEndo line 159
  14. instance OAI.Tachikawa.(instance at line 161) line 161
  15. def OAI.Tachikawa.freeCounit line 164
  16. lemma OAI.Tachikawa.freeCounit_surjective line 167
  17. instance OAI.Tachikawa.(instance at line 175) line 175
  18. def OAI.Tachikawa.freeCounitNat line 178
  19. instance OAI.Tachikawa.(instance at line 187) line 187
  20. def OAI.Tachikawa.freeKernel line 191
  21. instance OAI.Tachikawa.(instance at line 192) line 192
  22. def OAI.Tachikawa.freeι line 202
  23. lemma OAI.Tachikawa.freeι_counit line 205
  24. def OAI.Tachikawa.freeShort line 208
  25. lemma OAI.Tachikawa.freeShort_exact line 211
  26. instance OAI.Tachikawa.freeEndo_projective line 217
  27. instance OAI.Tachikawa.freeEndo_finite line 226
  28. instance OAI.Tachikawa.freeKernel_finite line 233
  29. lemma OAI.Tachikawa.freeKernel_pd line 242
  30. abbrev OAI.Tachikawa.Enveloping.coindComplex line 258
  31. abbrev OAI.Tachikawa.Enveloping.cokerComplex line 261
  32. def OAI.Tachikawa.Enveloping.coindComplexUnit line 264
  33. def OAI.Tachikawa.Enveloping.coindComplexπ line 268
  34. def OAI.Tachikawa.Enveloping.coindComplexShort line 272
  35. lemma OAI.Tachikawa.Enveloping.coindComplexShort_exact line 279
  36. abbrev OAI.Tachikawa.freeComplex line 293
  37. abbrev OAI.Tachikawa.kernelComplex line 295
  38. def OAI.Tachikawa.freeComplexCounit line 298
  39. def OAI.Tachikawa.freeComplexι line 302
  40. def OAI.Tachikawa.freeComplexShort line 306
  41. lemma OAI.Tachikawa.freeComplexShort_exact line 313
  42. lemma OAI.Tachikawa.mappingCone_map_quasiIso line 330
  43. def OAI.Tachikawa.shortExactReplacementMapDual line 355
  44. lemma OAI.Tachikawa.shortExactReplacementMapDual_quasiIso line 359
  45. structure OAI.Tachikawa.IndReplacement line 375
  46. def OAI.Tachikawa.indReplacement line 381
  47. lemma OAI.Tachikawa.mappingCone_projective line 391
  48. lemma OAI.Tachikawa.mappingCone_finite line 398
  49. lemma OAI.Tachikawa.mappingCone_isZero_X line 406
  50. lemma OAI.Tachikawa.indReplacement_bounded line 411
  51. lemma OAI.Tachikawa.indReplacement_terms line 426
  52. theorem OAI.Tachikawa.bounded_projective_replacement line 445
  53. abbrev OAI.Tachikawa.Construction.bimoduleRestriction line 465
  54. theorem OAI.Tachikawa.Construction.restricted_perfect_replacement line 472
  55. def OAI.Tachikawa.Construction.restrictedTwistedUnderlying line 515
  56. def OAI.Tachikawa.Construction.restrictedUUnderlying line 524
  57. def OAI.Tachikawa.Construction.rhoBimoduleLinear line 527
  58. lemma OAI.Tachikawa.Construction.rhoBimoduleLinear_tensor line 532
  59. def OAI.Tachikawa.Construction.rhoBimodule line 541
  60. lemma OAI.Tachikawa.Construction.restricted_socle_character line 545
  61. def OAI.Tachikawa.Enveloping.regularUnit line 566
  62. def OAI.Tachikawa.Enveloping.restrictedSingleMap line 571
  63. lemma OAI.Tachikawa.Enveloping.regularUnit_square line 578
  64. def OAI.Tachikawa.exactDerivedHom line 598
  65. lemma OAI.Tachikawa.exactDerivedHom_comp line 605
  66. lemma OAI.Tachikawa.exactDerivedHom_map line 612
  67. def OAI.Tachikawa.HomColumnBoundaries line 627
  68. lemma OAI.Tachikawa.raise_cochain_map line 633
  69. theorem OAI.Tachikawa.cochain_map_supported_nonnegative line 674
  70. lemma OAI.Tachikawa.resolution_HomColumnBoundaries line 693
  71. theorem OAI.Tachikawa.bounded_cochain_resolution_descends line 732
  72. theorem OAI.Tachikawa.bounded_orthogonal_derived_descent line 788
  73. def OAI.Tachikawa.HomRowBoundaries line 810
  74. lemma OAI.Tachikawa.lower_cochain_map line 816
  75. theorem OAI.Tachikawa.cochain_map_supported_nonpositive line 856
  76. lemma OAI.Tachikawa.coresolution_HomRowBoundaries line 875
  77. theorem OAI.Tachikawa.bounded_cochain_coresolution_descends line 912
  78. lemma OAI.Tachikawa.kInjective_chain_representative line 968
  79. theorem OAI.Tachikawa.bounded_orthogonal_derived_descent_dual line 991
  80. theorem OAI.Tachikawa.bounded_ordinary_factorization line 1013