mathlib3 documentation

category_theory.closed.functor_category

Functors from a groupoid into a monoidal closed category form a monoidal closed category. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

(Using the pointwise monoidal structure on the functor category.)

source
noncomputable def category_theory.functor.closed_ihom {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (F : D ⥤ C) :
(D ⥤ C) ⥤ D ⥤ C

Auxiliary definition for category_theory.monoidal_closed.functor_closed. The internal hom functor F ⟶[C] -

Equations
source
@[simp]
theorem category_theory.functor.closed_ihom_obj_obj {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (F Y : D ⥤ C) (X : D) :
(F.closed_ihom.obj Y).obj X = (category_theory.ihom (F.obj X)).obj (Y.obj X)
source
@[simp]
theorem category_theory.functor.closed_ihom_obj_map {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (F Y : D ⥤ C) (_x _x_1 : D) (f : _x ⟶ _x_1) :
(F.closed_ihom.obj Y).map f = (category_theory.monoidal_closed.pre (category_theory.inv (F.map f))).app (Y.obj _x) ≫ (category_theory.ihom (F.obj _x_1)).map (Y.map f)
source
@[simp]
theorem category_theory.functor.closed_ihom_map_app {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (F Y Y' : D ⥤ C) (g : Y ⟶ Y') (X : D) :
(F.closed_ihom.map g).app X = (category_theory.ihom (F.obj X)).map (g.app X)
source
def category_theory.functor.closed_unit {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (F : D ⥤ C) :
𝟭 (D ⥤ C) ⟶ category_theory.monoidal_category.tensor_left F ⋙ F.closed_ihom

Auxiliary definition for category_theory.monoidal_closed.functor_closed. The unit for the adjunction (tensor_left F) ⊣ (ihom F).

Equations
source
@[simp]
theorem category_theory.functor.closed_unit_app_app {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (F G : D ⥤ C) (X : D) :
(F.closed_unit.app G).app X = (category_theory.ihom.coev (F.obj X)).app (G.obj X)
source
def category_theory.functor.closed_counit {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (F : D ⥤ C) :
F.closed_ihom ⋙ category_theory.monoidal_category.tensor_left F ⟶ 𝟭 (D ⥤ C)

Auxiliary definition for category_theory.monoidal_closed.functor_closed. The counit for the adjunction (tensor_left F) ⊣ (ihom F).

Equations
source
@[simp]
theorem category_theory.functor.closed_counit_app_app {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (F G : D ⥤ C) (X : D) :
(F.closed_counit.app G).app X = (category_theory.ihom.ev (F.obj X)).app (G.obj X)
source
@[simp]
theorem category_theory.functor.closed_is_adj_adj {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (F : D ⥤ C) :
category_theory.is_left_adjoint.adj = category_theory.adjunction.mk_of_unit_counit {unit := F.closed_unit, counit := F.closed_counit, left_triangle' := _, right_triangle' := _}
source
@[protected, instance]
noncomputable def category_theory.functor.closed {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (F : D ⥤ C) :
category_theory.closed F

If C is a monoidal closed category and D is groupoid, then every functor F : D ⥤ C is closed in the functor category F : D ⥤ C with the pointwise monoidal structure.

Equations
source
@[simp]
theorem category_theory.functor.closed_is_adj_right {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (F : D ⥤ C) :
category_theory.is_left_adjoint.right (category_theory.monoidal_category.tensor_left F) = F.closed_ihom
source
@[simp]
theorem category_theory.functor.monoidal_closed_closed' {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (X : D ⥤ C) :
category_theory.monoidal_closed.closed' X = X.closed
source
@[protected, instance]
noncomputable def category_theory.functor.monoidal_closed {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] :
category_theory.monoidal_closed (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
theorem category_theory.functor.ihom_map {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (F : D ⥤ C) {G H : D ⥤ C} (f : G ⟶ H) :
(category_theory.ihom F).map f = F.closed_ihom.map f
source
theorem category_theory.functor.ihom_ev_app {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (F G : D ⥤ C) :
(category_theory.ihom.ev F).app G = F.closed_counit.app G
source
theorem category_theory.functor.ihom_coev_app {C : Type u_1} {D : Type u_2} [category_theory.groupoid D] [category_theory.category C] [category_theory.monoidal_category C] [category_theory.monoidal_closed C] (F G : D ⥤ C) :
(category_theory.ihom.coev F).app G = F.closed_unit.app G