Theorems · Theorem · category theory

CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc

∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C}
  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Z₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
        (CategoryTheory.CategoryStruct.comp f₂ g₂))
      h

Composition of tensor products is tensor product of compositions: (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = (f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂)

Defined in

Mathlib.CategoryTheory.Monoidal.Category

Cited by

14 results in Mathlib

Foundations

Depth 6 from the axioms · uses Quot.sound

Assumes

CategoryTheory.MonoidalCategory