Theorems · Definition · category theory

CategoryTheory.MonoidalClosed.FunctorCategory.adj

{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₂] →
              [inst_5 :
                  ∀ (F₁ F₂ : CategoryTheory.Functor J C),
                    CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom C F₁ F₂] →
                (F : CategoryTheory.Functor J C) →
                  CategoryTheory.MonoidalCategory.tensorLeft F ⊣
                    (CategoryTheory.eHomFunctor (CategoryTheory.Functor J C) (CategoryTheory.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.

Defined in

Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalClosedCategoryTheory.CategoryCategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHomCategoryTheory.Enriched.FunctorCategory.HasEnrichedHom