Goto Chapter: Top 1 2 3 4 5 6 7 8 9 10 11 Ind
 [Top of Book]  [Contents]   [Previous Chapter]   [Next Chapter] 

7 Tensor Product and Internal Hom
 7.1 Monoidal Categories

  7.1-1 TensorProductOnObjects

  7.1-2 AddTensorProductOnObjects

  7.1-3 TensorProductOnMorphisms

  7.1-4 TensorProductOnMorphismsWithGivenTensorProducts

  7.1-5 AddTensorProductOnMorphismsWithGivenTensorProducts

  7.1-6 AssociatorRightToLeft

  7.1-7 AssociatorRightToLeftWithGivenTensorProducts

  7.1-8 AddAssociatorRightToLeftWithGivenTensorProducts

  7.1-9 AssociatorLeftToRight

  7.1-10 AssociatorLeftToRightWithGivenTensorProducts

  7.1-11 AddAssociatorLeftToRightWithGivenTensorProducts

  7.1-12 TensorUnit

  7.1-13 AddTensorUnit

  7.1-14 LeftUnitor

  7.1-15 LeftUnitorWithGivenTensorProduct

  7.1-16 AddLeftUnitorWithGivenTensorProduct

  7.1-17 LeftUnitorInverse

  7.1-18 LeftUnitorInverseWithGivenTensorProduct

  7.1-19 AddLeftUnitorInverseWithGivenTensorProduct

  7.1-20 RightUnitor

  7.1-21 RightUnitorWithGivenTensorProduct

  7.1-22 AddRightUnitorWithGivenTensorProduct

  7.1-23 RightUnitorInverse

  7.1-24 RightUnitorInverseWithGivenTensorProduct

  7.1-25 AddRightUnitorInverseWithGivenTensorProduct

  7.1-26 LeftDistributivityExpanding

  7.1-27 LeftDistributivityExpandingWithGivenObjects

  7.1-28 AddLeftDistributivityExpandingWithGivenObjects

  7.1-29 LeftDistributivityFactoring

  7.1-30 LeftDistributivityFactoringWithGivenObjects

  7.1-31 AddLeftDistributivityFactoringWithGivenObjects

  7.1-32 RightDistributivityExpanding

  7.1-33 RightDistributivityExpandingWithGivenObjects

  7.1-34 AddRightDistributivityExpandingWithGivenObjects

  7.1-35 RightDistributivityFactoring

  7.1-36 RightDistributivityFactoringWithGivenObjects

  7.1-37 AddRightDistributivityFactoringWithGivenObjects
 7.2 Braided Monoidal Categories
 7.3 Symmetric Monoidal Categories
 7.4 Symmetric Closed Monoidal Categories

  7.4-1 InternalHomOnObjects

  7.4-2 AddInternalHomOnObjects

  7.4-3 InternalHomOnMorphisms

  7.4-4 InternalHomOnMorphismsWithGivenInternalHoms

  7.4-5 AddInternalHomOnMorphismsWithGivenInternalHoms

  7.4-6 EvaluationMorphism

  7.4-7 EvaluationMorphismWithGivenSource

  7.4-8 AddEvaluationMorphismWithGivenSource

  7.4-9 CoevaluationMorphism

  7.4-10 CoevaluationMorphismWithGivenRange

  7.4-11 AddCoevaluationMorphismWithGivenRange

  7.4-12 TensorProductToInternalHomAdjunctionMap

  7.4-13 AddTensorProductToInternalHomAdjunctionMap

  7.4-14 InternalHomToTensorProductAdjunctionMap

  7.4-15 AddInternalHomToTensorProductAdjunctionMap

  7.4-16 MonoidalPreComposeMorphism

  7.4-17 MonoidalPreComposeMorphismWithGivenObjects

  7.4-18 AddMonoidalPreComposeMorphismWithGivenObjects

  7.4-19 MonoidalPostComposeMorphism

  7.4-20 MonoidalPostComposeMorphismWithGivenObjects

  7.4-21 AddMonoidalPostComposeMorphismWithGivenObjects

  7.4-22 DualOnObjects

  7.4-23 AddDualOnObjects

  7.4-24 DualOnMorphisms

  7.4-25 DualOnMorphismsWithGivenDuals

  7.4-26 AddDualOnMorphismsWithGivenDuals

  7.4-27 EvaluationForDual

  7.4-28 EvaluationForDualWithGivenTensorProduct

  7.4-29 AddEvaluationForDualWithGivenTensorProduct

  7.4-30 CoevaluationForDual

  7.4-31 CoevaluationForDualWithGivenTensorProduct

  7.4-32 AddCoevaluationForDualWithGivenTensorProduct

  7.4-33 MorphismToBidual

  7.4-34 MorphismToBidualWithGivenBidual

  7.4-35 AddMorphismToBidualWithGivenBidual

  7.4-36 TensorProductInternalHomCompatibilityMorphism

  7.4-37 TensorProductInternalHomCompatibilityMorphismWithGivenObjects

  7.4-38 AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects

  7.4-39 TensorProductDualityCompatibilityMorphism

  7.4-40 TensorProductDualityCompatibilityMorphismWithGivenObjects

  7.4-41 AddTensorProductDualityCompatibilityMorphismWithGivenObjects

  7.4-42 MorphismFromTensorProductToInternalHom

  7.4-43 MorphismFromTensorProductToInternalHomWithGivenObjects

  7.4-44 AddMorphismFromTensorProductToInternalHomWithGivenObjects

  7.4-45 IsomorphismFromTensorProductToInternalHom

  7.4-46 AddIsomorphismFromTensorProductToInternalHom

  7.4-47 MorphismFromInternalHomToTensorProduct

  7.4-48 MorphismFromInternalHomToTensorProductWithGivenObjects

  7.4-49 AddMorphismFromInternalHomToTensorProductWithGivenObjects

  7.4-50 IsomorphismFromInternalHomToTensorProduct

  7.4-51 AddIsomorphismFromInternalHomToTensorProduct

  7.4-52 TraceMap

  7.4-53 AddTraceMap

  7.4-54 RankMorphism

  7.4-55 AddRankMorphism

  7.4-56 IsomorphismFromDualToInternalHom

  7.4-57 AddIsomorphismFromDualToInternalHom

  7.4-58 IsomorphismFromInternalHomToDual

  7.4-59 AddIsomorphismFromInternalHomToDual

  7.4-60 UniversalPropertyOfDual

  7.4-61 AddUniversalPropertyOfDual

  7.4-62 LambdaIntroduction

  7.4-63 AddLambdaIntroduction

  7.4-64 LambdaElimination

  7.4-65 AddLambdaElimination

  7.4-66 IsomorphismFromObjectToInternalHom

  7.4-67 IsomorphismFromObjectToInternalHomWithGivenInternalHom

  7.4-68 AddIsomorphismFromObjectToInternalHomWithGivenInternalHom

  7.4-69 IsomorphismFromInternalHomToObject

  7.4-70 IsomorphismFromInternalHomToObjectWithGivenInternalHom

  7.4-71 AddIsomorphismFromInternalHomToObjectWithGivenInternalHom
 7.5 Rigid Symmetric Closed Monoidal Categories

