# Documentation

Mathlib.CategoryTheory.Closed.FunctorCategory

# Functors from a groupoid into a monoidal closed category form a monoidal closed category. #

(Using the pointwise monoidal structure on the functor category.)

@[simp]
theorem CategoryTheory.Functor.closedIhom_obj_obj {D : Type u_1} {C : Type u_2} [] (F : ) (Y : ) (X : D) :
(().obj Y).obj X = (CategoryTheory.ihom (F.obj X)).obj (Y.obj X)
@[simp]
theorem CategoryTheory.Functor.closedIhom_map_app {D : Type u_1} {C : Type u_2} [] (F : ) :
∀ {X Y : } (g : X Y) (X_1 : D), (().map g).app X_1 = (CategoryTheory.ihom (F.obj X_1)).map (g.app X_1)
@[simp]
theorem CategoryTheory.Functor.closedIhom_obj_map {D : Type u_1} {C : Type u_2} [] (F : ) (Y : ) :
∀ {X Y : D} (f : X Y), (().obj Y).map f = CategoryTheory.CategoryStruct.comp (().app (Y.obj X)) ((CategoryTheory.ihom (F.obj Y)).map (Y.map f))
def CategoryTheory.Functor.closedIhom {D : Type u_1} {C : Type u_2} [] (F : ) :

Auxiliary definition for CategoryTheory.Functor.closed. The internal hom functor F ⟶[C] -

Instances For
@[simp]
theorem CategoryTheory.Functor.closedUnit_app_app {D : Type u_1} {C : Type u_2} [] (F : ) (G : ) (X : D) :
(().app G).app X = (CategoryTheory.ihom.coev (F.obj X)).app (G.obj X)

Auxiliary definition for CategoryTheory.Functor.closed. The unit for the adjunction (tensorLeft F) ⊣ (ihom F).

Instances For
@[simp]
theorem CategoryTheory.Functor.closedCounit_app_app {D : Type u_1} {C : Type u_2} [] (F : ) (G : ) (X : D) :
(().app G).app X = (CategoryTheory.ihom.ev (F.obj X)).app (G.obj X)

Auxiliary definition for CategoryTheory.Functor.closed. The counit for the adjunction (tensorLeft F) ⊣ (ihom F).

Instances For
instance CategoryTheory.Functor.closed {D : Type u_1} {C : Type u_2} [] (F : ) :

If C is a monoidal closed category and D is a groupoid, then every functor F : D ⥤ C is closed in the functor category F : D ⥤ C with the pointwise monoidal structure.

@[simp]
theorem CategoryTheory.Functor.monoidalClosed_closed_isAdj_adj_homEquiv_symm_apply_app {D : Type u_1} {C : Type u_2} [] (X : ) (X : ) (Y : ) (g : X ().obj Y) (X : D) :
((CategoryTheory.Adjunction.homEquiv CategoryTheory.IsLeftAdjoint.adj X Y).symm g).app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (X.obj X)) (g.app X)) ((CategoryTheory.ihom.ev (X.obj X)).app (Y.obj X))
@[simp]
theorem CategoryTheory.Functor.monoidalClosed_closed_isAdj_adj_homEquiv_apply_app {D : Type u_1} {C : Type u_2} [] (X : ) (X : ) (Y : ) (f : Y) (X : D) :
(↑(CategoryTheory.Adjunction.homEquiv CategoryTheory.IsLeftAdjoint.adj X Y) f).app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev (X.obj X)).app (X.obj X)) ((CategoryTheory.ihom (X.obj X)).map (f.app X))
@[simp]
theorem CategoryTheory.Functor.monoidalClosed_closed_isAdj_adj_unit_app_app {D : Type u_1} {C : Type u_2} [] (X : ) (G : ) (X : D) :
@[simp]
theorem CategoryTheory.Functor.monoidalClosed_closed_isAdj_right_map_app {D : Type u_1} {C : Type u_2} [] (X : ) :
∀ {X Y : } (g : X Y) (X_1 : D), ().app X_1 = (CategoryTheory.ihom (X.obj X_1)).map (g.app X_1)
@[simp]
theorem CategoryTheory.Functor.monoidalClosed_closed_isAdj_adj_counit_app_app {D : Type u_1} {C : Type u_2} [] (X : ) (G : ) (X : D) :
@[simp]
theorem CategoryTheory.Functor.monoidalClosed_closed_isAdj_right_obj_map {D : Type u_1} {C : Type u_2} [] (X : ) (Y : ) :
∀ {X Y : D} (f : X Y), ().map f = CategoryTheory.CategoryStruct.comp (().app (Y.obj X)) ((CategoryTheory.ihom (X.obj Y)).map (Y.map f))
@[simp]
theorem CategoryTheory.Functor.monoidalClosed_closed_isAdj_right_obj_obj {D : Type u_1} {C : Type u_2} [] (X : ) (Y : ) (X : D) :
().obj X = (CategoryTheory.ihom (X.obj X)).obj (Y.obj X)
instance CategoryTheory.Functor.monoidalClosed {D : Type u_1} {C : Type u_2} [] :

If C is a monoidal closed category and D is groupoid, then the functor category D ⥤ C, with the pointwise monoidal structure, is monoidal closed.

theorem CategoryTheory.Functor.ihom_map {D : Type u_1} {C : Type u_2} [] (F : ) {G : } {H : } (f : G H) :
().map f = ().map f
theorem CategoryTheory.Functor.ihom_ev_app {D : Type u_1} {C : Type u_2} [] (F : ) (G : ) :
().app G = ().app G
theorem CategoryTheory.Functor.ihom_coev_app {D : Type u_1} {C : Type u_2} [] (F : ) (G : ) :
().app G = ().app G