Theorems · Theorem · category theory

CategoryTheory.GradedObject.Monoidal.tensorHom_comp_tensorHom_assoc

∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C} (f₁ : X₁ ⟶ X₂)
  (f₂ : X₂ ⟶ X₃) (g₁ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃) [inst_3 : X₁.HasTensor Y₁] [inst_4 : X₂.HasTensor Y₂]
  [inst_5 : X₃.HasTensor Y₃] {Z : CategoryTheory.GradedObject I C}
  (h : CategoryTheory.GradedObject.Monoidal.tensorObj X₃ Y₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ g₁)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ g₂) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.comp f₁ f₂)
        (CategoryTheory.CategoryStruct.comp g₁ g₂))
      h

Defined in

Mathlib.CategoryTheory.GradedObject.Monoidal

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddMonoidCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasTensor