Documentation

Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

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

source
instance CategoryTheory.Monoidal.functorHasRightDual {C : Type u_1} {D : Type u_2} [Groupoid C] [Category.{u_4, u_2} D] [MonoidalCategory D] [RightRigidCategory D] (F : Functor C D) :
HasRightDual F
Equations
  • One or more equations did not get rendered due to their size.
source
instance CategoryTheory.Monoidal.rightRigidFunctorCategory {C : Type u_1} {D : Type u_2} [Groupoid C] [Category.{u_4, u_2} D] [MonoidalCategory D] [RightRigidCategory D] :
RightRigidCategory (Functor C D)
Equations
source
instance CategoryTheory.Monoidal.functorHasLeftDual {C : Type u_1} {D : Type u_2} [Groupoid C] [Category.{u_4, u_2} D] [MonoidalCategory D] [LeftRigidCategory D] (F : Functor C D) :
HasLeftDual F
Equations
  • One or more equations did not get rendered due to their size.
source
instance CategoryTheory.Monoidal.leftRigidFunctorCategory {C : Type u_1} {D : Type u_2} [Groupoid C] [Category.{u_4, u_2} D] [MonoidalCategory D] [LeftRigidCategory D] :
LeftRigidCategory (Functor C D)
Equations
source
instance CategoryTheory.Monoidal.rigidFunctorCategory {C : Type u_1} {D : Type u_2} [Groupoid C] [Category.{u_4, u_2} D] [MonoidalCategory D] [RigidCategory D] :
RigidCategory (Functor C D)
Equations