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} {C : Type u_1} [Groupoid D] [Category.{v_1, u_1} C] [MonoidalCategory C] [MonoidalClosed C] (F : Functor D C) : Functor (Functor D C) (Functor D C)

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.closedUnit {D : Type u} {C : Type u_1} [Groupoid D] [Category.{v_1, u_1} C] [MonoidalCategory C] [MonoidalClosed C] (F : Functor D C) : Functor.id (Functor D C) ⟶ (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} {C : Type u_1} [Groupoid D] [Category.{v_1, u_1} C] [MonoidalCategory C] [MonoidalClosed C] (F G : Functor D C) (X : D) : (F.closedUnit.app G).app X = (ihom.coev (F.obj X)).app (G.obj X)

def CategoryTheory.Functor.closedCounit {D : Type u} {C : Type u_1} [Groupoid D] [Category.{v_1, u_1} C] [MonoidalCategory C] [MonoidalClosed C] (F : Functor D C) : F.closedIhom.comp (MonoidalCategory.tensorLeft F) ⟶ Functor.id (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} {C : Type u_1} [Groupoid D] [Category.{v_1, u_1} C] [MonoidalCategory C] [MonoidalClosed C] (F G : Functor D C) (X : D) : (F.closedCounit.app G).app X = (ihom.ev (F.obj X)).app (G.obj X)

@[instance_reducible]

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

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

If C is a monoidal closed category and D is a 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} {C : Type u_1} [Groupoid D] [Category.{v_1, u_1} C] [MonoidalCategory C] [MonoidalClosed C] (X : Functor D C) : Closed.adj = { unit := X.closedUnit, counit := X.closedCounit, left_triangle_components := ⋯, right_triangle_components := ⋯ }

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

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

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