English
Under assumptions there is a monoidal category on D constructed from Day convolution data via a fully faithful functor ι.
Русский
При заданных условиях существует моноидальная категория на D, конструируемая Day-конволюцией через ι.
LaTeX
$$$ \text{monoidalOfHasDayConvolutions }(ι,ffι,...) = \text{MonoidalCategory } D $$$
Lean4
@[to_additive (attr := simps tensorObj_as leftUnitor rightUnitor associator) Discrete.addMonoidal]
instance monoidal : MonoidalCategory (Discrete M)
where
tensorUnit := Discrete.mk 1
tensorObj X Y := Discrete.mk (X.as * Y.as)
whiskerLeft X _ _ f := eqToHom (by rw [eq_of_hom f])
whiskerRight f X := eqToHom (by rw [eq_of_hom f])
tensorHom f g := eqToHom (by rw [eq_of_hom f, eq_of_hom g])
leftUnitor X := Discrete.eqToIso (one_mul X.as)
rightUnitor X := Discrete.eqToIso (mul_one X.as)
associator _ _ _ := Discrete.eqToIso (mul_assoc _ _ _)
