Theorems · Theorem · category theory

CategoryTheory.NatTrans.tensor_naturality

∀ {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 X' Y' : J} (f : X ⟶ Y) (g : X' ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (G.map g))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app Y) (β.app Y')) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app X) (β.app X'))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (F'.map f) (G'.map g))

Defined in

Mathlib.CategoryTheory.Monoidal.Category

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategory