OAI/RingTheory/Tachikawa/Perfect.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Tachikawa.cokerLinearEquiv line 12
  2. def OAI.Tachikawa.resolutionReflectCokerEquiv line 26
  3. lemma OAI.Tachikawa.FiniteModule.pos_cover_exact line 41
  4. def OAI.Tachikawa.FiniteModule.naturalCokerPositiveEquiv line 51
  5. def OAI.Tachikawa.FiniteModule.reflectCokerPositiveEquiv line 61
  6. abbrev OAI.Tachikawa.Construction.natJJ line 75
  7. abbrev OAI.Tachikawa.Construction.natJJDouble line 77
  8. abbrev OAI.Tachikawa.Construction.intJJDouble line 79
  9. def OAI.Tachikawa.Construction.jjNatIntX line 82
  10. lemma OAI.Tachikawa.Construction.ι_jjNatIntX line 87
  11. def OAI.Tachikawa.Construction.jjIntNatComponent line 93
  12. def OAI.Tachikawa.Construction.jjIntNatX line 102
  13. lemma OAI.Tachikawa.Construction.ι_jjIntNatX line 105
  14. def OAI.Tachikawa.Construction.jjNatIntIso line 110
  15. lemma OAI.Tachikawa.Construction.forwardJ_d_nat line 135
  16. lemma OAI.Tachikawa.Construction.forwardJ_d_bottom line 140
  17. lemma OAI.Tachikawa.Construction.jjNatInt_d₁ line 148
  18. lemma OAI.Tachikawa.Construction.natIntSign line 171
  19. lemma OAI.Tachikawa.Construction.jjNatInt_d₂ line 175
  20. lemma OAI.Tachikawa.Construction.jjNatInt_d line 198
  21. def OAI.Tachikawa.Construction.jjNatIntCokerEquiv line 209
  22. abbrev OAI.Tachikawa.StableMap line 225
  23. structure OAI.Tachikawa.StableEquiv line 228
  24. lemma OAI.Tachikawa.stableClass_eq_iff line 236
  25. def OAI.Tachikawa.stablePrecompose line 241
  26. lemma OAI.Tachikawa.stablePrecompose_class line 245
  27. def OAI.Tachikawa.StableEquiv.refl line 251
  28. def OAI.Tachikawa.StableEquiv.symm line 257
  29. def OAI.Tachikawa.StableEquiv.ofLinearEquiv line 263
  30. lemma OAI.Tachikawa.StableEquiv.post_inverse line 273
  31. lemma OAI.Tachikawa.StableEquiv.pre_inverse line 279
  32. def OAI.Tachikawa.StableEquiv.post line 285
  33. def OAI.Tachikawa.StableEquiv.pre line 298
  34. def OAI.Tachikawa.StableEquiv.trans line 311
  35. abbrev OAI.Tachikawa.NatCoker.obj line 347
  36. def OAI.Tachikawa.NatCoker.map line 349
  37. lemma OAI.Tachikawa.NatCoker.map_π line 358
  38. lemma OAI.Tachikawa.NatCoker.map_id line 361
  39. lemma OAI.Tachikawa.NatCoker.map_comp line 367
  40. lemma OAI.Tachikawa.NatCoker.homotopy_factors line 374
  41. def OAI.Tachikawa.NatCoker.stableEquiv line 400
  42. lemma OAI.Tachikawa.Construction.reverseJJ_above line 420
  43. def OAI.Tachikawa.Construction.jjFiberHighEquiv line 423
  44. lemma OAI.Tachikawa.Construction.jjFiberHighEquiv_apply line 430
  45. def OAI.Tachikawa.Construction.jjFiberHighCokerEquiv line 433
  46. def OAI.Tachikawa.Construction.natJJFiveFiberEquiv line 446
  47. def OAI.Tachikawa.Enveloping.evalCokerIso line 459
  48. lemma OAI.Tachikawa.goodComponent_up_at line 477
  49. lemma OAI.Tachikawa.tail_initial_component line 520
  50. lemma OAI.Tachikawa.exact_tail_at line 555
  51. def OAI.Tachikawa.TailNull.State line 568
  52. def OAI.Tachikawa.TailNull.up line 574
  53. def OAI.Tachikawa.TailNull.stateMap line 581
  54. def OAI.Tachikawa.TailNull.Step line 585
  55. lemma OAI.Tachikawa.TailNull.up_step line 588
  56. def OAI.Tachikawa.TailNull.component line 597
  57. lemma OAI.Tachikawa.TailNull.component_up line 601
  58. lemma OAI.Tachikawa.TailNull.hasStep line 605
  59. def OAI.Tachikawa.TailNull.hom line 612
  60. lemma OAI.Tachikawa.TailNull.hom_zero line 615
  61. lemma OAI.Tachikawa.TailNull.nullHomotopicMap_f line 618
  62. def OAI.Tachikawa.Cutoff.term line 640
  63. lemma OAI.Tachikawa.Cutoff.d_mem line 642
  64. def OAI.Tachikawa.Cutoff.differential line 656
  65. lemma OAI.Tachikawa.Cutoff.differential_val line 659
  66. def OAI.Tachikawa.Cutoff.complex line 662
  67. def OAI.Tachikawa.Cutoff.inclusion line 677
  68. def OAI.Tachikawa.Cutoff.lift line 683
  69. lemma OAI.Tachikawa.Cutoff.lift_inclusion line 698
  70. lemma OAI.Tachikawa.Cutoff.term_subsingleton line 703
  71. lemma OAI.Tachikawa.Cutoff.term_projective line 707
  72. lemma OAI.Tachikawa.Cutoff.term_finite line 717
  73. lemma OAI.Tachikawa.Cutoff.term_subsingleton_below line 726
  74. theorem OAI.Tachikawa.perfect_factorization line 742
  75. theorem OAI.Tachikawa.cochain_perfect_factorization line 798
  76. lemma OAI.Tachikawa.projectiveResolution_reflect_exact line 844
  77. theorem OAI.Tachikawa.stably_nonzero_high_lift line 856
  78. theorem OAI.Tachikawa.exists_stably_nonzero_high_lift line 892
  79. def OAI.Tachikawa.Enveloping.resRegularUnderlying line 925
  80. abbrev OAI.Tachikawa.Enveloping.restrictedOuterRegular line 936
  81. def OAI.Tachikawa.Enveloping.restrictedOuterRegularUnderlying line 941
  82. lemma OAI.Tachikawa.Enveloping.restrictedOuterRegularUnderlying_tmul line 947
  83. lemma OAI.Tachikawa.Enveloping.restrictedOuterRegular_action line 953
  84. def OAI.Tachikawa.Enveloping.restrictedOuterRegularEquiv line 970
  85. def OAI.Tachikawa.Enveloping.restrictedOuterRegularIso line 976
  86. lemma OAI.Tachikawa.ext_subsingleton_retract_left line 991
  87. lemma OAI.Tachikawa.ext_subsingleton_retract_right line 999
  88. def OAI.Tachikawa.InAdd line 1008
  89. lemma OAI.Tachikawa.ext_subsingleton_inAdd_left line 1010
  90. lemma OAI.Tachikawa.ext_subsingleton_inAdd_right line 1017