feat(category_theory/abelian): right derived functor (#12841)
This pr dualises derived.lean. Right derived functor and natural transformation between right derived functors and related lemmas are formalised.
The docs string currently contains more than what is in this file, but everything else will come shortly after.
