Pulling back a preadditive structure along a fully faithful functor

A preadditive structure on a category D transfers to a preadditive structure on C for a given fully faithful functor F : C ⥤ D.

def CategoryTheory.Preadditive.ofFullyFaithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] {F : Functor C D} (hF : F.FullyFaithful) : Preadditive C

If D is a preadditive category, any fully faithful functor F : C ⥤ D induces a preadditive structure on C.

Equations

• CategoryTheory.Preadditive.ofFullyFaithful hF = { homGroup := fun (P Q : C) => hF.homEquiv.addCommGroup, add_comp := ⋯, comp_add := ⋯ }

theorem CategoryTheory.Functor.FullyFaithful.additive_ofFullyFaithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] {F : Functor C D} (hF : F.FullyFaithful) : F.Additive

The preadditive structure on C induced by a fully faithful functor F : C ⥤ D makes F an additive functor.

theorem CategoryTheory.Equivalence.additive_inverse_of_FullyFaithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] (e : C ≌ D) : e.inverse.Additive

The preadditive structure on C induced by an equivalence e : C ≌ D makes e.inverse an additive functor.