feat(category_theory/abelian): abelian categories (#2817)
~~Depends on #2779.~~ Closes #2178. I will give instances for `AddCommGroup` and `Module`, but since this PR is large already, I'll wait until the next PR with that.
Co-authored-by: Johan Commelin <johan@commelin.net>
