Functor categories are monoidal closed

Let C be a monoidal closed category. Let J be a category. In this file, we obtain that the category J ⥤ C is monoidal closed if C has suitable limits.

noncomputable def CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [MonoidalClosed C] {J : Type u₂} [Category.{v₂, u₂} J] [∀ (F₁ F₂ : Functor J C), Enriched.FunctorCategory.HasFunctorEnrichedHom C F₁ F₂] {F₁ F₂ F₃ : Functor J C} : (MonoidalCategoryStruct.tensorObj F₁ F₂ ⟶ F₃) ≃ (F₂ ⟶ Enriched.FunctorCategory.functorEnrichedHom C F₁ F₃)

The bijection (F₁ ⊗ F₂ ⟶ F₃) ≃ (F₂ ⟶ functorEnrichedHom C F₁ F₃) when F₁, F₂ and F₃ are functors J ⥤ C, and C is monoidal closed.

theorem CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_two_symm {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [MonoidalClosed C] {J : Type u₂} [Category.{v₂, u₂} J] [∀ (F₁ F₂ : Functor J C), Enriched.FunctorCategory.HasFunctorEnrichedHom C F₁ F₂] {F₁ F₂ F₂' F₃ : Functor J C} (f₂ : F₂ ⟶ F₂') (g : F₂' ⟶ Enriched.FunctorCategory.functorEnrichedHom C F₁ F₃) : homEquiv.symm (CategoryStruct.comp f₂ g) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft F₁ f₂) (homEquiv.symm g)

theorem CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_three {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [MonoidalClosed C] {J : Type u₂} [Category.{v₂, u₂} J] [∀ (F₁ F₂ : Functor J C), Enriched.FunctorCategory.HasFunctorEnrichedHom C F₁ F₂] {F₁ F₂ F₃ F₃' : Functor J C} [∀ (F₁ F₂ : Functor J C), Enriched.FunctorCategory.HasEnrichedHom C F₁ F₂] (f : MonoidalCategoryStruct.tensorObj F₁ F₂ ⟶ F₃) (f₃ : F₃ ⟶ F₃') : homEquiv (CategoryStruct.comp f f₃) = CategoryStruct.comp (homEquiv f) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (Enriched.FunctorCategory.functorEnrichedHom C F₁ F₃)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (Enriched.FunctorCategory.functorEnrichedHom C F₁ F₃) ((Enriched.FunctorCategory.functorHomEquiv C) f₃)) (Enriched.FunctorCategory.functorEnrichedComp C F₁ F₃ F₃')))

noncomputable def CategoryTheory.MonoidalClosed.FunctorCategory.adj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [MonoidalClosed C] {J : Type u₂} [Category.{v₂, u₂} J] [∀ (F₁ F₂ : Functor J C), Enriched.FunctorCategory.HasFunctorEnrichedHom C F₁ F₂] [∀ (F₁ F₂ : Functor J C), Enriched.FunctorCategory.HasEnrichedHom C F₁ F₂] (F : Functor J C) : MonoidalCategory.tensorLeft F ⊣ (eHomFunctor (Functor J C) (Functor J C)).obj (Opposite.op F)

When C is monoidal closed and has suitable limits, then for any F : J ⥤ C, tensorLeft F has a right adjoint.

noncomputable def CategoryTheory.MonoidalClosed.FunctorCategory.closed {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [MonoidalClosed C] {J : Type u₂} [Category.{v₂, u₂} J] [∀ (F₁ F₂ : Functor J C), Enriched.FunctorCategory.HasFunctorEnrichedHom C F₁ F₂] [∀ (F₁ F₂ : Functor J C), Enriched.FunctorCategory.HasEnrichedHom C F₁ F₂] (F : Functor J C) : Closed F

When C is monoidal closed and has suitable limits, then for any F : J ⥤ C, tensorLeft F has a right adjoint.

noncomputable def CategoryTheory.MonoidalClosed.FunctorCategory.monoidalClosed {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [MonoidalClosed C] {J : Type u₂} [Category.{v₂, u₂} J] [∀ (F₁ F₂ : Functor J C), Enriched.FunctorCategory.HasFunctorEnrichedHom C F₁ F₂] [∀ (F₁ F₂ : Functor J C), Enriched.FunctorCategory.HasEnrichedHom C F₁ F₂] : MonoidalClosed (Functor J C)

If C is monoidal closed and has suitable limits, the functor category J ⥤ C is monoidal closed.