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

@[implicit_reducible]

def CategoryTheory.BraidedCategory.exactPairing_swap {C : Type u_1} [Category.{v_1, 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.

@[implicit_reducible]

def CategoryTheory.BraidedCategory.hasLeftDualOfHasRightDual {C : Type u_1} [Category.{v_1, 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ᘁ }

@[implicit_reducible]

def CategoryTheory.BraidedCategory.hasRightDualOfHasLeftDual {C : Type u_1} [Category.{v_1, 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 }

@[implicit_reducible]

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

If a braided category is right-rigid, then it is left-rigid. Not registered as an instance as this is not canonical enough.

Equations

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

@[implicit_reducible]

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

If a braided category is left-rigid, then it is right-rigid. Not registered as an instance as this is not canonical enough.

Equations

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

@[implicit_reducible]

def CategoryTheory.BraidedCategory.rigidCategoryOfRightRigidCategory {C : Type u_1} [Category.{v_1, 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. Not registered as an instance as this is not canonical enough.

Equations

• CategoryTheory.BraidedCategory.rigidCategoryOfRightRigidCategory = { rightDual := inferInstance, leftDual := fun (X : C) => CategoryTheory.BraidedCategory.hasLeftDualOfHasRightDual }

@[implicit_reducible]

def CategoryTheory.BraidedCategory.rigidCategoryOfLeftRigidCategory {C : Type u_1} [Category.{v_1, 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. Not registered as an instance as this is not canonical enough.

Equations

• CategoryTheory.BraidedCategory.rigidCategoryOfLeftRigidCategory = { rightDual := fun (X : C) => CategoryTheory.BraidedCategory.hasRightDualOfHasLeftDual, leftDual := inferInstance }