English
Compatibility of the map ι with tensor-hom under the LawfulDayConvolutionMonoidalCategoryStruct hypotheses.
Русский
Совместимость ι с тензор-гом в условиях LawfulDayConvolutionMonoidalCategoryStruct.
LaTeX
$$$ (ι C V D).map (f f') = DayConvolution.map ((ι C V D).map f) ((ι C V D).map f') $$$
Lean4
/-- Under suitable assumptions on existence of relevant Kan extensions and preservation
of relevant colimits by the tensor product of `V`, we can define a `MonoidalCategory D`
from the data of a fully faithful functor `ι : D ⥤ C ⥤ V` whose essential image
contains a Day convolution unit and is stable under binary Day convolutions. -/
noncomputable def monoidalOfHasDayConvolutions : MonoidalCategory D :=
letI induced : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D :=
.ofHasDayConvolutions ι ffι essImageDayConvolution essImageDayConvolutionUnit
letI := induced.mkMonoidalCategoryStruct
letI : LawfulDayConvolutionMonoidalCategoryStruct C V D := induced.mkLawfulDayConvolutionMonoidalCategoryStruct
monoidalOfLawfulDayConvolutionMonoidalCategoryStruct C V D