7 Tensor Product and Internal Hom

7.1 Monoidal Categories

A 6-tuple ( \mathbf{C}, \otimes, 1, \alpha, \lambda, \rho ) consisting of

is called a monoidal category, if

The corresponding GAP property is given by IsMonoidalCategory.

7.1-1 TensorProductOnObjects
‣ TensorProductOnObjects( a, b )( operation )

Returns: an object

The arguments are two objects a, b. The output is the tensor product a \otimes b.

7.1-2 AddTensorProductOnObjects
‣ AddTensorProductOnObjects( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation TensorProductOnObjects. F: (a,b) \mapsto a \otimes b.

7.1-3 TensorProductOnMorphisms
‣ TensorProductOnMorphisms( alpha, beta )( operation )

Returns: a morphism in \mathrm{Hom}(a \otimes b, a' \otimes b')

The arguments are two morphisms \alpha: a \rightarrow a', \beta: b \rightarrow b'. The output is the tensor product \alpha \otimes \beta.

7.1-4 TensorProductOnMorphismsWithGivenTensorProducts
‣ TensorProductOnMorphismsWithGivenTensorProducts( s, alpha, beta, r )( operation )

Returns: a morphism in \mathrm{Hom}(a \otimes b, a' \otimes b')

The arguments are an object s = a \otimes b, two morphisms \alpha: a \rightarrow a', \beta: b \rightarrow b', and an object r = a' \otimes b'. The output is the tensor product \alpha \otimes \beta.

7.1-5 AddTensorProductOnMorphismsWithGivenTensorProducts
‣ AddTensorProductOnMorphismsWithGivenTensorProducts( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation TensorProductOnMorphismsWithGivenTensorProducts. F: ( a \otimes b, \alpha: a \rightarrow a', \beta: b \rightarrow b', a' \otimes b' ) \mapsto \alpha \otimes \beta.

7.1-6 AssociatorRightToLeft
‣ AssociatorRightToLeft( a, b, c )( operation )

Returns: a morphism in \mathrm{Hom}( a \otimes (b \otimes c), (a \otimes b) \otimes c ).

The arguments are three objects a,b,c. The output is the associator \alpha_{a,(b,c)}: a \otimes (b \otimes c) \rightarrow (a \otimes b) \otimes c.

7.1-7 AssociatorRightToLeftWithGivenTensorProducts
‣ AssociatorRightToLeftWithGivenTensorProducts( s, a, b, c, r )( operation )

Returns: a morphism in \mathrm{Hom}( a \otimes (b \otimes c), (a \otimes b) \otimes c ).

The arguments are an object s = a \otimes (b \otimes c), three objects a,b,c, and an object r = (a \otimes b) \otimes c. The output is the associator \alpha_{a,(b,c)}: a \otimes (b \otimes c) \rightarrow (a \otimes b) \otimes c.

7.1-8 AddAssociatorRightToLeftWithGivenTensorProducts
‣ AddAssociatorRightToLeftWithGivenTensorProducts( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation AssociatorRightToLeftWithGivenTensorProducts. F: ( a \otimes (b \otimes c), a, b, c, (a \otimes b) \otimes c ) \mapsto \alpha_{a,(b,c)}.

7.1-9 AssociatorLeftToRight
‣ AssociatorLeftToRight( a, b, c )( operation )

Returns: a morphism in \mathrm{Hom}( (a \otimes b) \otimes c \rightarrow a \otimes (b \otimes c) ).

The arguments are three objects a,b,c. The output is the associator \alpha_{(a,b),c}: (a \otimes b) \otimes c \rightarrow a \otimes (b \otimes c).

7.1-10 AssociatorLeftToRightWithGivenTensorProducts
‣ AssociatorLeftToRightWithGivenTensorProducts( s, a, b, c, r )( operation )

Returns: a morphism in \mathrm{Hom}( (a \otimes b) \otimes c \rightarrow a \otimes (b \otimes c) ).

The arguments are an object s = (a \otimes b) \otimes c, three objects a,b,c, and an object r = a \otimes (b \otimes c). The output is the associator \alpha_{(a,b),c}: (a \otimes b) \otimes c \rightarrow a \otimes (b \otimes c).

7.1-11 AddAssociatorLeftToRightWithGivenTensorProducts
‣ AddAssociatorLeftToRightWithGivenTensorProducts( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation AssociatorLeftToRightWithGivenTensorProducts. F: (( a \otimes b ) \otimes c, a, b, c, a \otimes (b \otimes c )) \mapsto \alpha_{(a,b),c}.

7.1-12 TensorUnit
‣ TensorUnit( C )( attribute )

Returns: an object

The argument is a category \mathbf{C}. The output is the tensor unit 1 of \mathbf{C}.

7.1-13 AddTensorUnit
‣ AddTensorUnit( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation TensorUnit. F: ( ) \mapsto 1.

7.1-14 LeftUnitor
‣ LeftUnitor( a )( attribute )

Returns: a morphism in \mathrm{Hom}(1 \otimes a, a )

The argument is an object a. The output is the left unitor \lambda_a: 1 \otimes a \rightarrow a.

7.1-15 LeftUnitorWithGivenTensorProduct
‣ LeftUnitorWithGivenTensorProduct( a, s )( operation )

Returns: a morphism in \mathrm{Hom}(1 \otimes a, a )

The arguments are an object a and an object s = 1 \otimes a. The output is the left unitor \lambda_a: 1 \otimes a \rightarrow a.

7.1-16 AddLeftUnitorWithGivenTensorProduct
‣ AddLeftUnitorWithGivenTensorProduct( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation LeftUnitorWithGivenTensorProduct. F: (a, 1 \otimes a) \mapsto \lambda_a.

7.1-17 LeftUnitorInverse
‣ LeftUnitorInverse( a )( attribute )

Returns: a morphism in \mathrm{Hom}(a, 1 \otimes a)

The argument is an object a. The output is the inverse of the left unitor \lambda_a^{-1}: a \rightarrow 1 \otimes a.

7.1-18 LeftUnitorInverseWithGivenTensorProduct
‣ LeftUnitorInverseWithGivenTensorProduct( a, r )( operation )

Returns: a morphism in \mathrm{Hom}(a, 1 \otimes a)

The argument is an object a and an object r = 1 \otimes a. The output is the inverse of the left unitor \lambda_a^{-1}: a \rightarrow 1 \otimes a.

7.1-19 AddLeftUnitorInverseWithGivenTensorProduct
‣ AddLeftUnitorInverseWithGivenTensorProduct( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation LeftUnitorInverseWithGivenTensorProduct. F: (a, 1 \otimes a) \mapsto \lambda_a^{-1}.

7.1-20 RightUnitor
‣ RightUnitor( a )( attribute )

Returns: a morphism in \mathrm{Hom}(a \otimes 1, a )

The argument is an object a. The output is the right unitor \rho_a: a \otimes 1 \rightarrow a.

7.1-21 RightUnitorWithGivenTensorProduct
‣ RightUnitorWithGivenTensorProduct( a, s )( operation )

Returns: a morphism in \mathrm{Hom}(a \otimes 1, a )

The arguments are an object a and an object s = a \otimes 1. The output is the right unitor \rho_a: a \otimes 1 \rightarrow a.

7.1-22 AddRightUnitorWithGivenTensorProduct
‣ AddRightUnitorWithGivenTensorProduct( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation RightUnitorWithGivenTensorProduct. F: (a, a \otimes 1) \mapsto \rho_a.

7.1-23 RightUnitorInverse
‣ RightUnitorInverse( a )( attribute )

Returns: a morphism in \mathrm{Hom}( a, a \otimes 1 )

The argument is an object a. The output is the inverse of the right unitor \rho_a^{-1}: a \rightarrow a \otimes 1.

7.1-24 RightUnitorInverseWithGivenTensorProduct
‣ RightUnitorInverseWithGivenTensorProduct( a, r )( operation )

Returns: a morphism in \mathrm{Hom}( a, a \otimes 1 )

The arguments are an object a and an object r = a \otimes 1. The output is the inverse of the right unitor \rho_a^{-1}: a \rightarrow a \otimes 1.

7.1-25 AddRightUnitorInverseWithGivenTensorProduct
‣ AddRightUnitorInverseWithGivenTensorProduct( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation RightUnitorInverseWithGivenTensorProduct. F: (a, a \otimes 1) \mapsto \rho_a^{-1}.

7.1-26 LeftDistributivityExpanding
‣ LeftDistributivityExpanding( a, L )( operation )

Returns: a morphism in \mathrm{Hom}( a \otimes (b_1 \oplus \dots \oplus b_n), (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n) )

The arguments are an object a and a list of objects L = (b_1, \dots, b_n). The output is the left distributivity morphism a \otimes (b_1 \oplus \dots \oplus b_n) \rightarrow (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n).

7.1-27 LeftDistributivityExpandingWithGivenObjects
‣ LeftDistributivityExpandingWithGivenObjects( s, a, L, r )( operation )

Returns: a morphism in \mathrm{Hom}( s, r )

The arguments are an object s = a \otimes (b_1 \oplus \dots \oplus b_n), an object a, a list of objects L = (b_1, \dots, b_n), and an object r = (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n). The output is the left distributivity morphism s \rightarrow r.

7.1-28 AddLeftDistributivityExpandingWithGivenObjects
‣ AddLeftDistributivityExpandingWithGivenObjects( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation LeftDistributivityExpandingWithGivenObjects. F: (a \otimes (b_1 \oplus \dots \oplus b_n), a, L, (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n)) \mapsto \mathrm{LeftDistributivityExpandingWithGivenObjects}(a,L).

7.1-29 LeftDistributivityFactoring
‣ LeftDistributivityFactoring( a, L )( operation )

Returns: a morphism in \mathrm{Hom}( (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n), a \otimes (b_1 \oplus \dots \oplus b_n) )

The arguments are an object a and a list of objects L = (b_1, \dots, b_n). The output is the left distributivity morphism (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n) \rightarrow a \otimes (b_1 \oplus \dots \oplus b_n).

7.1-30 LeftDistributivityFactoringWithGivenObjects
‣ LeftDistributivityFactoringWithGivenObjects( s, a, L, r )( operation )

Returns: a morphism in \mathrm{Hom}( s, r )

The arguments are an object s = (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n), an object a, a list of objects L = (b_1, \dots, b_n), and an object r = a \otimes (b_1 \oplus \dots \oplus b_n). The output is the left distributivity morphism s \rightarrow r.

7.1-31 AddLeftDistributivityFactoringWithGivenObjects
‣ AddLeftDistributivityFactoringWithGivenObjects( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation LeftDistributivityFactoringWithGivenObjects. F: ((a \otimes b_1) \oplus \dots \oplus (a \otimes b_n), a, L, a \otimes (b_1 \oplus \dots \oplus b_n)) \mapsto \mathrm{LeftDistributivityFactoringWithGivenObjects}(a,L).

7.1-32 RightDistributivityExpanding
‣ RightDistributivityExpanding( L, a )( operation )

Returns: a morphism in \mathrm{Hom}( (b_1 \oplus \dots \oplus b_n) \otimes a, (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a) )

The arguments are a list of objects L = (b_1, \dots, b_n) and an object a. The output is the right distributivity morphism (b_1 \oplus \dots \oplus b_n) \otimes a \rightarrow (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a).

7.1-33 RightDistributivityExpandingWithGivenObjects
‣ RightDistributivityExpandingWithGivenObjects( s, L, a, r )( operation )

Returns: a morphism in \mathrm{Hom}( s, r )

The arguments are an object s = (b_1 \oplus \dots \oplus b_n) \otimes a, a list of objects L = (b_1, \dots, b_n), an object a, and an object r = (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a). The output is the right distributivity morphism s \rightarrow r.

7.1-34 AddRightDistributivityExpandingWithGivenObjects
‣ AddRightDistributivityExpandingWithGivenObjects( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation RightDistributivityExpandingWithGivenObjects. F: ((b_1 \oplus \dots \oplus b_n) \otimes a, L, a, (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a)) \mapsto \mathrm{RightDistributivityExpandingWithGivenObjects}(L,a).

7.1-35 RightDistributivityFactoring
‣ RightDistributivityFactoring( L, a )( operation )

Returns: a morphism in \mathrm{Hom}( (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a), (b_1 \oplus \dots \oplus b_n) \otimes a)

The arguments are a list of objects L = (b_1, \dots, b_n) and an object a. The output is the right distributivity morphism (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a) \rightarrow (b_1 \oplus \dots \oplus b_n) \otimes a .

7.1-36 RightDistributivityFactoringWithGivenObjects
‣ RightDistributivityFactoringWithGivenObjects( s, L, a, r )( operation )

Returns: a morphism in \mathrm{Hom}( s, r )

The arguments are an object s = (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a), a list of objects L = (b_1, \dots, b_n), an object a, and an object r = (b_1 \oplus \dots \oplus b_n) \otimes a. The output is the right distributivity morphism s \rightarrow r.

7.1-37 AddRightDistributivityFactoringWithGivenObjects
‣ AddRightDistributivityFactoringWithGivenObjects( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation RightDistributivityFactoringWithGivenObjects. F: ((b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a), L, a, (b_1 \oplus \dots \oplus b_n) \otimes a) \mapsto \mathrm{RightDistributivityFactoringWithGivenObjects}(L,a).

7.2 Braided Monoidal Categories

A monoidal category \mathbf{C} equipped with a natural isomorphism B_{a,b}: a \otimes b \cong b \otimes a is called a braided monoidal category if

The corresponding GAP property is given by IsBraidedMonoidalCategory.

7.2-1 Braiding
‣ Braiding( a, b )( operation )

Returns: a morphism in \mathrm{Hom}( a \otimes b, b \otimes a ).

The arguments are two objects a,b. The output is the braiding B_{a,b}: a \otimes b \rightarrow b \otimes a.

7.2-2 BraidingWithGivenTensorProducts
‣ BraidingWithGivenTensorProducts( s, a, b, r )( operation )

Returns: a morphism in \mathrm{Hom}( a \otimes b, b \otimes a ).

The arguments are an object s = a \otimes b, two objects a,b, and an object r = b \otimes a. The output is the braiding B_{a,b}: a \otimes b \rightarrow b \otimes a.

7.2-3 AddBraidingWithGivenTensorProducts
‣ AddBraidingWithGivenTensorProducts( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation BraidingWithGivenTensorProducts. F: (a \otimes b, a, b, b \otimes a) \rightarrow B_{a,b}.

7.2-4 BraidingInverse
‣ BraidingInverse( a, b )( operation )

Returns: a morphism in \mathrm{Hom}( b \otimes a, a \otimes b ).

The arguments are two objects a,b. The output is the inverse of the braiding B_{a,b}^{-1}: b \otimes a \rightarrow a \otimes b.

7.2-5 BraidingInverseWithGivenTensorProducts
‣ BraidingInverseWithGivenTensorProducts( s, a, b, r )( operation )

Returns: a morphism in \mathrm{Hom}( b \otimes a, a \otimes b ).

The arguments are an object s = b \otimes a, two objects a,b, and an object r = a \otimes b. The output is the braiding B_{a,b}^{-1}: b \otimes a \rightarrow a \otimes b.

7.2-6 AddBraidingInverseWithGivenTensorProducts
‣ AddBraidingInverseWithGivenTensorProducts( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation BraidingInverseWithGivenTensorProducts. F: (b \otimes a, a, b, a \otimes b) \rightarrow B_{a,b}^{-1}.

7.3 Symmetric Monoidal Categories

A braided monoidal category \mathbf{C} is called symmetric monoidal category if B_{a,b}^{-1} = B_{b,a}. The corresponding GAP property is given by IsSymmetricMonoidalCategory.

7.4 Symmetric Closed Monoidal Categories

A symmetric monoidal category \mathbf{C} which has for each functor - \otimes b: \mathbf{C} \rightarrow \mathbf{C} a right adjoint (denoted by \underline{\mathrm{Hom}}(b,-)) is called a symmetric closed monoidal category. The corresponding GAP property is given by IsSymmetricClosedMonoidalCategory.

7.4-1 InternalHomOnObjects
‣ InternalHomOnObjects( a, b )( operation )

Returns: an object

The arguments are two objects a,b. The output is the internal hom object \underline{\mathrm{Hom}}(a,b).

7.4-2 AddInternalHomOnObjects
‣ AddInternalHomOnObjects( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation InternalHomOnObjects. F: (a,b) \mapsto \underline{\mathrm{Hom}}(a,b).

7.4-3 InternalHomOnMorphisms
‣ InternalHomOnMorphisms( alpha, beta )( operation )

Returns: a morphism in \mathrm{Hom}( \underline{\mathrm{Hom}}(a',b), \underline{\mathrm{Hom}}(a,b') )

The arguments are two morphisms \alpha: a \rightarrow a', \beta: b \rightarrow b'. The output is the internal hom morphism \underline{\mathrm{Hom}}(\alpha,\beta): \underline{\mathrm{Hom}}(a',b) \rightarrow \underline{\mathrm{Hom}}(a,b').

7.4-4 InternalHomOnMorphismsWithGivenInternalHoms
‣ InternalHomOnMorphismsWithGivenInternalHoms( s, alpha, beta, r )( operation )

Returns: a morphism in \mathrm{Hom}( \underline{\mathrm{Hom}}(a',b), \underline{\mathrm{Hom}}(a,b') )

The arguments are an object s = \underline{\mathrm{Hom}}(a',b), two morphisms \alpha: a \rightarrow a', \beta: b \rightarrow b', and an object r = \underline{\mathrm{Hom}}(a,b'). The output is the internal hom morphism \underline{\mathrm{Hom}}(\alpha,\beta): \underline{\mathrm{Hom}}(a',b) \rightarrow \underline{\mathrm{Hom}}(a,b').

7.4-5 AddInternalHomOnMorphismsWithGivenInternalHoms
‣ AddInternalHomOnMorphismsWithGivenInternalHoms( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation InternalHomOnMorphismsWithGivenInternalHoms. F: (\underline{\mathrm{Hom}}(a',b), \alpha: a \rightarrow a', \beta: b \rightarrow b', \underline{\mathrm{Hom}}(a,b') ) \mapsto \underline{\mathrm{Hom}}(\alpha,\beta).

7.4-6 EvaluationMorphism
‣ EvaluationMorphism( a, b )( operation )

Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}}(a,b) \otimes a, b ).

The arguments are two objects a, b. The output is the evaluation morphism \mathrm{ev}_{a,b}: \mathrm{\underline{Hom}}(a,b) \otimes a \rightarrow b, i.e., the counit of the tensor hom adjunction.

7.4-7 EvaluationMorphismWithGivenSource
‣ EvaluationMorphismWithGivenSource( a, b, s )( operation )

Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}}(a,b) \otimes a, b ).

The arguments are two objects a,b and an object s = \mathrm{\underline{Hom}}(a,b) \otimes a. The output is the evaluation morphism \mathrm{ev}_{a,b}: \mathrm{\underline{Hom}}(a,b) \otimes a \rightarrow b, i.e., the counit of the tensor hom adjunction.

7.4-8 AddEvaluationMorphismWithGivenSource
‣ AddEvaluationMorphismWithGivenSource( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation EvaluationMorphismWithGivenSource. F: (a, b, \mathrm{\underline{Hom}}(a,b) \otimes a) \mapsto \mathrm{ev}_{a,b}.

7.4-9 CoevaluationMorphism
‣ CoevaluationMorphism( a, b )( operation )

Returns: a morphism in \mathrm{Hom}( a, \mathrm{\underline{Hom}}(b, a \otimes b) ).

The arguments are two objects a,b. The output is the coevaluation morphism \mathrm{coev}_{a,b}: a \rightarrow \mathrm{\underline{Hom}(b, a \otimes b)}, i.e., the unit of the tensor hom adjunction.

7.4-10 CoevaluationMorphismWithGivenRange
‣ CoevaluationMorphismWithGivenRange( a, b, r )( operation )

Returns: a morphism in \mathrm{Hom}( a, \mathrm{\underline{Hom}}(b, a \otimes b) ).

The arguments are two objects a,b and an object r = \mathrm{\underline{Hom}(b, a \otimes b)}. The output is the coevaluation morphism \mathrm{coev}_{a,b}: a \rightarrow \mathrm{\underline{Hom}(b, a \otimes b)}, i.e., the unit of the tensor hom adjunction.

7.4-11 AddCoevaluationMorphismWithGivenRange
‣ AddCoevaluationMorphismWithGivenRange( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation CoevaluationMorphismWithGivenRange. F: (a, b, \mathrm{\underline{Hom}}(b, a \otimes b)) \mapsto \mathrm{coev}_{a,b}.

7.4-12 TensorProductToInternalHomAdjunctionMap
‣ TensorProductToInternalHomAdjunctionMap( a, b, f )( operation )

Returns: a morphism in \mathrm{Hom}( a, \mathrm{\underline{Hom}}(b,c) ).

The arguments are objects a,b and a morphism f: a \otimes b \rightarrow c. The output is a morphism g: a \rightarrow \mathrm{\underline{Hom}}(b,c) corresponding to f under the tensor hom adjunction.

7.4-13 AddTensorProductToInternalHomAdjunctionMap
‣ AddTensorProductToInternalHomAdjunctionMap( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation TensorProductToInternalHomAdjunctionMap. F: (a, b, f: a \otimes b \rightarrow c) \mapsto ( g: a \rightarrow \mathrm{\underline{Hom}}(b,c) ).

7.4-14 InternalHomToTensorProductAdjunctionMap
‣ InternalHomToTensorProductAdjunctionMap( b, c, g )( operation )

Returns: a morphism in \mathrm{Hom}(a \otimes b, c).

The arguments are objects b,c and a morphism g: a \rightarrow \mathrm{\underline{Hom}}(b,c). The output is a morphism f: a \otimes b \rightarrow c corresponding to g under the tensor hom adjunction.

7.4-15 AddInternalHomToTensorProductAdjunctionMap
‣ AddInternalHomToTensorProductAdjunctionMap( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation InternalHomToTensorProductAdjunctionMap. F: (b, c, g: a \rightarrow \mathrm{\underline{Hom}}(b,c)) \mapsto ( g: a \otimes b \rightarrow c ).

7.4-16 MonoidalPreComposeMorphism
‣ MonoidalPreComposeMorphism( a, b, c )( operation )

Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c), \mathrm{\underline{Hom}}(a,c) ).

The arguments are three objects a,b,c. The output is the precomposition morphism \mathrm{MonoidalPreComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c) \rightarrow \mathrm{\underline{Hom}}(a,c).

7.4-17 MonoidalPreComposeMorphismWithGivenObjects
‣ MonoidalPreComposeMorphismWithGivenObjects( s, a, b, c, r )( operation )

Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c), \mathrm{\underline{Hom}}(a,c) ).

The arguments are an object s = \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c), three objects a,b,c, and an object r = \mathrm{\underline{Hom}}(a,c). The output is the precomposition morphism \mathrm{MonoidalPreComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c) \rightarrow \mathrm{\underline{Hom}}(a,c).

7.4-18 AddMonoidalPreComposeMorphismWithGivenObjects
‣ AddMonoidalPreComposeMorphismWithGivenObjects( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation MonoidalPreComposeMorphismWithGivenObjects. F: (\mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c),a,b,c,\mathrm{\underline{Hom}}(a,c)) \mapsto \mathrm{MonoidalPreComposeMorphismWithGivenObjects}_{a,b,c}.

7.4-19 MonoidalPostComposeMorphism
‣ MonoidalPostComposeMorphism( a, b, c )( operation )

Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b), \mathrm{\underline{Hom}}(a,c) ).

The arguments are three objects a,b,c. The output is the postcomposition morphism \mathrm{MonoidalPostComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b) \rightarrow \mathrm{\underline{Hom}}(a,c).

7.4-20 MonoidalPostComposeMorphismWithGivenObjects
‣ MonoidalPostComposeMorphismWithGivenObjects( s, a, b, c, r )( operation )

Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b), \mathrm{\underline{Hom}}(a,c) ).

The arguments are an object s = \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b), three objects a,b,c, and an object r = \mathrm{\underline{Hom}}(a,c). The output is the postcomposition morphism \mathrm{MonoidalPostComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b) \rightarrow \mathrm{\underline{Hom}}(a,c).

7.4-21 AddMonoidalPostComposeMorphismWithGivenObjects
‣ AddMonoidalPostComposeMorphismWithGivenObjects( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation MonoidalPostComposeMorphismWithGivenObjects. F: (\mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b),a,b,c,\mathrm{\underline{Hom}}(a,c)) \mapsto \mathrm{MonoidalPostComposeMorphismWithGivenObjects}_{a,b,c}.

7.4-22 DualOnObjects
‣ DualOnObjects( a )( attribute )

Returns: an object

The argument is an object a. The output is its dual object a^{\vee}.

7.4-23 AddDualOnObjects
‣ AddDualOnObjects( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation DualOnObjects. F: a \mapsto a^{\vee}.

7.4-24 DualOnMorphisms
‣ DualOnMorphisms( alpha )( attribute )

Returns: a morphism in \mathrm{Hom}( b^{\vee}, a^{\vee} ).

The argument is a morphism \alpha: a \rightarrow b. The output is its dual morphism \alpha^{\vee}: b^{\vee} \rightarrow a^{\vee}.

7.4-25 DualOnMorphismsWithGivenDuals
‣ DualOnMorphismsWithGivenDuals( s, alpha, r )( operation )

Returns: a morphism in \mathrm{Hom}( b^{\vee}, a^{\vee} ).

The argument is an object s = b^{\vee}, a morphism \alpha: a \rightarrow b, and an object r = a^{\vee}. The output is the dual morphism \alpha^{\vee}: b^{\vee} \rightarrow a^{\vee}.

7.4-26 AddDualOnMorphismsWithGivenDuals
‣ AddDualOnMorphismsWithGivenDuals( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation DualOnMorphismsWithGivenDuals. F: (b^{\vee},\alpha,a^{\vee}) \mapsto \alpha^{\vee}.

7.4-27 EvaluationForDual
‣ EvaluationForDual( a )( attribute )

Returns: a morphism in \mathrm{Hom}( a^{\vee} \otimes a, 1 ).

The argument is an object a. The output is the evaluation morphism \mathrm{ev}_{a}: a^{\vee} \otimes a \rightarrow 1.

7.4-28 EvaluationForDualWithGivenTensorProduct
‣ EvaluationForDualWithGivenTensorProduct( s, a, r )( operation )

Returns: a morphism in \mathrm{Hom}( a^{\vee} \otimes a, 1 ).

The arguments are an object s = a^{\vee} \otimes a, an object a, and an object r = 1. The output is the evaluation morphism \mathrm{ev}_{a}: a^{\vee} \otimes a \rightarrow 1.

7.4-29 AddEvaluationForDualWithGivenTensorProduct
‣ AddEvaluationForDualWithGivenTensorProduct( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation EvaluationForDualWithGivenTensorProduct. F: (a^{\vee} \otimes a, a, 1) \mapsto \mathrm{ev}_{a}.

7.4-30 CoevaluationForDual
‣ CoevaluationForDual( a )( attribute )

Returns: a morphism in \mathrm{Hom}(1,a \otimes a^{\vee}).

The argument is an object a. The output is the coevaluation morphism \mathrm{coev}_{a}:1 \rightarrow a \otimes a^{\vee}.

7.4-31 CoevaluationForDualWithGivenTensorProduct
‣ CoevaluationForDualWithGivenTensorProduct( s, a, r )( operation )

Returns: a morphism in \mathrm{Hom}(1,a \otimes a^{\vee}).

The arguments are an object s = 1, an object a, and an object r = a \otimes a^{\vee}. The output is the coevaluation morphism \mathrm{coev}_{a}:1 \rightarrow a \otimes a^{\vee}.

7.4-32 AddCoevaluationForDualWithGivenTensorProduct
‣ AddCoevaluationForDualWithGivenTensorProduct( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation CoevaluationForDualWithGivenTensorProduct. F: (1, a, a \otimes a^{\vee}) \mapsto \mathrm{coev}_{a}.

7.4-33 MorphismToBidual
‣ MorphismToBidual( a )( attribute )

Returns: a morphism in \mathrm{Hom}(a, (a^{\vee})^{\vee}).

The argument is an object a. The output is the morphism to the bidual a \rightarrow (a^{\vee})^{\vee}.

7.4-34 MorphismToBidualWithGivenBidual
‣ MorphismToBidualWithGivenBidual( a, r )( operation )

Returns: a morphism in \mathrm{Hom}(a, (a^{\vee})^{\vee}).

The arguments are an object a, and an object r = (a^{\vee})^{\vee}. The output is the morphism to the bidual a \rightarrow (a^{\vee})^{\vee}.

7.4-35 AddMorphismToBidualWithGivenBidual
‣ AddMorphismToBidualWithGivenBidual( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation MorphismToBidualWithGivenBidual. F: (a, (a^{\vee})^{\vee}) \mapsto (a \rightarrow (a^{\vee})^{\vee}).

7.4-36 TensorProductInternalHomCompatibilityMorphism
‣ TensorProductInternalHomCompatibilityMorphism( a, a', b, b' )( operation )

Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'), \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b')).

The arguments are four objects a, a', b, b'. The output is the natural morphism \mathrm{TensorProductInternalHomCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b') \rightarrow \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b').

7.4-37 TensorProductInternalHomCompatibilityMorphismWithGivenObjects
‣ TensorProductInternalHomCompatibilityMorphismWithGivenObjects( a, a', b, b', L )( operation )

Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'), \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b')).

The arguments are four objects a, a', b, b', and a list L = [ \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'), \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b') ]. The output is the natural morphism \mathrm{TensorProductInternalHomCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b') \rightarrow \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b').

7.4-38 AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects
‣ AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation TensorProductInternalHomCompatibilityMorphismWithGivenObjects. F: ( a,a',b,b', [ \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'), \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b') ]) \mapsto \mathrm{TensorProductInternalHomCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}.

7.4-39 TensorProductDualityCompatibilityMorphism
‣ TensorProductDualityCompatibilityMorphism( a, b )( operation )

Returns: a morphism in \mathrm{Hom}( a^{\vee} \otimes b^{\vee}, (a \otimes b)^{\vee} ).

The arguments are two objects a,b. The output is the natural morphism \mathrm{TensorProductDualityCompatibilityMorphismWithGivenObjects}: a^{\vee} \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}.

7.4-40 TensorProductDualityCompatibilityMorphismWithGivenObjects
‣ TensorProductDualityCompatibilityMorphismWithGivenObjects( s, a, b, r )( operation )

Returns: a morphism in \mathrm{Hom}( a^{\vee} \otimes b^{\vee}, (a \otimes b)^{\vee} ).

The arguments are an object s = a^{\vee} \otimes b^{\vee}, two objects a,b, and an object r = (a \otimes b)^{\vee}. The output is the natural morphism \mathrm{TensorProductDualityCompatibilityMorphismWithGivenObjects}_{a,b}: a^{\vee} \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}.

7.4-41 AddTensorProductDualityCompatibilityMorphismWithGivenObjects
‣ AddTensorProductDualityCompatibilityMorphismWithGivenObjects( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation TensorProductDualityCompatibilityMorphismWithGivenObjects. F: ( a^{\vee} \otimes b^{\vee}, a, b, (a \otimes b)^{\vee} ) \mapsto \mathrm{TensorProductDualityCompatibilityMorphismWithGivenObjects}_{a,b}.

7.4-42 MorphismFromTensorProductToInternalHom
‣ MorphismFromTensorProductToInternalHom( a, b )( operation )

Returns: a morphism in \mathrm{Hom}( a^{\vee} \otimes b, \mathrm{\underline{Hom}}(a,b) ).

The arguments are two objects a,b. The output is the natural morphism \mathrm{MorphismFromTensorProductToInternalHomWithGivenObjects}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}}(a,b).

7.4-43 MorphismFromTensorProductToInternalHomWithGivenObjects
‣ MorphismFromTensorProductToInternalHomWithGivenObjects( s, a, b, r )( operation )

Returns: a morphism in \mathrm{Hom}( a^{\vee} \otimes b, \mathrm{\underline{Hom}}(a,b) ).

The arguments are an object s = a^{\vee} \otimes b, two objects a,b, and an object r = \mathrm{\underline{Hom}}(a,b). The output is the natural morphism \mathrm{MorphismFromTensorProductToInternalHomWithGivenObjects}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}}(a,b).

