Right adjoints between preadditive categories are additive

A right adjoint between preadditive categories preserves binary products and zero morphisms, so it is additive as soon as its source has binary products. Mathlib records this fact only for the functor of a MoritaEquivalence; this file records it as an instance for every right adjoint. In particular it applies to every functor that is an equivalence, through Mathlib's CategoryTheory.Functor.isRightAdjoint_of_isEquivalence, and so to both directions e.functor and e.inverse of an equivalence e. This makes the Grothendieck groups of module categories and the Cartan map functorial along equivalences of module categories, and lets finite biproducts be transported along them, as in the Krull-Schmidt theorem for quiver representations.

Some hypothesis on the source is needed: an equivalence between one-object preadditive categories is an isomorphism of the multiplicative monoids of their endomorphism rings, which need not be additive.

instance CategoryTheory.Functor.additive_of_isRightAdjoint {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasBinaryProducts C] (F : Functor C D) [F.IsRightAdjoint] : F.Additive

A right adjoint between preadditive categories is additive, provided its source has binary products.