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

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

def CategoryTheory.Functor.closedIhom {D : Type u_1} {C : Type u_2} [CategoryTheory.Groupoid D] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (F : CategoryTheory.Functor D C) : CategoryTheory.Functor (CategoryTheory.Functor D C) (CategoryTheory.Functor D C)

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

Equations

• F.closedIhom = ((CategoryTheory.whiskeringRight₂ D Cᵒᵖ C C).obj CategoryTheory.MonoidalClosed.internalHom).obj ((CategoryTheory.Groupoid.invFunctor D).comp F.op)

@[simp]

theorem CategoryTheory.Functor.closedIhom_obj_map {D : Type u_1} {C : Type u_2} [CategoryTheory.Groupoid D] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (F Y : CategoryTheory.Functor D C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (F.closedIhom.obj Y).map f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre (CategoryTheory.inv (F.map f))).app (Y.obj X✝)) ((CategoryTheory.ihom (F.obj Y✝)).map (Y.map f))

@[simp]

theorem CategoryTheory.Functor.closedIhom_map_app {D : Type u_1} {C : Type u_2} [CategoryTheory.Groupoid D] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (F : CategoryTheory.Functor D C) {X✝ Y✝ : CategoryTheory.Functor D C} (g : X✝ ⟶ Y✝) (X : D) : (F.closedIhom.map g).app X = (CategoryTheory.ihom (F.obj X)).map (g.app X)

@[simp]

theorem CategoryTheory.Functor.closedIhom_obj_obj {D : Type u_1} {C : Type u_2} [CategoryTheory.Groupoid D] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (F Y : CategoryTheory.Functor D C) (X : D) : (F.closedIhom.obj Y).obj X = (CategoryTheory.ihom (F.obj X)).obj (Y.obj X)

def CategoryTheory.Functor.closedUnit {D : Type u_1} {C : Type u_2} [CategoryTheory.Groupoid D] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (F : CategoryTheory.Functor D C) : CategoryTheory.Functor.id (CategoryTheory.Functor D C) ⟶ (CategoryTheory.MonoidalCategory.tensorLeft F).comp F.closedIhom

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

Equations

• F.closedUnit = { app := fun (G : CategoryTheory.Functor D C) => { app := fun (X : D) => (CategoryTheory.ihom.coev (F.obj X)).app (G.obj X), naturality := ⋯ }, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.closedUnit_app_app {D : Type u_1} {C : Type u_2} [CategoryTheory.Groupoid D] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (F G : CategoryTheory.Functor D C) (X : D) : (F.closedUnit.app G).app X = (CategoryTheory.ihom.coev (F.obj X)).app (G.obj X)

def CategoryTheory.Functor.closedCounit {D : Type u_1} {C : Type u_2} [CategoryTheory.Groupoid D] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (F : CategoryTheory.Functor D C) : F.closedIhom.comp (CategoryTheory.MonoidalCategory.tensorLeft F) ⟶ CategoryTheory.Functor.id (CategoryTheory.Functor D C)

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

Equations

• F.closedCounit = { app := fun (G : CategoryTheory.Functor D C) => { app := fun (X : D) => (CategoryTheory.ihom.ev (F.obj X)).app (G.obj X), naturality := ⋯ }, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.closedCounit_app_app {D : Type u_1} {C : Type u_2} [CategoryTheory.Groupoid D] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (F G : CategoryTheory.Functor D C) (X : D) : (F.closedCounit.app G).app X = (CategoryTheory.ihom.ev (F.obj X)).app (G.obj X)

instance CategoryTheory.Functor.closed {D : Type u_1} {C : Type u_2} [CategoryTheory.Groupoid D] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (F : CategoryTheory.Functor D C) : CategoryTheory.Closed 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.

Equations

• F.closed = { rightAdj := F.closedIhom, adj := { unit := F.closedUnit, counit := F.closedCounit, left_triangle_components := ⋯, right_triangle_components := ⋯ } }

instance CategoryTheory.Functor.monoidalClosed {D : Type u_1} {C : Type u_2} [CategoryTheory.Groupoid D] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] : CategoryTheory.MonoidalClosed (CategoryTheory.Functor D C)

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.

Equations

• CategoryTheory.Functor.monoidalClosed = { closed := inferInstance }

@[simp]

theorem CategoryTheory.Functor.monoidalClosed_closed_adj {D : Type u_1} {C : Type u_2} [CategoryTheory.Groupoid D] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Functor D C) : CategoryTheory.Closed.adj = { unit := X.closedUnit, counit := X.closedCounit, left_triangle_components := ⋯, right_triangle_components := ⋯ }

theorem CategoryTheory.Functor.ihom_map {D : Type u_1} {C : Type u_2} [CategoryTheory.Groupoid D] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (F : CategoryTheory.Functor D C) {G H : CategoryTheory.Functor D C} (f : G ⟶ H) : (CategoryTheory.ihom F).map f = F.closedIhom.map f

theorem CategoryTheory.Functor.ihom_ev_app {D : Type u_1} {C : Type u_2} [CategoryTheory.Groupoid D] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (F G : CategoryTheory.Functor D C) : (CategoryTheory.ihom.ev F).app G = F.closedCounit.app G

theorem CategoryTheory.Functor.ihom_coev_app {D : Type u_1} {C : Type u_2} [CategoryTheory.Groupoid D] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (F G : CategoryTheory.Functor D C) : (CategoryTheory.ihom.coev F).app G = F.closedUnit.app G