Theorems · Theorem · category theory

CategoryTheory.Functor.Monoidal.tensorObjComp_hom_app

∀ {C : Type u_2} {D : Type u_3} {E : Type u_4} [inst : CategoryTheory.Category.{v_2, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} E]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory C] [inst_4 : CategoryTheory.CartesianMonoidalCategory E]
  (F G : CategoryTheory.Functor D C) (H : CategoryTheory.Functor C E)
  [inst_5 : CategoryTheory.Limits.PreservesFiniteProducts H] (X : D),
  (CategoryTheory.Functor.Monoidal.tensorObjComp F G H).hom.app X =
    CategoryTheory.CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X)

Defined in

Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategoryCategoryTheory.CartesianMonoidalCategoryCategoryTheory.Limits.PreservesFiniteProducts