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_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_1 : D), (F.closedIhom.map g).app X_1 = (CategoryTheory.ihom (F.obj X_1)).map (g.app X_1)

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

Equations
Instances For

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

    Equations
    Instances For

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

      Equations
      Instances For

        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 := } }
        @[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 := }

        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 }