7.4-44 AddMorphismFromTensorProductToInternalHomWithGivenObjects
‣ AddMorphismFromTensorProductToInternalHomWithGivenObjects( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation MorphismFromTensorProductToInternalHomWithGivenObjects. F: ( a^{\vee} \otimes b, a, b, \mathrm{\underline{Hom}}(a,b) ) \mapsto \mathrm{MorphismFromTensorProductToInternalHomWithGivenObjects}_{a,b}.

7.4-45 IsomorphismFromTensorProductToInternalHom
‣ IsomorphismFromTensorProductToInternalHom( a, b )( operation )

Returns: a morphism in \mathrm{Hom}( a^{\vee} \otimes b, \mathrm{\underline{Hom}}(a,b) ).

The arguments are two objects a,b. The output is the natural morphism \mathrm{IsomorphismFromTensorProductToInternalHom}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}}(a,b).

7.4-46 AddIsomorphismFromTensorProductToInternalHom
‣ AddIsomorphismFromTensorProductToInternalHom( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation IsomorphismFromTensorProductToInternalHom. F: ( a, b ) \mapsto \mathrm{IsomorphismFromTensorProductToInternalHom}_{a,b}.

7.4-47 MorphismFromInternalHomToTensorProduct
‣ MorphismFromInternalHomToTensorProduct( a, b )( operation )

Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}}(a,b), a^{\vee} \otimes b ).

