Documentation

Mathlib.CategoryTheory.Monoidal.Rigid.Braided

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

source
def CategoryTheory.BraidedCategory.exactPairing_swap {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (Y : C) [CategoryTheory.ExactPairing X Y] :
CategoryTheory.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.
source
def CategoryTheory.BraidedCategory.hasLeftDualOfHasRightDual {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X : C} [CategoryTheory.HasRightDual X] :
CategoryTheory.HasLeftDual X

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

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

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

Equations
source
instance CategoryTheory.BraidedCategory.leftRigidCategoryOfRightRigidCategory {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.RightRigidCategory C] :
CategoryTheory.LeftRigidCategory C
Equations
  • CategoryTheory.BraidedCategory.leftRigidCategoryOfRightRigidCategory = CategoryTheory.LeftRigidCategory.mk
source
instance CategoryTheory.BraidedCategory.rightRigidCategoryOfLeftRigidCategory {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.LeftRigidCategory C] :
CategoryTheory.RightRigidCategory C
Equations
  • CategoryTheory.BraidedCategory.rightRigidCategoryOfLeftRigidCategory = CategoryTheory.RightRigidCategory.mk
source
instance CategoryTheory.BraidedCategory.rigidCategoryOfRightRigidCategory {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.RightRigidCategory C] :
CategoryTheory.RigidCategory C

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

Equations
  • CategoryTheory.BraidedCategory.rigidCategoryOfRightRigidCategory = CategoryTheory.RigidCategory.mk
source
instance CategoryTheory.BraidedCategory.rigidCategoryOfLeftRigidCategory {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.LeftRigidCategory C] :
CategoryTheory.RigidCategory C

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

Equations
  • CategoryTheory.BraidedCategory.rigidCategoryOfLeftRigidCategory = CategoryTheory.RigidCategory.mk