Commit 2025-08-28 18:47 7e6436d6

feat(CategoryTheory/Monoidal/DayConvolution): LawfulDayConvolutionMonoidalCategoryStruct (#26798) Given monoidal categories C, V and a category D with a pre-existing MonoidalCategoryStruct, we introduce a typeclass LawfulDayConvolutionMonoidalCategoryStruct C V D that bundles the required data and equations that the structure on D must have to be a monoidal subcategory of C ⥤ V if the latter was endowed with the day convolution monoidal structure. The data in question is that of a faithful functor ι : D ⥤ C ⥤ V, as well as explicit natural transformations ι.obj d ⊠ (ι.obj d') ⟶ tensor C ⋙ ι.obj (d ⊗ d') that exhibit ι.obj (d ⊗ d') as a Day convolution of ι.obj d and (ι.obj d'), as well as similar data asserting that ι.obj (𝟙_ D) is a Day convolution unit. The equations required are identical to the ones that characterize the unitors and associators for Day convolution with respect to the Kan extensions units. Given such a structure, using that the corresponding relations hold in C ⥤ V, we show that the monoidal category structure on D defines a MonoidalCategory D, i.e that all the required equations such as the pentagon/triangular equalities, bifunctoriality of the tensor product etc. are satisfied. Thus, we can think of LawfulDayConvolutionMonoidalCategoryStruct C V D as a constructor for monoidal categories. While this is a step towards a Day convolution monoidal structure in (a type alias) C ⥤ V, the framework is yet incomplete, as it assumes a pre-existing monoidal category structure. We will give constructors for (MonoidalCategoryStruct and) LawfulDayConvolutionMonoidalCategoryStruct C V D with various degree of definitional control over the resulting structure in a forthcoming PR.