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} [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
    Instances For
      source
      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
        Instances For
          source
          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
            Instances For
              source
              instance CategoryTheory.BraidedCategory.leftRigidCategoryOfRightRigidCategory {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] [BraidedCategory C] [RightRigidCategory C] :
              LeftRigidCategory C
              Equations
                source
                instance CategoryTheory.BraidedCategory.rightRigidCategoryOfLeftRigidCategory {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] [BraidedCategory C] [LeftRigidCategory C] :
                RightRigidCategory C
                Equations
                  source
                  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
                    source
                    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