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

source
@[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 : CategoryTheory.Functor D C) (Y : CategoryTheory.Functor D C) (X : D) :
((CategoryTheory.Functor.closedIhom F).toPrefunctor.obj Y).toPrefunctor.obj X = (CategoryTheory.ihom (F.toPrefunctor.obj X)).toPrefunctor.obj (Y.toPrefunctor.obj X)
source
@[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), ((CategoryTheory.Functor.closedIhom F).toPrefunctor.map g).app X_1 = (CategoryTheory.ihom (F.toPrefunctor.obj X_1)).toPrefunctor.map (g.app X_1)
source
@[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 : CategoryTheory.Functor D C) (Y : CategoryTheory.Functor D C) :
∀ {X Y_1 : D} (f : X ⟶ Y_1), ((CategoryTheory.Functor.closedIhom F).toPrefunctor.obj Y).toPrefunctor.map f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre (CategoryTheory.inv (F.toPrefunctor.map f))).app (Y.toPrefunctor.obj X)) ((CategoryTheory.ihom (F.toPrefunctor.obj Y_1)).toPrefunctor.map (Y.toPrefunctor.map f))
source
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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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 : CategoryTheory.Functor D C) (G : CategoryTheory.Functor D C) (X : D) :
    ((CategoryTheory.Functor.closedUnit F).app G).app X = (CategoryTheory.ihom.coev (F.toPrefunctor.obj X)).app (G.toPrefunctor.obj X)
    source
    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.Functor.comp (CategoryTheory.MonoidalCategory.tensorLeft F) (CategoryTheory.Functor.closedIhom F)

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[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 : CategoryTheory.Functor D C) (G : CategoryTheory.Functor D C) (X : D) :
      ((CategoryTheory.Functor.closedCounit F).app G).app X = (CategoryTheory.ihom.ev (F.toPrefunctor.obj X)).app (G.toPrefunctor.obj X)
      source
      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) :
      CategoryTheory.Functor.comp (CategoryTheory.Functor.closedIhom F) (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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        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
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem CategoryTheory.Functor.monoidalClosed_closed_isAdj_adj_homEquiv_symm_apply_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] (X : CategoryTheory.Functor D C) (X : CategoryTheory.Functor D C) (Y : CategoryTheory.Functor D C) (g : X✝ ⟶ (CategoryTheory.Functor.closedIhom X✝¹).toPrefunctor.obj Y) (X : D) :
        ((CategoryTheory.IsLeftAdjoint.adj.homEquiv X✝ Y).symm g).app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (X✝¹.toPrefunctor.obj X)) (g.app X)) ((CategoryTheory.ihom.ev (X✝¹.toPrefunctor.obj X)).app (Y.toPrefunctor.obj X))
        source
        @[simp]
        theorem CategoryTheory.Functor.monoidalClosed_closed_isAdj_adj_homEquiv_apply_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] (X : CategoryTheory.Functor D C) (X : CategoryTheory.Functor D C) (Y : CategoryTheory.Functor D C) (f : (CategoryTheory.MonoidalCategory.tensorLeft X✝¹).toPrefunctor.obj X✝ ⟶ Y) (X : D) :
        ((CategoryTheory.IsLeftAdjoint.adj.homEquiv X✝ Y) f).app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev (X✝¹.toPrefunctor.obj X)).app (X✝.toPrefunctor.obj X)) ((CategoryTheory.ihom (X✝¹.toPrefunctor.obj X)).toPrefunctor.map (f.app X))
        source
        @[simp]
        theorem CategoryTheory.Functor.monoidalClosed_closed_isAdj_adj_unit_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] (X : CategoryTheory.Functor D C) (G : CategoryTheory.Functor D C) (X : D) :
        (CategoryTheory.IsLeftAdjoint.adj.unit.app G).app X = (CategoryTheory.ihom.coev (X✝.toPrefunctor.obj X)).app (G.toPrefunctor.obj X)
        source
        @[simp]
        theorem CategoryTheory.Functor.monoidalClosed_closed_isAdj_right_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] (X : CategoryTheory.Functor D C) :
        ∀ {X_1 Y : CategoryTheory.Functor D C} (g : X_1 ⟶ Y) (X_2 : D), ((CategoryTheory.IsLeftAdjoint.right (CategoryTheory.MonoidalCategory.tensorLeft X)).toPrefunctor.map g).app X_2 = (CategoryTheory.ihom (X.toPrefunctor.obj X_2)).toPrefunctor.map (g.app X_2)
        source
        @[simp]
        theorem CategoryTheory.Functor.monoidalClosed_closed_isAdj_adj_counit_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] (X : CategoryTheory.Functor D C) (G : CategoryTheory.Functor D C) (X : D) :
        (CategoryTheory.IsLeftAdjoint.adj.counit.app G).app X = (CategoryTheory.ihom.ev (X✝.toPrefunctor.obj X)).app (G.toPrefunctor.obj X)
        source
        @[simp]
        theorem CategoryTheory.Functor.monoidalClosed_closed_isAdj_right_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] (X : CategoryTheory.Functor D C) (Y : CategoryTheory.Functor D C) :
        ∀ {X_1 Y_1 : D} (f : X_1 ⟶ Y_1), ((CategoryTheory.IsLeftAdjoint.right (CategoryTheory.MonoidalCategory.tensorLeft X)).toPrefunctor.obj Y).toPrefunctor.map f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre (CategoryTheory.inv (X.toPrefunctor.map f))).app (Y.toPrefunctor.obj X_1)) ((CategoryTheory.ihom (X.toPrefunctor.obj Y_1)).toPrefunctor.map (Y.toPrefunctor.map f))
        source
        @[simp]
        theorem CategoryTheory.Functor.monoidalClosed_closed_isAdj_right_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] (X : CategoryTheory.Functor D C) (Y : CategoryTheory.Functor D C) (X : D) :
        ((CategoryTheory.IsLeftAdjoint.right (CategoryTheory.MonoidalCategory.tensorLeft X✝)).toPrefunctor.obj Y).toPrefunctor.obj X = (CategoryTheory.ihom (X✝.toPrefunctor.obj X)).toPrefunctor.obj (Y.toPrefunctor.obj X)
        source
        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 }
        source
        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 : CategoryTheory.Functor D C} {H : CategoryTheory.Functor D C} (f : G ⟶ H) :
        (CategoryTheory.ihom F).toPrefunctor.map f = (CategoryTheory.Functor.closedIhom F).toPrefunctor.map f
        source
        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 : CategoryTheory.Functor D C) (G : CategoryTheory.Functor D C) :
        (CategoryTheory.ihom.ev F).app G = (CategoryTheory.Functor.closedCounit F).app G
        source
        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 : CategoryTheory.Functor D C) (G : CategoryTheory.Functor D C) :
        (CategoryTheory.ihom.coev F).app G = (CategoryTheory.Functor.closedUnit F).app G