Documentation

Mathlib.CategoryTheory.Closed.FunctorCategory.Groupoid

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

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

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