Functors from a groupoid into a right/left rigid category form a right/left rigid category. #
(Using the pointwise monoidal structure on the functor category.)
@[instance_reducible]
noncomputable instance CategoryTheory.Monoidal.functorHasRightDual {C : Type u_1} {D : Type u_2} [Groupoid C] [Category.{v_1, u_2} D] [MonoidalCategory D] [RightRigidCategory D] (F : Functor C D) :
Equations
- One or more equations did not get rendered due to their size.
@[instance_reducible]
noncomputable instance CategoryTheory.Monoidal.rightRigidFunctorCategory {C : Type u_1} {D : Type u_2} [Groupoid C] [Category.{v_1, u_2} D] [MonoidalCategory D] [RightRigidCategory D] :
RightRigidCategory (Functor C D)
Equations
- CategoryTheory.Monoidal.rightRigidFunctorCategory = { rightDual := fun (X : CategoryTheory.Functor C D) => CategoryTheory.Monoidal.functorHasRightDual X }
@[instance_reducible]
noncomputable instance CategoryTheory.Monoidal.functorHasLeftDual {C : Type u_1} {D : Type u_2} [Groupoid C] [Category.{v_1, u_2} D] [MonoidalCategory D] [LeftRigidCategory D] (F : Functor C D) :
Equations
- One or more equations did not get rendered due to their size.
@[instance_reducible]
noncomputable instance CategoryTheory.Monoidal.leftRigidFunctorCategory {C : Type u_1} {D : Type u_2} [Groupoid C] [Category.{v_1, u_2} D] [MonoidalCategory D] [LeftRigidCategory D] :
LeftRigidCategory (Functor C D)
Equations
- CategoryTheory.Monoidal.leftRigidFunctorCategory = { leftDual := fun (X : CategoryTheory.Functor C D) => CategoryTheory.Monoidal.functorHasLeftDual X }
@[instance_reducible]
noncomputable instance CategoryTheory.Monoidal.rigidFunctorCategory {C : Type u_1} {D : Type u_2} [Groupoid C] [Category.{v_1, u_2} D] [MonoidalCategory D] [RigidCategory D] :
RigidCategory (Functor C D)
Equations
- One or more equations did not get rendered due to their size.