feat(CategoryTheory/Localization): the localized category is preadditive

[joelriou]

trafficstars

In this PR, it is shown that if W : MorphismProperty C has a left calculus of fractions and C is preadditive, then the localized category is also preadditive.

---

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

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

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

[jcommelin]

LGTM, two minor comments (Sorry for resolving the merge conflict... I realized too late that this might mess with your multi-stacked-mega-PR-DAG.)

bors d+

[joelriou]

Thanks for the review!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style