Theorems · Theorem · category theory

Bimod.whiskerRight_hom

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z : CategoryTheory.Mon C} {M₁ M₂ : Bimod X Y} (f : M₁ ⟶ M₂) (N : Bimod Y Z),
  (Bimod.whiskerRight f N).hom =
    CategoryTheory.Limits.colimMap
      (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight M₁.actRight N.X)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M₁.X Y.X N.X).hom
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M₁.X N.actLeft))
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight M₂.actRight N.X)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M₂.X Y.X N.X).hom
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M₂.X N.actLeft))
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Y.X) N.X)
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom N.X) ⋯ ⋯)

Defined in

Mathlib.CategoryTheory.Monoidal.Bimod

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.Limits.HasCoequalizersCategoryTheory.Limits.PreservesColimitsOfSizeCategoryTheory.Limits.PreservesColimitsOfSize