Equivalences of preadditive categories are additive #
The functor of an equivalence between preadditive categories preserves binary products and zero
morphisms, so it is additive as soon as the source has binary products. Mathlib records this fact
for the functor of a MoritaEquivalence; this file records it as an instance for every
equivalence, so that the Grothendieck-group functoriality of additive functors applies to
equivalences of module categories without further hypotheses. The inverse is then additive by
Mathlib's CategoryTheory.Equivalence.inverse_additive.
instance
CategoryTheory.Equivalence.functor_additive
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[Preadditive C]
[Preadditive D]
[Limits.HasBinaryProducts C]
(e : C ≌ D)
:
The functor of an equivalence between preadditive categories with binary products is additive.