Theorems · Theorem · category theory

CategoryTheory.MonoidalCategory.DayConvolution.associator_hom_unit_unit_assoc

∀ {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)]
  (x y z : C) {Z : V}
  (h :
    (CategoryTheory.MonoidalCategory.DayConvolution.convolution F
            (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)).obj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) z) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y)) (H.obj z))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayConvolution.unit
              (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H).app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj x y, z))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.MonoidalCategory.DayConvolution.associator F G H).hom.app
            (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) z))
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj x) (G.obj y) (H.obj z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x)
          ((CategoryTheory.MonoidalCategory.DayConvolution.unit G H).app (y, z)))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.MonoidalCategory.DayConvolution.unit F
                (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)).app
            (x, CategoryTheory.MonoidalCategoryStruct.tensorObj y z))
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F
                  (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)).map
              (CategoryTheory.MonoidalCategoryStruct.associator x y z).inv)
            h)))

Characterizing the forward direction of the associator isomorphism with respect to the unit transformations.

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution

Cited by

4 results in Mathlib

Foundations

Depth 58 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.PreservesColimitsOfShape