The arguments are two objects a,b. The output is the inverse of \mathrm{MorphismFromTensorProductToInternalHomWithGivenObjects}, namely \mathrm{MorphismFromInternalHomToTensorProductWithGivenObjects}_{a,b}: \mathrm{\underline{Hom}}(a,b) \rightarrow a^{\vee} \otimes b.

7.4-48 MorphismFromInternalHomToTensorProductWithGivenObjects
‣ MorphismFromInternalHomToTensorProductWithGivenObjects( s, a, b, r )( operation )

Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}}(a,b), a^{\vee} \otimes b ).

The arguments are an object s = \mathrm{\underline{Hom}}(a,b), two objects a,b, and an object r = a^{\vee} \otimes b. The output is the inverse of \mathrm{MorphismFromTensorProductToInternalHomWithGivenObjects}, namely \mathrm{MorphismFromInternalHomToTensorProductWithGivenObjects}_{a,b}: \mathrm{\underline{Hom}}(a,b) \rightarrow a^{\vee} \otimes b.

7.4-49 AddMorphismFromInternalHomToTensorProductWithGivenObjects
‣ AddMorphismFromInternalHomToTensorProductWithGivenObjects( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation MorphismFromInternalHomToTensorProductWithGivenObjects. F: ( \mathrm{\underline{Hom}}(a,b),a,b,a^{\vee} \otimes b ) \mapsto \mathrm{MorphismFromInternalHomToTensorProductWithGivenObjects}_{a,b}.

7.4-50 IsomorphismFromInternalHomToTensorProduct
‣ IsomorphismFromInternalHomToTensorProduct( a, b )( operation )

Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}}(a,b), a^{\vee} \otimes b ).

