English
If D is a category with a faithful additive monoidal functor F: D → C into a monoidal preadditive category C, and F is monoidal and additive, then D inherits a MonoidalPreadditive structure.
Русский
Если существует наблюдаемо-верный аддитивный моноидальный функтор F: D → C в моноидальную предадитивную категорию C, и F моноидальный и аддитивный, то D наследует структуру моноидативной предадитивности.
LaTeX
$$$\\text{MonoidalPreadditive}(D)$$$
Lean4
/-- A faithful additive monoidal functor to a monoidal preadditive category
ensures that the domain is monoidal preadditive. -/
theorem monoidalPreadditive_of_faithful {D} [Category D] [Preadditive D] [MonoidalCategory D] (F : D ⥤ C) [F.Monoidal]
[F.Faithful] [F.Additive] : MonoidalPreadditive D :=
{ whiskerLeft_zero := by
intros
apply F.map_injective
simp [Functor.Monoidal.map_whiskerLeft]
zero_whiskerRight := by
intros
apply F.map_injective
simp [Functor.Monoidal.map_whiskerRight]
whiskerLeft_add := by
intros
apply F.map_injective
simp only [Functor.Monoidal.map_whiskerLeft, Functor.map_add, Preadditive.comp_add, Preadditive.add_comp,
MonoidalPreadditive.whiskerLeft_add]
add_whiskerRight := by
intros
apply F.map_injective
simp only [Functor.Monoidal.map_whiskerRight, Functor.map_add, Preadditive.comp_add, Preadditive.add_comp,
MonoidalPreadditive.add_whiskerRight] }
