Theorems · Inductive type · category theory

CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct

(C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (V : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalCategory V] →
            (D : Type u₃) →
              [inst : CategoryTheory.Category.{v₃, u₃} D] →
                [CategoryTheory.MonoidalCategoryStruct D] → Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)

The class DayConvolutionMonoidalCategory C V D bundles the necessary data to turn a monoidal category D into a monoidal full subcategory of a category of functors C ⥤ V endowed with a Day convolution monoidal structure. The design of this class is to bundle a fully faithful functor into C ⥤ V with left extensions on its values representing the fact that it maps tensors products in D to Day convolutions, and furthermore ask that this data is "lawful", i.e that once realized in the functor category, the objects behave like the corresponding ones in the category C ⥤ V.

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution

Cited by

10 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryStruct