Dual Functors for Rigid Categories

This file defines the left and right dual functors from a rigid monoidal category to (Cᵒᵖ)ᴹᵒᵖ (the monoidal opposite of the opposite category).

Main definitions

• leftDualFunctor C: For a left rigid category, the functor C ⥤ (Cᵒᵖ)ᴹᵒᵖ sending X to ᘁX and f to ᘁf.
• rightDualFunctor C: For a right rigid category, the functor C ⥤ (Cᵒᵖ)ᴹᵒᵖ sending X to Xᘁ and f to fᘁ.

Future work

• Show that in a RigidCategory, these functors are monoidal equivalences.

def CategoryTheory.leftDualFunctor (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [LeftRigidCategory C] : Functor C Cᵒᵖᴹᵒᵖ

The left dual functor from C to (Cᵒᵖ)ᴹᵒᵖ.

Equations

• CategoryTheory.leftDualFunctor C = { obj := fun (X : C) => { unmop := Opposite.op ᘁX }, map := fun {X Y : C} (f : X ⟶ Y) => (ᘁf).op.mop, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.leftDualFunctor_map (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [LeftRigidCategory C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (leftDualFunctor C).map f = (ᘁf).op.mop

@[simp]

theorem CategoryTheory.leftDualFunctor_obj (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [LeftRigidCategory C] (X : C) : (leftDualFunctor C).obj X = { unmop := Opposite.op ᘁX }

def CategoryTheory.rightDualFunctor (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [RightRigidCategory C] : Functor C Cᵒᵖᴹᵒᵖ

The right dual functor from C to (Cᵒᵖ)ᴹᵒᵖ.

Equations

• CategoryTheory.rightDualFunctor C = { obj := fun (X : C) => { unmop := Opposite.op Xᘁ }, map := fun {X Y : C} (f : X ⟶ Y) => fᘁ.op.mop, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.rightDualFunctor_map (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [RightRigidCategory C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (rightDualFunctor C).map f = fᘁ.op.mop

@[simp]

theorem CategoryTheory.rightDualFunctor_obj (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [RightRigidCategory C] (X : C) : (rightDualFunctor C).obj X = { unmop := Opposite.op Xᘁ }