Theorems · Theorem · category theory

CategoryTheory.NatTrans.whiskerRight_app_tensor_app

∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.MonoidalCategory C]
  {F G F' G' : CategoryTheory.Functor J C} (α : F ⟶ F') (β : G ⟶ G') {X Y : J} (f : X ⟶ Y) (X' : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (G.obj X'))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app Y) (β.app X')) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app X) (β.app X'))
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F'.map f) (G'.obj X'))

Defined in

Mathlib.CategoryTheory.Monoidal.Category

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategory