CategoryTheory.monoidalLinearOfFaithful

theorem CategoryTheory.monoidalLinearOfFaithful : ∀ (R : Type u_1) [inst : Semiring R] {C : Type u_2} [inst_1 : CategoryTheory.Category.{u_5, u_2} C] [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : CategoryTheory.MonoidalCategory C] [inst_5 : CategoryTheory.MonoidalPreadditive C] [inst_6 : CategoryTheory.MonoidalLinear R C] {D : Type u_3} [inst_7 : CategoryTheory.Category.{u_4, u_3} D] [inst_8 : CategoryTheory.Preadditive D] [inst_9 : CategoryTheory.Linear R D] [inst_10 : CategoryTheory.MonoidalCategory D] [inst_11 : CategoryTheory.MonoidalPreadditive D] (F : CategoryTheory.MonoidalFunctor D C) [inst_12 : F.Faithful] [inst_13 : F.Additive] [inst_14 : CategoryTheory.Functor.Linear R F.toFunctor], CategoryTheory.MonoidalLinear R D

This theorem states that if we have a faithful and additive linear monoidal functor `F` from a category `D` to a category `C`, where both categories `C` and `D` are linear, preadditive, and monoidal, then the domain category `D` is also monoidal linear. Here, `R` is a semiring that provides the scalar multiplication for the linear structure. In simpler terms, if we have a structure-preserving mapping from `D` to `C`, and `C` has a certain property (monoidal linear), then `D` must also have that property.

More concisely: If `F: D → C` is a faithful, additive, and monoidal functor between linear, preadditive and monoidal categories `D` and `C`, then `D` is a monoidal linear category.