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.)

source
def CategoryTheory.Functor.closedIhom {D : Type u_1} {C : Type u_2} [Groupoid D] [Category.{u_4, u_2} 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
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Functor.closedIhom_obj_map {D : Type u_1} {C : Type u_2} [Groupoid D] [Category.{u_4, u_2} 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))
      source
      @[simp]
      theorem CategoryTheory.Functor.closedIhom_map_app {D : Type u_1} {C : Type u_2} [Groupoid D] [Category.{u_4, u_2} 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)
      source
      @[simp]
      theorem CategoryTheory.Functor.closedIhom_obj_obj {D : Type u_1} {C : Type u_2} [Groupoid D] [Category.{u_4, u_2} 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)
      source
      def CategoryTheory.Functor.closedUnit {D : Type u_1} {C : Type u_2} [Groupoid D] [Category.{u_4, u_2} 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
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Functor.closedUnit_app_app {D : Type u_1} {C : Type u_2} [Groupoid D] [Category.{u_4, u_2} 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)
          source
          def CategoryTheory.Functor.closedCounit {D : Type u_1} {C : Type u_2} [Groupoid D] [Category.{u_4, u_2} 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
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Functor.closedCounit_app_app {D : Type u_1} {C : Type u_2} [Groupoid D] [Category.{u_4, u_2} 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)
              source
              instance CategoryTheory.Functor.closed {D : Type u_1} {C : Type u_2} [Groupoid D] [Category.{u_4, u_2} 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
                source
                instance CategoryTheory.Functor.monoidalClosed {D : Type u_1} {C : Type u_2} [Groupoid D] [Category.{u_4, u_2} C] [MonoidalCategory C] [MonoidalClosed C] :
                MonoidalClosed (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
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.monoidalClosed_closed_adj {D : Type u_1} {C : Type u_2} [Groupoid D] [Category.{u_4, u_2} C] [MonoidalCategory C] [MonoidalClosed C] (X : Functor D C) :
                  Closed.adj = { unit := X.closedUnit, counit := X.closedCounit, left_triangle_components := ⋯, right_triangle_components := ⋯ }
                  source
                  theorem CategoryTheory.Functor.ihom_map {D : Type u_1} {C : Type u_2} [Groupoid D] [Category.{u_4, u_2} 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
                  source
                  theorem CategoryTheory.Functor.ihom_ev_app {D : Type u_1} {C : Type u_2} [Groupoid D] [Category.{u_4, u_2} C] [MonoidalCategory C] [MonoidalClosed C] (F G : Functor D C) :
                  (ihom.ev F).app G = F.closedCounit.app G
                  source
                  theorem CategoryTheory.Functor.ihom_coev_app {D : Type u_1} {C : Type u_2} [Groupoid D] [Category.{u_4, u_2} C] [MonoidalCategory C] [MonoidalClosed C] (F G : Functor D C) :
                  (ihom.coev F).app G = F.closedUnit.app G