Functors from a groupoid into a right/left rigid category form a right/left rigid 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.)
@[protected, instance]
noncomputable
def
category_theory.monoidal.functor_has_right_dual
{C : Type u_1}
{D : Type u_2}
[category_theory.groupoid C]
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.right_rigid_category D]
(F : C ⥤ D) :
Equations
- category_theory.monoidal.functor_has_right_dual F = category_theory.has_right_dual.mk {obj := λ (X : C), (F.obj X)ᘁ, map := λ (X Y : C) (f : X ⟶ Y), (F.map (category_theory.inv f))ᘁ, map_id' := _, map_comp' := _}
@[protected, instance]
noncomputable
def
category_theory.monoidal.right_rigid_functor_category
{C : Type u_1}
{D : Type u_2}
[category_theory.groupoid C]
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.right_rigid_category D] :
@[protected, instance]
noncomputable
def
category_theory.monoidal.functor_has_left_dual
{C : Type u_1}
{D : Type u_2}
[category_theory.groupoid C]
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.left_rigid_category D]
(F : C ⥤ D) :
Equations
- category_theory.monoidal.functor_has_left_dual F = category_theory.has_left_dual.mk {obj := λ (X : C), ᘁ(F.obj X), map := λ (X Y : C) (f : X ⟶ Y), ᘁ(F.map (category_theory.inv f)), map_id' := _, map_comp' := _}
@[protected, instance]
noncomputable
def
category_theory.monoidal.left_rigid_functor_category
{C : Type u_1}
{D : Type u_2}
[category_theory.groupoid C]
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.left_rigid_category D] :
@[protected, instance]
noncomputable
def
category_theory.monoidal.rigid_functor_category
{C : Type u_1}
{D : Type u_2}
[category_theory.groupoid C]
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.rigid_category D] :