Commit 2021-04-06 05:50 6aa0e30e

feat(category_theory/preadditive): additive functors preserve biproducts (#6882) An additive functor between preadditive categories creates and preserves biproducts. Also, renames src/category_theory/abelian/additive_functor.lean to src/category_theory/preadditive/additive_functor.lean as it so far doesn't actually rely on anything being abelian. Also, moves the .map_X lemmas about additive functors into the functor namespace, so we can use dot notation F.map_add etc, when [functor.additive F] is available.