[Merged by Bors] - feat: the derived category of an abelian category

[joelriou]

The derived category of an abelian category is defined and it is shown that it is a triangulated category.

---

• depends on: [Merged by Bors] - feat(CategoryTheory): triangulated subcategories #11740
• depends on: [Merged by Bors] - feat(CategoryTheory): the class of morphisms whose cone belongs to a triangulated subcategory #11789
• depends on: [Merged by Bors] - feat(CategoryTheory/Triangulated): homological functors #11759
• depends on: [Merged by Bors] - feat(CategoryTheory/Triangulated): the long exact sequence of a homological functor #11805
• depends on: [Merged by Bors] - feat(CategoryTheory/Shift): the induced shift sequence #11764
• depends on: [Merged by Bors] - feat(Algebra/Homology): compatibilities of homology and shifts #11782
• depends on: [Merged by Bors] - feat: the homological functor on the homotopy category of cochain complexes in an abelian category #11760
• depends on: [Merged by Bors] - feat(CategoryTheory/Localization): dualize results for right calculus of fractions #11721
• depends on: [Merged by Bors] - feat(CategoryTheory): more lemmas for the calculus of fractions #11737
• depends on: [Merged by Bors] - feat(CategoryTheory/Localization): the localized category is preadditive #11728
• depends on: [Merged by Bors] - feat(CategoryTheory): localization of pretriangulated categories #11738
• depends on: [Merged by Bors] - feat(CategoryTheory): localization of triangulated categories #11786
• depends on: [Merged by Bors] - feat: mapComposableArrows is essentially surjective for localization functors when there is a calculus of fractions #13558

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory): triangulated subcategories #11740
• [Merged by Bors] - feat(CategoryTheory): the class of morphisms whose cone belongs to a triangulated subcategory #11789
• [Merged by Bors] - feat(CategoryTheory/Triangulated): homological functors #11759
• [Merged by Bors] - feat(CategoryTheory/Triangulated): the long exact sequence of a homological functor #11805
• [Merged by Bors] - feat(CategoryTheory/Shift): the induced shift sequence #11764
• [Merged by Bors] - feat(Algebra/Homology): compatibilities of homology and shifts #11782
• [Merged by Bors] - feat: the homological functor on the homotopy category of cochain complexes in an abelian category #11760
• [Merged by Bors] - feat(CategoryTheory/Localization): dualize results for right calculus of fractions #11721
• [Merged by Bors] - feat(CategoryTheory): more lemmas for the calculus of fractions #11737
• [Merged by Bors] - feat(CategoryTheory/Localization): the localized category is preadditive #11728
• [Merged by Bors] - feat(CategoryTheory): localization of pretriangulated categories #11738
• [Merged by Bors] - feat(CategoryTheory): localization of triangulated categories #11786
• [Merged by Bors] - feat: mapComposableArrows is essentially surjective for localization functors when there is a calculus of fractions #13558
  By Dependent Issues (🤖). Happy coding!

[joelriou]

(Note: with omega, irrelevant unnecessary variables were added to the lemma. Using simp solves this issue.)

[github-actions]

PR summary

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Triangulated.Subcategory	958	999	+41 (+4.28%)
Mathlib.CategoryTheory.Triangulated.HomologicalFunctor	1048	1055	+7 (+0.67%)

---

Diff of declarations

+ DerivedCategory
+ HasDerivedCategory.standard
+ Q
+ Qh
+ instance (n : ℤ) : (shiftFunctor (DerivedCategory C) n).Additive
+ instance : Category.{w} (DerivedCategory C)
+ instance : ClosedUnderIsomorphisms (subcategoryAcyclic C).P
+ instance : HasShift (DerivedCategory C) ℤ
+ instance : HasZeroObject (DerivedCategory C)
+ instance : IsTriangulated (DerivedCategory C)
+ instance : Preadditive (DerivedCategory C)
+ instance : Pretriangulated (DerivedCategory C)
+ instance : Qh.IsLocalization (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
+ instance : Qh.IsLocalization (HomotopyCategory.subcategoryAcyclic C).W
+ instance : S.W.IsCompatibleWithShift ℤ
+ instance [IsTriangulated C] : S.W.IsCompatibleWithTriangulation
+ mem_subcategoryAcyclic_iff
+ on
+ quasiIso_eq_subcategoryAcyclic_W
+ quotientCompQhIso
+ quotient_obj_mem_subcategoryAcyclic_iff_exactAt
+ should
+ subcategoryAcyclic
++ instance : (Q (C
+++ instance : (Qh (C

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[erdOne]

Thanks!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[jcommelin]

Thanks 🎉 This is a massive milestone! Huge kudos!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style