Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.lawfulDayConvolutionMonoidalCategoryStructOfHasDayConvolutions

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            {D : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} D] →
                (ι : CategoryTheory.Functor D (CategoryTheory.Functor C V)) →
                  (ffι : ι.FullyFaithful) →
                    [hasDayConvolution :
                        ∀ (d d' : D),
                          (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
                            (CategoryTheory.MonoidalCategory.externalProduct (ι.obj d) (ι.obj d'))] →
                      (essImageDayConvolution :
                          ∀ (d d' : D),
                            ι.essImage
                              ((CategoryTheory.MonoidalCategory.tensor C).pointwiseLeftKanExtension
                                (CategoryTheory.MonoidalCategory.externalProduct (ι.obj d) (ι.obj d')))) →
                        [hasDayConvolutionUnit :
                            (CategoryTheory.Functor.fromPUnit
                                  (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
                              (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))] →
                          (essImageDayConvolutionUnit :
                              ι.essImage
                                ((CategoryTheory.Functor.fromPUnit
                                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).pointwiseLeftKanExtension
                                  (CategoryTheory.Functor.fromPUnit
                                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)))) →
                            [inst_5 :
                                ∀ (v : V) (d : C),
                                  CategoryTheory.Limits.PreservesColimitsOfShape
                                    (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
                                    (CategoryTheory.MonoidalCategory.tensorLeft v)] →
                              [inst_6 :
                                  ∀ (v : V) (d : C),
                                    CategoryTheory.Limits.PreservesColimitsOfShape
                                      (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
                                      (CategoryTheory.MonoidalCategory.tensorRight v)] →
                                [inst_7 :
                                    ∀ (v : V) (d : C),
                                      CategoryTheory.Limits.PreservesColimitsOfShape
                                        (CategoryTheory.CostructuredArrow
                                          (CategoryTheory.Functor.fromPUnit
                                            (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                          d)
                                        (CategoryTheory.MonoidalCategory.tensorLeft v)] →
                                  [inst_8 :
                                      ∀ (v : V) (d : C),
                                        CategoryTheory.Limits.PreservesColimitsOfShape
                                          (CategoryTheory.CostructuredArrow
                                            (CategoryTheory.Functor.fromPUnit
                                              (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                            d)
                                          (CategoryTheory.MonoidalCategory.tensorRight v)] →
                                    [inst_9 :
                                        ∀ (v : V) (d : C × C),
                                          CategoryTheory.Limits.PreservesColimitsOfShape
                                            (CategoryTheory.CostructuredArrow
                                              ((CategoryTheory.Functor.id C).prod
                                                (CategoryTheory.Functor.fromPUnit
                                                  (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
                                              d)
                                            (CategoryTheory.MonoidalCategory.tensorRight v)] →
                                      [inst_10 :
                                          ∀ (v : V) (d : C × C),
                                            CategoryTheory.Limits.PreservesColimitsOfShape
                                              (CategoryTheory.CostructuredArrow
                                                ((CategoryTheory.MonoidalCategory.tensor C).prod
                                                  (CategoryTheory.Functor.id C))
                                                d)
                                              (CategoryTheory.MonoidalCategory.tensorRight v)] →
                                        CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D

The monoidal category constructed via monoidalOfHasDayConvolutions has a canonical LawfulDayConvolutionMonoidalCategoryStruct C V D.

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution

Cited by

0 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategoryCategoryTheory.CategoryCategoryTheory.Functor.HasPointwiseLeftKanExtensionCategoryTheory.Functor.HasPointwiseLeftKanExtensionCategoryTheory.Limits.PreservesColimitsOfShapeCategoryTheory.Limits.PreservesColimitsOfShapeCategoryTheory.Limits.PreservesColimitsOfShapeCategoryTheory.Limits.PreservesColimitsOfShapeCategoryTheory.Limits.PreservesColimitsOfShapeCategoryTheory.Limits.PreservesColimitsOfShape