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.
Instances For
    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
    Instances For
      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
      Instances For
        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