Theorems · Theorem · category theory

CategoryTheory.GradedObject.Monoidal.tensorHom_comp_tensorHom

∀ {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₃],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ g₁)
      (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ g₂) =
    CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.comp f₁ f₂)
      (CategoryTheory.CategoryStruct.comp g₁ g₂)

Defined in

Mathlib.CategoryTheory.GradedObject.Monoidal

Cited by

3 results in Mathlib

Foundations

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

Assumes

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