Theorems · Theorem · category theory

CategoryTheory.MonoidalCategory.DayConvolution.associator_naturality

∀ {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]
  {F G : CategoryTheory.Functor C V} [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  {H : CategoryTheory.Functor C V} [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution G H]
  [inst_6 :
    CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)]
  [inst_7 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H]
  [inst_8 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_9 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  {F' G' H' : CategoryTheory.Functor C V} [inst_10 : CategoryTheory.MonoidalCategory.DayConvolution F' G']
  [inst_11 : CategoryTheory.MonoidalCategory.DayConvolution G' H']
  [inst_12 :
    CategoryTheory.MonoidalCategory.DayConvolution F'
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution G' H')]
  [inst_13 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F' G')
      H']
  (f : F ⟶ F') (g : G ⟶ G') (h : H ⟶ H'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.MonoidalCategory.DayConvolution.map f g) h)
      (CategoryTheory.MonoidalCategory.DayConvolution.associator F' G' H').hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator F G H).hom
      (CategoryTheory.MonoidalCategory.DayConvolution.map f (CategoryTheory.MonoidalCategory.DayConvolution.map g h))

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategory.DayConvolutionCategoryTheory.MonoidalCategory.DayConvolutionCategoryTheory.MonoidalCategory.DayConvolutionCategoryTheory.MonoidalCategory.DayConvolutionCategoryTheory.Limits.PreservesColimitsOfShapeCategoryTheory.Limits.PreservesColimitsOfShapeCategoryTheory.MonoidalCategory.DayConvolutionCategoryTheory.MonoidalCategory.DayConvolutionCategoryTheory.MonoidalCategory.DayConvolutionCategoryTheory.MonoidalCategory.DayConvolution