Theorems · Theorem · category theory

CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorHom_eq

∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {V : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} V}
  {inst_2 : CategoryTheory.MonoidalCategory C} {inst_3 : CategoryTheory.MonoidalCategory V} {D : Type u₃}
  {inst_4 : CategoryTheory.Category.{v₃, u₃} D}
  [self : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D]
  {d₁ d₂ d₁' d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂'),
  (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map
      (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorHom f f') =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObjIsoConvolution C V
          d₁ d₁').hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.DayConvolution.map
          ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map f)
          ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map f'))
        (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObjIsoConvolution C
            V d₂ d₂').inv)

Lawfulness of tensorHom.

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore