Commit 2021-02-24 03:38 358fdf23

View on Github →

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.

Estimated changes

Created src/category_theory/abelian/additive_functor.lean

added theorem category_theory.functor.additive.map_neg

added theorem category_theory.functor.additive.map_sub

added theorem category_theory.functor.coe_map_add_hom

added def category_theory.functor.map_add_hom