feat(CategoryTheory): localization of pretriangulated categories

[joelriou]

In this file, it is shown that if a class of morphisms W in a pretriangulated category is compatible with the triangulation and has a left calculus of fractions, then the localized category is also pretriangulated.

---

• [ ] depends on: #11737
• [ ] depends on: #11721
• [ ] depends on: #11728

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#11737~~
• ~~leanprover-community/mathlib4#11721~~
• ~~leanprover-community/mathlib4#11728~~ By Dependent Issues (🤖). Happy coding!

[joelriou]

Thanks @erdOne for the fix!

[erdOne]

Thanks! maintainer merge

[github-actions[bot]]

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

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style