OAI/RingTheory/Tachikawa/CompleteResolution.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Tachikawa.CokerAt line 12
  2. instance OAI.Tachikawa.CokerAt.(instance at line 17) line 17
  3. instance OAI.Tachikawa.CokerAt.(instance at line 19) line 19
  4. def OAI.Tachikawa.CokerAt.π line 22
  5. lemma OAI.Tachikawa.CokerAt.π_surjective line 24
  6. lemma OAI.Tachikawa.CokerAt.π_d line 26
  7. def OAI.Tachikawa.CokerAt.ι line 31
  8. lemma OAI.Tachikawa.CokerAt.ι_π line 37
  9. lemma OAI.Tachikawa.CokerAt.ι_comp_π line 39
  10. lemma OAI.Tachikawa.CokerAt.ι_injective line 41
  11. def OAI.Tachikawa.CokerAt.descend line 50
  12. lemma OAI.Tachikawa.CokerAt.descend_π line 56
  13. lemma OAI.Tachikawa.CokerAt.descend_comp_π line 59
  14. def OAI.Tachikawa.ComplexExact line 63
  15. def OAI.Tachikawa.TotallyAcyclic line 66
  16. lemma OAI.Tachikawa.TotallyAcyclic.projective_boundaries line 75
  17. lemma OAI.Tachikawa.TotallyAcyclic.extend_coker line 94
  18. instance OAI.Tachikawa.CokerAt.(instance at line 116) line 116
  19. instance OAI.Tachikawa.CokerAt.(instance at line 118) line 118
  20. lemma OAI.Tachikawa.ComplexExact.adjacent line 122
  21. def OAI.Tachikawa.completeResolutionTail line 129
  22. lemma OAI.Tachikawa.completeResolutionTail_d line 146
  23. lemma OAI.Tachikawa.TotallyAcyclic.factors_iff_boundary line 156
  24. lemma OAI.Tachikawa.TotallyAcyclic.boundaries_of_stableHom line 183
  25. lemma OAI.Tachikawa.TotallyAcyclic.ext_subsingleton_of_stableHom line 196
  26. def OAI.Tachikawa.CokerAt.δ line 227
  27. lemma OAI.Tachikawa.CokerAt.δ_π line 230
  28. lemma OAI.Tachikawa.CokerAt.δ_comp_π line 232
  29. lemma OAI.Tachikawa.CokerAt.δ_injective line 234
  30. lemma OAI.Tachikawa.CokerAt.π_comp_δ line 240
  31. lemma OAI.Tachikawa.CokerAt.δ_π_exact line 247
  32. def OAI.Tachikawa.CokerAt.factorThrough line 258
  33. lemma OAI.Tachikawa.CokerAt.factorThrough_spec line 264
  34. lemma OAI.Tachikawa.TotallyAcyclic.extend_at line 277
  35. structure OAI.Tachikawa.ComparisonStep line 288
  36. lemma OAI.Tachikawa.comparison_step_up line 294
  37. lemma OAI.Tachikawa.comparison_step_down line 312
  38. def OAI.Tachikawa.CompleteLift.up line 334
  39. def OAI.Tachikawa.CompleteLift.upSquare line 338
  40. def OAI.Tachikawa.CompleteLift.down line 342
  41. def OAI.Tachikawa.CompleteLift.downSquare line 346
  42. def OAI.Tachikawa.CompleteLift.cokerMap line 352
  43. lemma OAI.Tachikawa.CompleteLift.cokerMap_zero line 355
  44. lemma OAI.Tachikawa.CompleteLift.cokerMap_up line 358
  45. lemma OAI.Tachikawa.CompleteLift.cokerMap_down line 363
  46. lemma OAI.Tachikawa.CompleteLift.hasSquare_down line 368
  47. lemma OAI.Tachikawa.CompleteLift.hasSquare line 376
  48. def OAI.Tachikawa.CompleteLift.square line 384
  49. def OAI.Tachikawa.CompleteLift.chainMap line 389
  50. def OAI.Tachikawa.CokerAt.map line 410
  51. lemma OAI.Tachikawa.CokerAt.map_π line 420
  52. lemma OAI.Tachikawa.CokerAt.map_comp line 423
  53. lemma OAI.Tachikawa.CokerAt.map_id line 429
  54. theorem OAI.Tachikawa.exists_complete_lift line 435
  55. def OAI.Tachikawa.CokerAt.augmentationEquiv line 459
  56. lemma OAI.Tachikawa.CokerAt.augmentationEquiv_π line 473