Theorems · Definition · category theory

CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.MonoidalClosed C] →
        {J : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} J] →
            [inst_4 :
                ∀ (F₁ F₂ : CategoryTheory.Functor J C),
                  CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom C F₁ F₂] →
              {F₁ F₂ F₃ : CategoryTheory.Functor J C} →
                (CategoryTheory.MonoidalCategoryStruct.tensorObj F₁ F₂ ⟶ F₃) ≃
                  (F₂ ⟶ CategoryTheory.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.

Defined in

Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalClosedCategoryTheory.CategoryCategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom