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₂) [CategoryTheory.Category.{v₂, u₂} I] (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ((CategoryTheory.whiskeringLeft (CategoryTheory.Discrete I) I C).obj (CategoryTheory.Functor.incl I)).ReflectsIsomorphisms

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.Functor.instPreservesLimitOfIsCoreflexivePairDiscreteObjWhiskeringLeftIncl I C = { out := inferInstance }

instance CategoryTheory.Functor.instComonadicLeftAdjointDiscreteObjWhiskeringLeftIncl (I : Type u₂) [CategoryTheory.Category.{v₂, u₂} I] (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [∀ (F : CategoryTheory.Functor (CategoryTheory.Discrete I) C), (CategoryTheory.Discrete.functor id).HasRightKanExtension F] [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair C] : CategoryTheory.ComonadicLeftAdjoint ((CategoryTheory.whiskeringLeft (CategoryTheory.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₂) [CategoryTheory.Category.{v₂, u₂} I] (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (F : CategoryTheory.Functor I C) : (CategoryTheory.MonoidalCategory.tensorLeft ((CategoryTheory.Functor.incl I).comp F)).IsLeftAdjoint

Equations

• ⋯ = ⋯

def CategoryTheory.Functor.functorCategoryClosed (I : Type u₂) [CategoryTheory.Category.{v₂, u₂} I] (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] [∀ (F : CategoryTheory.Functor (CategoryTheory.Discrete I) C), (CategoryTheory.Discrete.functor id).HasRightKanExtension F] [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair C] (F : CategoryTheory.Functor I C) : CategoryTheory.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₂) [CategoryTheory.Category.{v₂, u₂} I] (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] [∀ (F : CategoryTheory.Functor (CategoryTheory.Discrete I) C), (CategoryTheory.Discrete.functor id).HasRightKanExtension F] [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair C] : CategoryTheory.MonoidalClosed (CategoryTheory.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 }