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
  • One or more equations did not get rendered due to their size.
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