CategoryTheory.monoidalPreadditive_of_faithful

theorem CategoryTheory.monoidalPreadditive_of_faithful : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C] {D : Type u_2} [inst_4 : CategoryTheory.Category.{u_3, u_2} D] [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor D C) [inst_7 : F.Faithful] [inst : F.Additive], CategoryTheory.MonoidalPreadditive D

The theorem `CategoryTheory.monoidalPreadditive_of_faithful` states that given any category `C` that is both a monoidal category and a preadditive category, along with a category `D` that is a monoidal category, if there exists a monoidal functor `F` from `D` to `C` which is faithful and additive, then `D` is also a monoidal preadditive category. In simpler terms, a faithful additive monoidal functor from `D` to a monoidal preadditive category `C` is enough to ensure that `D` itself is a monoidal preadditive category.

More concisely: A faithful additive monoidal functor from a monoidal category `D` to a monoidal preadditive category `C` implies that `D` is a monoidal preadditive category.