A \(6\)-tuple \(( \mathbf{C}, \otimes, 1, \alpha, \lambda, \rho )\) consisting of
a category \(\mathbf{C}\),
a functor \(\otimes: \mathbf{C} \times \mathbf{C} \rightarrow \mathbf{C}\),
an object \(1 \in \mathbf{C}\),
a natural isomorphism \(\alpha_{a,b,c}: a \otimes (b \otimes c) \cong (a \otimes b) \otimes c\),
a natural isomorphism \(\lambda_{a}: 1 \otimes a \cong a\),
a natural isomorphism \(\rho_{a}: a \otimes 1 \cong a\),
is called a monoidal category, if
for all objects \(a,b,c,d\), the pentagon identity holds: \((\alpha_{a,b,c} \otimes \mathrm{id}_d) \circ \alpha_{a,b \otimes c, d} \circ ( \mathrm{id}_a \otimes \alpha_{b,c,d} ) = \alpha_{a \otimes b, c, d} \circ \alpha_{a,b,c \otimes d}\),
for all objects \(a,c\), the triangle identity holds: \(( \rho_a \otimes \mathrm{id}_c ) \circ \alpha_{a,1,c} = \mathrm{id}_a \otimes \lambda_c\).
The corresponding GAP property is given by IsMonoidalCategory.
‣ TensorProductOnObjects( a, b ) | ( operation ) |
Returns: an object
The arguments are two objects \(a, b\). The output is the tensor product \(a \otimes b\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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)}\).
‣ 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)\).
‣ 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)\).
‣ 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}\).
‣ TensorUnit( C ) | ( attribute ) |
Returns: an object
The argument is a category \(\mathbf{C}\). The output is the tensor unit \(1\) of \(\mathbf{C}\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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}\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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}\).
‣ 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)\).
‣ 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\).
‣ 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)\).
‣ 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)\).
‣ 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\).
‣ 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)\).
‣ 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)\).
‣ 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\).
‣ 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)\).
‣ 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 \).
‣ 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\).
‣ 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)\).
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
\(\lambda_a \circ B_{a,1} = \rho_a\),
\((B_{c,a} \otimes \mathrm{id}_b) \circ \alpha_{c,a,b} \circ B_{a \otimes b,c} = \alpha_{a,c,b} \circ ( \mathrm{id}_a \otimes B_{b,c}) \circ \alpha^{-1}_{a,b,c}\),
\(( \mathrm{id}_b \otimes B_{c,a} ) \circ \alpha^{-1}_{b,c,a} \circ B_{a,b \otimes c} = \alpha^{-1}_{b,a,c} \circ (B_{a,b} \otimes \mathrm{id}_c) \circ \alpha_{a,b,c}\).
The corresponding GAP property is given by IsBraidedMonoidalCategory.
‣ 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\).
‣ 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\).
‣ 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}\).
‣ 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\).
‣ 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\).
‣ 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}\).
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.
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.
‣ 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)\).
‣ 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)\).
‣ 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')\).
‣ 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')\).
‣ 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)\).
‣ 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.
‣ 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.
‣ 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}\).
‣ 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.
‣ 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.
‣ 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}\).
‣ 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.
‣ 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) )\).
‣ 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.
‣ 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 )\).
‣ 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)\).
‣ 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)\).
‣ 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}\).
‣ 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)\).
‣ 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)\).
‣ 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}\).
‣ DualOnObjects( a ) | ( attribute ) |
Returns: an object
The argument is an object \(a\). The output is its dual object \(a^{\vee}\).
‣ 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}\).
‣ 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}\).
‣ 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}\).
‣ 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}\).
‣ 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\).
‣ 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\).
‣ 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}\).
‣ 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}\).
‣ 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}\).
‣ 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}\).
‣ 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}\).
‣ 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}\).
‣ 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})\).
‣ 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')\).
‣ 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')\).
‣ 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'}\).
‣ 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}\).
‣ 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}\).
‣ 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}\).
‣ 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)\).
‣ 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)\).
‣ 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}\).
‣ 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)\).
‣ 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}\).
‣ 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\).
‣ 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\).
‣ 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}\).
‣ 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\).
‣ 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}\).
‣ 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\).
‣ 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}\)
‣ 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\).
‣ 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}\)
‣ 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)\).
‣ 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}\)
‣ 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}\).
‣ 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}\)
‣ 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}\).
‣ 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} )\).
‣ 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.
‣ 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) )\).
‣ 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.
‣ 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 )\).
‣ 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)\).
‣ 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)\).
‣ 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) )\).
‣ 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\).
‣ 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\).
‣ 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 )\).
A symmetric closed monoidal category \(\mathbf{C}\) satisfying
the natural morphism \(\underline{\mathrm{Hom}}(a_1,b_1) \otimes \underline{\mathrm{Hom}}(a_2,b_2) \rightarrow \underline{\mathrm{Hom}}(a_1 \otimes a_2,b_1 \otimes b_2)\) is an isomorphism,
the natural morphism \(a \rightarrow \underline{\mathrm{Hom}}(\underline{\mathrm{Hom}}(a, 1), 1)\) is an isomorphism
is called a rigid symmetric closed monoidal category.
‣ 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')\).
‣ 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')\).
‣ 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'}\).
‣ 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\).
‣ 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\).
‣ 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)\).
generated by GAPDoc2HTML