Commit 2023-03-11 13:48 e112ddd0

View on Github →

feat: port CategoryTheory.Preadditive.AdditiveFunctor (#2779)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

added def CategoryTheory.AdditiveFunctor.forget

added theorem CategoryTheory.AdditiveFunctor.forget_map

added theorem CategoryTheory.AdditiveFunctor.forget_obj

added theorem CategoryTheory.AdditiveFunctor.forget_obj_of

added def CategoryTheory.AdditiveFunctor.of

added def CategoryTheory.AdditiveFunctor.ofExact

added theorem CategoryTheory.AdditiveFunctor.ofExact_map

added theorem CategoryTheory.AdditiveFunctor.ofExact_obj_fst

added def CategoryTheory.AdditiveFunctor.ofLeftExact

added theorem CategoryTheory.AdditiveFunctor.ofLeftExact_map

added theorem CategoryTheory.AdditiveFunctor.ofLeftExact_obj_fst

added def CategoryTheory.AdditiveFunctor.ofRightExact

added theorem CategoryTheory.AdditiveFunctor.ofRightExact_map

added theorem CategoryTheory.AdditiveFunctor.ofRightExact_obj_fst

added theorem CategoryTheory.AdditiveFunctor.of_fst

added def CategoryTheory.AdditiveFunctor

added theorem CategoryTheory.Functor.additive_of_preservesBinaryBiproducts

added theorem CategoryTheory.Functor.coe_mapAddHom

added def CategoryTheory.Functor.mapAddHom

added theorem CategoryTheory.Functor.map_add

added theorem CategoryTheory.Functor.map_neg

added theorem CategoryTheory.Functor.map_nsmul

added theorem CategoryTheory.Functor.map_sub

added theorem CategoryTheory.Functor.map_sum

added theorem CategoryTheory.Functor.map_zsmul