English
A faithful linear monoidal functor to a linear monoidal category endows the domain with a compatible linear monoidal structure.
Русский
Верный линейный моноидальный функтор в линейную моноидальную категорию наделяет область совместимой линейной моноидальной структурой.
LaTeX
$$$\\text{MonoidalLinear } R D$$$
Lean4
/-- A faithful linear monoidal functor to a linear monoidal category
ensures that the domain is linear monoidal. -/
theorem monoidalLinearOfFaithful {D : Type*} [Category D] [Preadditive D] [Linear R D] [MonoidalCategory D]
[MonoidalPreadditive D] (F : D ⥤ C) [F.Monoidal] [F.Faithful] [F.Linear R] : MonoidalLinear R D :=
{ whiskerLeft_smul := by
intro X Y Z r f
apply F.map_injective
rw [Functor.Monoidal.map_whiskerLeft]
simp
smul_whiskerRight := by
intro r X Y f Z
apply F.map_injective
rw [Functor.Monoidal.map_whiskerRight]
simp }
