Functors into a complete monoidal closed category form a monoidal closed category.

TODO (in progress by Joël Riou): make a more explicit construction of the internal hom in functor categories.

instance CategoryTheory.Functor.instReflectsIsomorphismsDiscreteObjWhiskeringLeftIncl (I : Type u₂) [Category.{v₂, u₂} I] (C : Type u₁) [Category.{v₁, u₁} C] : ((whiskeringLeft (Discrete I) I C).obj (CategoryTheory.Functor.incl✝ I)).ReflectsIsomorphisms

instance CategoryTheory.Functor.instPreservesLimitOfIsCoreflexivePairDiscreteObjWhiskeringLeftIncl (I : Type u₂) [Category.{v₂, u₂} I] (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasLimitsOfShape Limits.WalkingParallelPair C] : Comonad.PreservesLimitOfIsCoreflexivePair ((whiskeringLeft (Discrete I) I C).obj (CategoryTheory.Functor.incl✝ I))

instance CategoryTheory.Functor.instComonadicLeftAdjointDiscreteObjWhiskeringLeftIncl (I : Type u₂) [Category.{v₂, u₂} I] (C : Type u₁) [Category.{v₁, u₁} C] [∀ (F : Functor (Discrete I) C), (Discrete.functor id).HasRightKanExtension F] [Limits.HasLimitsOfShape Limits.WalkingParallelPair C] : ComonadicLeftAdjoint ((whiskeringLeft (Discrete I) I C).obj (CategoryTheory.Functor.incl✝ I))

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Functor.instIsLeftAdjointDiscreteTensorLeftCompIncl (I : Type u₂) [Category.{v₂, u₂} I] (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [MonoidalClosed C] (F : Functor I C) : (MonoidalCategory.tensorLeft ((CategoryTheory.Functor.incl✝ I).comp F)).IsLeftAdjoint

def CategoryTheory.Functor.functorCategoryClosed (I : Type u₂) [Category.{v₂, u₂} I] (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [MonoidalClosed C] [∀ (F : Functor (Discrete I) C), (Discrete.functor id).HasRightKanExtension F] [Limits.HasLimitsOfShape Limits.WalkingParallelPair C] (F : Functor I C) : Closed F

Auxiliary definition for functorCategoryMonoidalClosed

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Functor.functorCategoryMonoidalClosed (I : Type u₂) [Category.{v₂, u₂} I] (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [MonoidalClosed C] [∀ (F : Functor (Discrete I) C), (Discrete.functor id).HasRightKanExtension F] [Limits.HasLimitsOfShape Limits.WalkingParallelPair C] : MonoidalClosed (Functor I C)

Assuming the existence of certain limits, functors into a monoidal closed category form a monoidal closed category.

Note: this is defined completely abstractly, and does not have any good definitional properties. See the TODO in the module docstring.

Equations

• CategoryTheory.Functor.functorCategoryMonoidalClosed I C = { closed := fun (F : CategoryTheory.Functor I C) => CategoryTheory.Functor.functorCategoryClosed I C F }