feat(category_theory/abelian/additive_functor): Adds definition of additive functors (#6367)
This PR adds the basic definition of an additive functor.
See associated [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Additive.20functors/near/227295322).
Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>