The arguments are two objects a,b. The output is the inverse of \mathrm{IsomorphismFromTensorProductToInternalHom}, namely \mathrm{IsomorphismFromInternalHomToTensorProduct}_{a,b}: \mathrm{\underline{Hom}}(a,b) \rightarrow a^{\vee} \otimes b.

7.4-51 AddIsomorphismFromInternalHomToTensorProduct
‣ AddIsomorphismFromInternalHomToTensorProduct( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation IsomorphismFromInternalHomToTensorProduct. F: ( a,b ) \mapsto \mathrm{IsomorphismFromInternalHomToTensorProduct}_{a,b}.

7.4-52 TraceMap
‣ TraceMap( alpha )( attribute )

Returns: a morphism in \mathrm{Hom}(1,1).

The argument is a morphism \alpha. The output is the trace morphism \mathrm{trace}_{\alpha}: 1 \rightarrow 1.

7.4-53 AddTraceMap
‣ AddTraceMap( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation TraceMap. F: \alpha \mapsto \mathrm{trace}_{\alpha}

7.4-54 RankMorphism
‣ RankMorphism( a )( attribute )

Returns: a morphism in \mathrm{Hom}(1,1).

The argument is an object a. The output is the rank morphism \mathrm{rank}_a: 1 \rightarrow 1.

7.4-55 AddRankMorphism
‣ AddRankMorphism( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation RankMorphism. F: a \mapsto \mathrm{rank}_{a}

7.4-56 IsomorphismFromDualToInternalHom
‣ IsomorphismFromDualToInternalHom( a )( attribute )

Returns: a morphism in \mathrm{Hom}(a^{\vee}, \mathrm{Hom}(a,1)).

The argument is an object a. The output is the isomorphism \mathrm{IsomorphismFromDualToInternalHom}_{a}: a^{\vee} \rightarrow \mathrm{Hom}(a,1).

7.4-57 AddIsomorphismFromDualToInternalHom
‣ AddIsomorphismFromDualToInternalHom( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation IsomorphismFromDualToInternalHom. F: a \mapsto \mathrm{IsomorphismFromDualToInternalHom}_{a}

7.4-58 IsomorphismFromInternalHomToDual
‣ IsomorphismFromInternalHomToDual( a )( attribute )

Returns: a morphism in \mathrm{Hom}(\mathrm{Hom}(a,1), a^{\vee}).

The argument is an object a. The output is the isomorphism \mathrm{IsomorphismFromInternalHomToDual}_{a}: \mathrm{Hom}(a,1) \rightarrow a^{\vee}.

7.4-59 AddIsomorphismFromInternalHomToDual
‣ AddIsomorphismFromInternalHomToDual( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation IsomorphismFromInternalHomToDual. F: a \mapsto \mathrm{IsomorphismFromInternalHomToDual}_{a}

7.4-60 UniversalPropertyOfDual
‣ UniversalPropertyOfDual( t, a, alpha )( operation )

Returns: a morphism in \mathrm{Hom}(t, a^{\vee}).

The arguments are two objects t,a, and a morphism \alpha: t \otimes a \rightarrow 1. The output is the morphism t \rightarrow a^{\vee} given by the universal property of a^{\vee}.

7.4-61 AddUniversalPropertyOfDual
‣ AddUniversalPropertyOfDual( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation UniversalPropertyOfDual. F: ( t,a,\alpha: t \otimes a \rightarrow 1 ) \mapsto ( t \rightarrow a^{\vee} ).

7.4-62 LambdaIntroduction
‣ LambdaIntroduction( alpha )( attribute )

Returns: a morphism in \mathrm{Hom}( 1, \mathrm{\underline{Hom}}(a,b) ).

The argument is a morphism \alpha: a \rightarrow b. The output is the corresponding morphism 1 \rightarrow \mathrm{\underline{Hom}}(a,b) under the tensor hom adjunction.

7.4-63 AddLambdaIntroduction
‣ AddLambdaIntroduction( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation LambdaIntroduction. F: ( \alpha: a \rightarrow b ) \mapsto ( 1 \rightarrow \mathrm{\underline{Hom}}(a,b) ).

7.4-64 LambdaElimination
‣ LambdaElimination( a, b, alpha )( operation )

Returns: a morphism in \mathrm{Hom}(a,b).

The arguments are two objects a,b, and a morphism \alpha: 1 \rightarrow \mathrm{\underline{Hom}}(a,b). The output is a morphism a \rightarrow b corresponding to \alpha under the tensor hom adjunction.

7.4-65 AddLambdaElimination
‣ AddLambdaElimination( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation LambdaElimination. F: ( a,b,\alpha: 1 \rightarrow \mathrm{\underline{Hom}}(a,b) ) \mapsto ( a \rightarrow b ).

7.4-66 IsomorphismFromObjectToInternalHom
‣ IsomorphismFromObjectToInternalHom( a )( attribute )

Returns: a morphism in \mathrm{Hom}(a, \mathrm{\underline{Hom}}(1,a)).

The argument is an object a. The output is the natural isomorphism a \rightarrow \mathrm{\underline{Hom}}(1,a).

7.4-67 IsomorphismFromObjectToInternalHomWithGivenInternalHom
‣ IsomorphismFromObjectToInternalHomWithGivenInternalHom( a, r )( operation )

Returns: a morphism in \mathrm{Hom}(a, \mathrm{\underline{Hom}}(1,a)).

The argument is an object a, and an object r = \mathrm{\underline{Hom}}(1,a). The output is the natural isomorphism a \rightarrow \mathrm{\underline{Hom}}(1,a).

7.4-68 AddIsomorphismFromObjectToInternalHomWithGivenInternalHom
‣ AddIsomorphismFromObjectToInternalHomWithGivenInternalHom( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation IsomorphismFromObjectToInternalHomWithGivenInternalHom. F: ( a, \mathrm{\underline{Hom}}(1,a) ) \mapsto ( a \rightarrow \mathrm{\underline{Hom}}(1,a) ).

7.4-69 IsomorphismFromInternalHomToObject
‣ IsomorphismFromInternalHomToObject( a )( attribute )

Returns: a morphism in \mathrm{Hom}(\mathrm{\underline{Hom}}(1,a),a).

The argument is an object a. The output is the natural isomorphism \mathrm{\underline{Hom}}(1,a) \rightarrow a.

7.4-70 IsomorphismFromInternalHomToObjectWithGivenInternalHom
‣ IsomorphismFromInternalHomToObjectWithGivenInternalHom( a, s )( operation )

Returns: a morphism in \mathrm{Hom}(\mathrm{\underline{Hom}}(1,a),a).

The argument is an object a, and an object s = \mathrm{\underline{Hom}}(1,a). The output is the natural isomorphism \mathrm{\underline{Hom}}(1,a) \rightarrow a.

7.4-71 AddIsomorphismFromInternalHomToObjectWithGivenInternalHom
‣ AddIsomorphismFromInternalHomToObjectWithGivenInternalHom( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation IsomorphismFromInternalHomToObjectWithGivenInternalHom. F: ( a, \mathrm{\underline{Hom}}(1,a) ) \mapsto ( \mathrm{\underline{Hom}}(1,a) \rightarrow a ).

7.5 Rigid Symmetric Closed Monoidal Categories

A symmetric closed monoidal category \mathbf{C} satisfying

is called a rigid symmetric closed monoidal category.

7.5-1 TensorProductInternalHomCompatibilityMorphismInverse
‣ TensorProductInternalHomCompatibilityMorphismInverse( a, a', b, b' )( operation )

Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b'), \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b')).

The arguments are four objects a, a', b, b'. The output is the natural morphism \mathrm{TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b') \rightarrow \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b').

7.5-2 TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects
‣ TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects( a, a', b, b', L )( operation )

Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b'), \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b')).

The arguments are four objects a, a', b, b', and a list L = [ \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'), \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b') ]. The output is the natural morphism \mathrm{TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b') \rightarrow \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b').

7.5-3 AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects
‣ AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects. F: ( a,a',b,b', [ \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'), \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b') ]) \mapsto \mathrm{TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}.

7.5-4 MorphismFromBidual
‣ MorphismFromBidual( a )( attribute )

Returns: a morphism in \mathrm{Hom}((a^{\vee})^{\vee},a).

The argument is an object a. The output is the inverse of the morphism to the bidual (a^{\vee})^{\vee} \rightarrow a.

7.5-5 MorphismFromBidualWithGivenBidual
‣ MorphismFromBidualWithGivenBidual( a, s )( operation )

Returns: a morphism in \mathrm{Hom}((a^{\vee})^{\vee},a).

The argument is an object a, and an object s = (a^{\vee})^{\vee}. The output is the inverse of the morphism to the bidual (a^{\vee})^{\vee} \rightarrow a.

7.5-6 AddMorphismFromBidualWithGivenBidual
‣ AddMorphismFromBidualWithGivenBidual( C, F )( operation )

Returns: nothing

The arguments are a category C and a function F. This operations adds the given function F to the category for the basic operation MorphismFromBidualWithGivenBidual. F: (a, (a^{\vee})^{\vee}) \mapsto ((a^{\vee})^{\vee} \rightarrow a).

 [Top of Book]  [Contents]   [Previous Chapter]   [Next Chapter] 
Goto Chapter: Top 1 2 3 4 5 6 7 8 9 10 11 Ind

generated by GAPDoc2HTML