Deriving RigidCategory instance for braided and left/right rigid categories.

def CategoryTheory.BraidedCategory.exactPairing_swap {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] [BraidedCategory C] (X Y : C) [ExactPairing X Y] : ExactPairing Y X

If X and Y forms an exact pairing in a braided category, then so does Y and X by composing the coevaluation and evaluation morphisms with associators.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.BraidedCategory.hasLeftDualOfHasRightDual {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] [BraidedCategory C] {X : C} [HasRightDual X] : HasLeftDual X

If X has a right dual in a braided category, then it has a left dual.

Equations

• CategoryTheory.BraidedCategory.hasLeftDualOfHasRightDual = { leftDual := Xᘁ, exact := CategoryTheory.BraidedCategory.exactPairing_swap X Xᘁ }

def CategoryTheory.BraidedCategory.hasRightDualOfHasLeftDual {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] [BraidedCategory C] {X : C} [HasLeftDual X] : HasRightDual X

If X has a left dual in a braided category, then it has a right dual.

Equations

• CategoryTheory.BraidedCategory.hasRightDualOfHasLeftDual = { rightDual := ᘁX, exact := CategoryTheory.BraidedCategory.exactPairing_swap (ᘁX) X }

instance CategoryTheory.BraidedCategory.leftRigidCategoryOfRightRigidCategory {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] [BraidedCategory C] [RightRigidCategory C] : LeftRigidCategory C

Equations

• CategoryTheory.BraidedCategory.leftRigidCategoryOfRightRigidCategory = { leftDual := fun (X : C) => CategoryTheory.BraidedCategory.hasLeftDualOfHasRightDual }

instance CategoryTheory.BraidedCategory.rightRigidCategoryOfLeftRigidCategory {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] [BraidedCategory C] [LeftRigidCategory C] : RightRigidCategory C

Equations

• CategoryTheory.BraidedCategory.rightRigidCategoryOfLeftRigidCategory = { rightDual := fun (X : C) => CategoryTheory.BraidedCategory.hasRightDualOfHasLeftDual }

instance CategoryTheory.BraidedCategory.rigidCategoryOfRightRigidCategory {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] [BraidedCategory C] [RightRigidCategory C] : RigidCategory C

If C is a braided and right rigid category, then it is a rigid category.

Equations

• CategoryTheory.BraidedCategory.rigidCategoryOfRightRigidCategory = { rightDual := inferInstance, leftDual := inferInstance }

instance CategoryTheory.BraidedCategory.rigidCategoryOfLeftRigidCategory {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] [BraidedCategory C] [LeftRigidCategory C] : RigidCategory C

If C is a braided and left rigid category, then it is a rigid category.

Equations

• CategoryTheory.BraidedCategory.rigidCategoryOfLeftRigidCategory = { rightDual := inferInstance, leftDual := inferInstance }