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}\) compatible with the congruence of morphisms,
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} ) \sim \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} \sim \mathrm{id}_a \otimes \lambda_c\).
The corresponding GAP property is given by IsMonoidalCategory
.
‣ 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\).
‣ 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\).
‣ 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)\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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 operation adds the given function \(F\) to the category for the basic operation TensorProductOnObjects
. \(F: (a,b) \mapsto a \otimes b\).
‣ 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 operation adds the given function \(F\) to the category for the basic operation TensorUnit
. \(F: ( ) \mapsto 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\).
‣ 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\).
‣ 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\).
‣ 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\).
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} \sim \rho_a\),
\((B_{c,a} \otimes \mathrm{id}_b) \circ \alpha_{c,a,b} \circ B_{a \otimes b,c} \sim \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} \sim \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\).
‣ 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 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 inverse braiding \( B_{a,b}^{-1}: b \otimes a \rightarrow a \otimes b\).
A braided monoidal category \(\mathbf{C}\) is called symmetric monoidal category if \(B_{a,b}^{-1} \sim B_{b,a}\). The corresponding GAP property is given by IsSymmetricMonoidalCategory
.
A monoidal category \(\mathbf{C}\) which has for each functor \(- \otimes b: \mathbf{C} \rightarrow \mathbf{C}\) a right adjoint (denoted by \(\mathrm{\underline{Hom}}(b,-)\)) is called a closed monoidal category.
If no operations involving duals are installed manually, the dual objects will be derived as \(a^\vee \coloneqq \mathrm{\underline{Hom}}(a,1)\).
The corresponding GAP property is called IsClosedMonoidalCategory
.
‣ InternalHomOnObjects ( a, b ) | ( operation ) |
Returns: an object
The arguments are two objects \(a,b\). The output is the internal hom object \(\mathrm{\underline{Hom}}(a,b)\).
‣ InternalHomOnMorphisms ( alpha, beta ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}}(a',b), \mathrm{\underline{Hom}}(a,b') )\)
The arguments are two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\). The output is the internal hom morphism \(\mathrm{\underline{Hom}}(\alpha,\beta): \mathrm{\underline{Hom}}(a',b) \rightarrow \mathrm{\underline{Hom}}(a,b')\).
‣ InternalHomOnMorphismsWithGivenInternalHoms ( s, alpha, beta, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}}(a',b), \mathrm{\underline{Hom}}(a,b') )\)
The arguments are an object \(s = \mathrm{\underline{Hom}}(a',b)\), two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\), and an object \(r = \mathrm{\underline{Hom}}(a,b')\). The output is the internal hom morphism \(\mathrm{\underline{Hom}}(\alpha,\beta): \mathrm{\underline{Hom}}(a',b) \rightarrow \mathrm{\underline{Hom}}(a,b')\).
‣ 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.
‣ 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.
‣ TensorProductToInternalHomAdjunctionMap ( a, b, f ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, \mathrm{\underline{Hom}}(b,c) )\).
The arguments are two 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.
‣ TensorProductToInternalHomAdjunctionMapWithGivenInternalHom ( a, b, f, i ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, \mathrm{\underline{Hom}}(b,c) )\).
The arguments are two objects \(a,b\), a morphism \(f: a \otimes b \rightarrow c\) and an object \(i = \mathrm{\underline{Hom}}(b,c)\). The output is a morphism \(g: a \rightarrow \mathrm{\underline{Hom}}(b,c)\) corresponding to \(f\) under the tensor hom adjunction.
‣ InternalHomToTensorProductAdjunctionMap ( b, c, g ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \otimes b, c)\).
The arguments are two 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.
‣ InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct ( b, c, g, t ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \otimes b, c)\).
The arguments are two objects \(b,c\), a morphism \(g: a \rightarrow \mathrm{\underline{Hom}}(b,c)\) and an object \(t = a \otimes b\). The output is a morphism \(f: a \otimes b \rightarrow c\) corresponding to \(g\) under the tensor hom adjunction.
‣ 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)\).
‣ 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)\).
‣ DualOnObjects ( a ) | ( attribute ) |
Returns: an object
The argument is an object \(a\). The output is its dual object \(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}\).
‣ 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\).
‣ 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}\).
‣ TensorProductInternalHomCompatibilityMorphism ( list ) | ( 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 argument is a list of 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 ( s, list, r ) | ( 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 a list of four objects \([ a, a', b, b' ]\), and two objects \(s = \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b')\) and \(r = \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')\).
‣ 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}\).
‣ 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)\).
‣ IsomorphismFromDualObjectToInternalHomIntoTensorUnit ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a^{\vee}, \mathrm{\underline{Hom}}(a,1))\).
The argument is an object \(a\). The output is the isomorphism \(\mathrm{IsomorphismFromDualObjectToInternalHomIntoTensorUnit}_{a}: a^{\vee} \rightarrow \mathrm{\underline{Hom}}(a,1)\).
‣ IsomorphismFromInternalHomIntoTensorUnitToDualObject ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(\mathrm{\underline{Hom}}(a,1), a^{\vee})\).
The argument is an object \(a\). The output is the isomorphism \(\mathrm{IsomorphismFromInternalHomIntoTensorUnitToDualObject}_{a}: \mathrm{\underline{Hom}}(a,1) \rightarrow a^{\vee}\).
‣ 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}\).
‣ 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.
‣ 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.
‣ 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)\).
‣ 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\).
A monoidal category \(\mathbf{C}\) which has for each functor \(- \otimes b: \mathbf{C} \rightarrow \mathbf{C}\) a left adjoint (denoted by \(\mathrm{\underline{coHom}}(-,b)\)) is called a coclosed monoidal category.
If no operations involving coduals are installed manually, the codual objects will be derived as \(a_\vee \coloneqq \mathrm{\underline{coHom}}(1,a)\).
The corresponding GAP property is called IsCoclosedMonoidalCategory
.
‣ InternalCoHomOnObjects ( a, b ) | ( operation ) |
Returns: an object
The arguments are two objects \(a,b\). The output is the internal cohom object \(\mathrm{\underline{coHom}}(a,b)\).
‣ InternalCoHomOnMorphisms ( alpha, beta ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b'), \mathrm{\underline{coHom}}(a',b) )\)
The arguments are two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\). The output is the internal cohom morphism \(\mathrm{\underline{coHom}}(\alpha,\beta): \mathrm{\underline{coHom}}(a,b') \rightarrow \mathrm{\underline{coHom}}(a',b)\).
‣ InternalCoHomOnMorphismsWithGivenInternalCoHoms ( s, alpha, beta, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b'), \mathrm{\underline{coHom}}(a',b) )\)
The arguments are an object \(s = \mathrm{\underline{coHom}}(a,b')\), two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\), and an object \(r = \mathrm{\underline{coHom}}(a',b)\). The output is the internal cohom morphism \(\mathrm{\underline{coHom}}(\alpha,\beta): \mathrm{\underline{coHom}}(a,b') \rightarrow \mathrm{\underline{coHom}}(a',b)\).
‣ CoclosedEvaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, \mathrm{\underline{coHom}}(a,b) \otimes b )\).
The arguments are two objects \(a, b\). The output is the coclosed evaluation morphism \(\mathrm{coclev}_{a,b}: a \rightarrow \mathrm{\underline{coHom}}(a,b) \otimes b\), i.e., the unit of the cohom tensor adjunction.
‣ CoclosedEvaluationMorphismWithGivenRange ( a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, \mathrm{\underline{coHom}}(a,b) \otimes b )\).
The arguments are two objects \(a,b\) and an object \(r = \mathrm{\underline{coHom}}(a,b) \otimes b\). The output is the coclosed evaluation morphism \(\mathrm{coclev}_{a,b}: a \rightarrow \mathrm{\underline{coHom}}(a,b) \otimes b\), i.e., the unit of the cohom tensor adjunction.
‣ CoclosedCoevaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a \otimes b, b), a )\).
The arguments are two objects \(a,b\). The output is the coclosed coevaluation morphism \(\mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}}(a \otimes b, b) \rightarrow a\), i.e., the counit of the cohom tensor adjunction.
‣ CoclosedCoevaluationMorphismWithGivenSource ( a, b, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a \otimes b, b), b )\).
The arguments are two objects \(a,b\) and an object \(s = \mathrm{\underline{coHom}(a \otimes b, b)}\). The output is the coclosed coevaluation morphism \(\mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}}(a \otimes b, b) \rightarrow a\), i.e., the unit of the cohom tensor adjunction.
‣ TensorProductToInternalCoHomAdjunctionMap ( c, b, g ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b), c )\).
The arguments are two objects \(c,b\) and a morphism \(g: a \rightarrow c \otimes b\). The output is a morphism \(f: \mathrm{\underline{coHom}}(a,b) \rightarrow c\) corresponding to \(g\) under the cohom tensor adjunction.
‣ TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom ( c, b, g, i ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b), c )\).
The arguments are two objects \(c,b\), a morphism \(g: a \rightarrow c \otimes b\) and an object \(i = \mathrm{\underline{coHom}(a,b)}\). The output is a morphism \(f: \mathrm{\underline{coHom}}(a,b) \rightarrow c\) corresponding to \(g\) under the cohom tensor adjunction.
‣ InternalCoHomToTensorProductAdjunctionMap ( a, b, f ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, c \otimes b)\).
The arguments are two objects \(a,b\) and a morphism \(f: \mathrm{\underline{coHom}}(a,b) \rightarrow c\). The output is a morphism \(g: a \rightarrow c \otimes b\) corresponding to \(f\) under the cohom tensor adjunction.
‣ InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct ( a, b, f, t ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, c \otimes b)\).
The arguments are two objects \(a,b\), a morphism \(f: \mathrm{\underline{coHom}}(a,b) \rightarrow c\) and an object \(t = c \otimes b\). The output is a morphism \(g: a \rightarrow c \otimes b\) corresponding to \(f\) under the cohom tensor adjunction.
‣ MonoidalPreCoComposeMorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,c), \mathrm{\underline{coHom}}(b,c) \otimes \mathrm{\underline{coHom}}(a,b) )\).
The arguments are three objects \(a,b,c\). The output is the precocomposition morphism \(\mathrm{MonoidalPreCoComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{coHom}}(a,c) \rightarrow \mathrm{\underline{coHom}}(b,c) \otimes \mathrm{\underline{coHom}}(a,b)\).
‣ MonoidalPreCoComposeMorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,c), \mathrm{\underline{coHom}}(b,c) \otimes \mathrm{\underline{coHom}}(a,b) )\).
The arguments are an object \(s = \mathrm{\underline{coHom}}(a,c)\), three objects \(a,b,c\), and an object \(r = \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(b,c)\). The output is the precocomposition morphism \(\mathrm{MonoidalPreCoComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{coHom}}(a,c) \rightarrow \mathrm{\underline{coHom}}(b,c) \otimes \mathrm{\underline{coHom}}(a,b)\).
‣ MonoidalPostCoComposeMorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,c), \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(b,c) )\).
The arguments are three objects \(a,b,c\). The output is the postcocomposition morphism \(\mathrm{MonoidalPostCoComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{coHom}}(a,c) \rightarrow \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(b,c)\).
‣ MonoidalPostCoComposeMorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,c), \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(b,c) )\).
The arguments are an object \(s = \mathrm{\underline{coHom}}(a,c)\), three objects \(a,b,c\), and an object \(r = \mathrm{\underline{coHom}}(b,c) \otimes \mathrm{\underline{coHom}}(a,b)\). The output is the postcocomposition morphism \(\mathrm{MonoidalPostCoComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{coHom}}(a,c) \rightarrow \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(b,c)\).
‣ CoDualOnObjects ( a ) | ( attribute ) |
Returns: an object
The argument is an object \(a\). The output is its codual object \(a_{\vee}\).
‣ CoDualOnMorphisms ( 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 codual morphism \(\alpha_{\vee}: b_{\vee} \rightarrow a_{\vee}\).
‣ CoDualOnMorphismsWithGivenCoDuals ( 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}\).
‣ CoclosedEvaluationForCoDual ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( 1, a_{\vee} \otimes a )\).
The argument is an object \(a\). The output is the coclosed evaluation morphism \(\mathrm{coclev}_{a}: 1 \rightarrow a_{\vee} \otimes a\).
‣ CoclosedEvaluationForCoDualWithGivenTensorProduct ( s, a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( 1, a_{\vee} \otimes a )\).
The arguments are an object \(s = 1\), an object \(a\), and an object \(r = a_{\vee} \otimes a\). The output is the coclosed evaluation morphism \(\mathrm{coclev}_{a}: 1 \rightarrow a_{\vee} \otimes a\).
‣ MorphismFromCoBidual ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}((a_{\vee})_{\vee}, a)\).
The argument is an object \(a\). The output is the morphism from the cobidual \((a_{\vee})_{\vee} \rightarrow a\).
‣ MorphismFromCoBidualWithGivenCoBidual ( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}((a_{\vee})_{\vee}, a)\).
The arguments are an object \(a\), and an object \(s = (a_{\vee})_{\vee}\). The output is the morphism from the cobidual \((a_{\vee})_{\vee} \rightarrow a\).
‣ InternalCoHomTensorProductCompatibilityMorphism ( list ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a \otimes a', b \otimes b'), \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b'))\).
The argument is a list of four objects \([ a, a', b, b' ]\). The output is the natural morphism \(\mathrm{InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{coHom}}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b')\).
‣ InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects ( s, list, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a \otimes a', b \otimes b'), \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b') )\).
The arguments are a list of four objects \([ a, a', b, b' ]\), and two objects \(s = \mathrm{\underline{coHom}}(a \otimes a', b \otimes b')\) and \(r = \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b')\). The output is the natural morphism \(\mathrm{InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{coHom}}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b')\).
‣ CoDualityTensorProductCompatibilityMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( (a \otimes b)_{\vee}, a_{\vee} \otimes b_{\vee} )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{CoDualityTensorProductCompatibilityMorphismWithGivenObjects}: (a \otimes b)_{\vee} \rightarrow a_{\vee} \otimes b_{\vee}\).
‣ CoDualityTensorProductCompatibilityMorphismWithGivenObjects ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( (a \otimes b)_{\vee}, a_{\vee} \otimes b_{\vee} )\).
The arguments are an object \(s = (a \otimes b)_{\vee}\), two objects \(a,b\), and an object \(r = a_{\vee} \otimes b_{\vee}\). The output is the natural morphism \(\mathrm{CoDualityTensorProductCompatibilityMorphismWithGivenObjects}_{a,b}: (a \otimes b)_{\vee} \rightarrow a_{\vee} \otimes b_{\vee}\).
‣ MorphismFromInternalCoHomToTensorProduct ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b), b_{\vee} \otimes a )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{MorphismFromInternalCoHomToTensorProductWithGivenObjects}_{a,b}: \mathrm{\underline{coHom}}(a,b) \rightarrow b_{\vee} \otimes a\).
‣ MorphismFromInternalCoHomToTensorProductWithGivenObjects ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b), a \otimes b_{\vee} )\).
The arguments are an object \(s = \mathrm{\underline{coHom}}(a,b)\), two objects \(a,b\), and an object \(r = b_{\vee} \otimes a\). The output is the natural morphism \(\mathrm{MorphismFromInternalCoHomToTensorProductWithGivenObjects}_{a,b}: \mathrm{\underline{coHom}}(a,b) \rightarrow a \otimes b_{\vee}\).
‣ IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a_{\vee}, \mathrm{\underline{coHom}}(1,a))\).
The argument is an object \(a\). The output is the isomorphism \(\mathrm{IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit}_{a}: a_{\vee} \rightarrow \mathrm{\underline{coHom}}(1,a)\).
‣ IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(\mathrm{\underline{coHom}}(1,a), a_{\vee})\).
The argument is an object \(a\). The output is the isomorphism \(\mathrm{IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject}_{a}: \mathrm{\underline{coHom}}(1,a) \rightarrow a_{\vee}\).
‣ UniversalPropertyOfCoDual ( t, a, alpha ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a_{\vee}, t)\).
The arguments are two objects \(t,a\), and a morphism \(\alpha: 1 \rightarrow t \otimes a\). The output is the morphism \(a_{\vee} \rightarrow t\) given by the universal property of \(a_{\vee}\).
‣ CoLambdaIntroduction ( alpha ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b), 1 )\).
The argument is a morphism \(\alpha: a \rightarrow b\). The output is the corresponding morphism \( \mathrm{\underline{coHom}}(a,b) \rightarrow 1\) under the cohom tensor adjunction.
‣ CoLambdaElimination ( a, b, alpha ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a,b)\).
The arguments are two objects \(a,b\), and a morphism \(\alpha: \mathrm{\underline{coHom}}(a,b) \rightarrow 1\). The output is a morphism \(a \rightarrow b\) corresponding to \(\alpha\) under the cohom tensor adjunction.
‣ IsomorphismFromObjectToInternalCoHom ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a, \mathrm{\underline{coHom}}(a,1))\).
The argument is an object \(a\). The output is the natural isomorphism \(a \rightarrow \mathrm{\underline{coHom}}(a,1)\).
‣ IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom ( a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, \mathrm{\underline{coHom}}(a,1))\).
The argument is an object \(a\), and an object \(r = \mathrm{\underline{coHom}}(a,1)\). The output is the natural isomorphism \(a \rightarrow \mathrm{\underline{coHom}}(a,1)\).
‣ IsomorphismFromInternalCoHomToObject ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(\mathrm{\underline{coHom}}(a,1), a)\).
The argument is an object \(a\). The output is the natural isomorphism \(\mathrm{\underline{coHom}}(a,1) \rightarrow a\).
‣ IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom ( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(\mathrm{\underline{coHom}}(a,1), a)\).
The argument is an object \(a\), and an object \(s = \mathrm{\underline{coHom}}(a,1)\). The output is the natural isomorphism \(\mathrm{\underline{coHom}}(a,1) \rightarrow a\).
A monoidal category \(\mathbf{C}\) which is symmetric and closed is called a symmetric closed monoidal category.
The corresponding GAP property is given by IsSymmetricClosedMonoidalCategory
.
A monoidal category \(\mathbf{C}\) which is symmetric and coclosed is called a symmetric coclosed monoidal category.
The corresponding GAP property is given by IsSymmetricCoclosedMonoidalCategory
.
A symmetric closed monoidal category \(\mathbf{C}\) satisfying
the natural morphism
\(\mathrm{\underline{Hom}}(a, a') \otimes \mathrm{\underline{Hom}}(b, b') \rightarrow \mathrm{\underline{Hom}}(a \otimes b, a' \otimes b')\) is an isomorphism,
the natural morphism
\(a \rightarrow \mathrm{\underline{Hom}}(\mathrm{\underline{Hom}}(a, 1), 1)\) is an isomorphism is called a rigid symmetric closed monoidal category.
If no operations involving the closed structure are installed manually, the internal hom objects will be derived as \(\mathrm{\underline{Hom}}(a,b) \coloneqq a^\vee \otimes b\) and, in particular, \(\mathrm{\underline{Hom}}(a,1) \coloneqq a^\vee \otimes 1\).
The corresponding GAP property is given by IsRigidSymmetricClosedMonoidalCategory
.
‣ IsomorphismFromTensorProductWithDualObjectToInternalHom ( 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{IsomorphismFromTensorProductWithDualObjectToInternalHom}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}}(a,b)\).
‣ IsomorphismFromInternalHomToTensorProductWithDualObject ( 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{IsomorphismFromTensorProductWithDualObjectToInternalHom}\), namely \(\mathrm{IsomorphismFromInternalHomToTensorProductWithDualObject}_{a,b}: \mathrm{\underline{Hom}}(a,b) \rightarrow a^{\vee} \otimes 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\).
‣ TensorProductInternalHomCompatibilityMorphismInverse ( list ) | ( 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 argument is a list of 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 ( s, list, r ) | ( 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 a list of four objects \([ a, a', b, b' ]\), and two objects \(s = \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b')\) and \(r = \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(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')\).
‣ 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}\).
‣ TraceMap ( alpha ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(1,1)\).
The argument is an endomorphism \(\alpha: a \rightarrow a\). The output is the trace morphism \(\mathrm{trace}_{\alpha}: 1 \rightarrow 1\).
‣ 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\).
‣ 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\).
A symmetric coclosed monoidal category \(\mathbf{C}\) satisfying
the natural morphism
\(\mathrm{\underline{coHom}}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}}(a, b) \otimes \mathrm{\underline{coHom}}(a', b')\) is an isomorphism,
the natural morphism
\(\mathrm{\underline{coHom}}(1, \mathrm{\underline{coHom}}(1, a)) \rightarrow a\) is an isomorphism is called a rigid symmetric coclosed monoidal category.
If no operations involving the coclosed structure are installed manually, the internal cohom objects will be derived as \(\mathrm{\underline{coHom}}(a,b) \coloneqq a \otimes b_\vee\) and, in particular, \(\mathrm{\underline{coHom}}(1,a) \coloneqq 1 \otimes a_\vee\).
The corresponding GAP property is given by IsRigidSymmetricCoclosedMonoidalCategory
.
‣ IsomorphismFromInternalCoHomToTensorProductWithCoDualObject ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b), b_{\vee} \otimes a )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{IsomorphismFromInternalCoHomToTensorProductWithCoDualObjectWithGivenObjects}_{a,b}: \mathrm{\underline{coHom}}(a,b) \rightarrow b_{\vee} \otimes a\).
‣ IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a_{\vee} \otimes b, \mathrm{\underline{coHom}}(b,a)\).
The arguments are two objects \(a,b\). The output is the inverse of \(\mathrm{IsomorphismFromInternalCoHomToTensorProductWithCoDualObject}\), namely \(\mathrm{IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom}_{a,b}: a_{\vee} \otimes b \rightarrow \mathrm{\underline{coHom}}(b,a)\).
‣ MorphismFromTensorProductToInternalCoHom ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a_{\vee} \otimes b, \mathrm{\underline{coHom}}(b,a) )\).
The arguments are two objects \(a,b\). The output is the inverse of \(\mathrm{MorphismFromInternalCoHomToTensorProductWithGivenObjects}\), namely \(\mathrm{MorphismFromTensorProductToInternalCoHomWithGivenObjects}_{a,b}: a_{\vee} \otimes b \rightarrow \mathrm{\underline{coHom}}(b,a)\).
‣ MorphismFromTensorProductToInternalCoHomWithGivenObjects ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a_{\vee} \otimes b, \mathrm{\underline{coHom}}(b,a)\).
The arguments are an object \(s_{\vee} = a \otimes b\), two objects \(a,b\), and an object \(r = \mathrm{\underline{coHom}}(b,a)\). The output is the inverse of \(\mathrm{MorphismFromInternalCoHomToTensorProductWithGivenObjects}\), namely \(\mathrm{MorphismFromTensorProductToInternalCoHomWithGivenObjects}_{a,b}: a_{\vee} \otimes b \rightarrow \mathrm{\underline{coHom}}(b,a)\).
‣ InternalCoHomTensorProductCompatibilityMorphismInverse ( list ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b'), \mathrm{\underline{coHom}}(a \otimes a', b \otimes b' )\).
The argument is a list of four objects \([ a, a', b, b' ]\). The output is the natural morphism \(\mathrm{InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b') \rightarrow \mathrm{\underline{coHom}}(a \otimes a', b \otimes b')\).
‣ InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects ( s, list, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b'), \mathrm{\underline{coHom}}(a \otimes a', b \otimes b' )\).
The arguments are a list of four objects \([ a, a', b, b' ]\), and two objects \(s = \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b')\) and \(r = \mathrm{\underline{coHom}}(a \otimes a', b \otimes b')\). The output is the natural morphism \(\mathrm{InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b') \rightarrow \mathrm{\underline{coHom}}(a \otimes a', b \otimes b')\).
‣ CoclosedCoevaluationForCoDual ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a \otimes a_{\vee}, 1)\).
The argument is an object \(a\). The output is the coclosed coevaluation morphism \(\mathrm{coclcoev}_{a}: a \otimes a_{\vee} \rightarrow 1\).
‣ CoclosedCoevaluationForCoDualWithGivenTensorProduct ( s, a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \otimes a_{\vee}, 1)\).
The arguments are an object \(s = a \otimes a_{\vee}\), an object \(a\), and an object \(r = 1\). The output is the coclosed coevaluation morphism \(\mathrm{coclcoev}_{a}: a \otimes a_{\vee} \rightarrow 1\).
‣ CoTraceMap ( alpha ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(1,1)\).
The argument is an endomorphism \(\alpha: a \rightarrow a\). The output is the cotrace morphism \(\mathrm{cotrace}_{\alpha}: 1 \rightarrow 1\).
‣ CoRankMorphism ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(1,1)\).
The argument is an object \(a\). The output is the corank morphism \(\mathrm{corank}_a: 1 \rightarrow 1\).
‣ MorphismToCoBidual ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a, (a_{\vee})_{\vee})\).
The argument is an object \(a\). The output is the inverse of the morphism from the cobidual \(a \rightarrow (a_{\vee})_{\vee}\).
‣ MorphismToCoBidualWithGivenCoBidual ( a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a,(a_{\vee})_{\vee})\).
The argument is an object \(a\), and an object \(r = (a_{\vee})_{\vee}\). The output is the inverse of the morphism from the cobidual \(a \rightarrow (a_{\vee})_{\vee}\).
‣ InternalHom ( a, b ) | ( operation ) |
Returns: a cell
This is a convenience method. The arguments are two cells \(a,b\). The output is the internal hom cell. If \(a,b\) are two CAP objects the output is the internal Hom object \(\mathrm{\underline{Hom}}(a,b)\). If at least one of the arguments is a CAP morphism the output is a CAP morphism, namely the internal hom on morphisms, where any object is replaced by its identity morphism.
‣ InternalCoHom ( a, b ) | ( operation ) |
Returns: a cell
This is a convenience method. The arguments are two cells \(a,b\). The output is the internal cohom cell. If \(a,b\) are two CAP objects the output is the internal cohom object \(\mathrm{\underline{coHom}}(a,b)\). If at least one of the arguments is a CAP morphism the output is a CAP morphism, namely the internal cohom on morphisms, where any object is replaced by its identity morphism.
‣ AddLeftDistributivityExpanding ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftDistributivityExpanding
. \(F: ( a, L ) \mapsto \mathtt{LeftDistributivityExpanding}(a, L)\).
‣ AddLeftDistributivityExpandingWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftDistributivityExpandingWithGivenObjects
. \(F: ( s, a, L, r ) \mapsto \mathtt{LeftDistributivityExpandingWithGivenObjects}(s, a, L, r)\).
‣ AddLeftDistributivityFactoring ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftDistributivityFactoring
. \(F: ( a, L ) \mapsto \mathtt{LeftDistributivityFactoring}(a, L)\).
‣ AddLeftDistributivityFactoringWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftDistributivityFactoringWithGivenObjects
. \(F: ( s, a, L, r ) \mapsto \mathtt{LeftDistributivityFactoringWithGivenObjects}(s, a, L, r)\).
‣ AddRightDistributivityExpanding ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightDistributivityExpanding
. \(F: ( L, a ) \mapsto \mathtt{RightDistributivityExpanding}(L, a)\).
‣ AddRightDistributivityExpandingWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightDistributivityExpandingWithGivenObjects
. \(F: ( s, L, a, r ) \mapsto \mathtt{RightDistributivityExpandingWithGivenObjects}(s, L, a, r)\).
‣ AddRightDistributivityFactoring ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightDistributivityFactoring
. \(F: ( L, a ) \mapsto \mathtt{RightDistributivityFactoring}(L, a)\).
‣ AddRightDistributivityFactoringWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightDistributivityFactoringWithGivenObjects
. \(F: ( s, L, a, r ) \mapsto \mathtt{RightDistributivityFactoringWithGivenObjects}(s, L, a, r)\).
‣ AddBraiding ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation Braiding
. \(F: ( a, b ) \mapsto \mathtt{Braiding}(a, b)\).
‣ AddBraidingInverse ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation BraidingInverse
. \(F: ( a, b ) \mapsto \mathtt{BraidingInverse}(a, b)\).
‣ AddBraidingInverseWithGivenTensorProducts ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation BraidingInverseWithGivenTensorProducts
. \(F: ( s, a, b, r ) \mapsto \mathtt{BraidingInverseWithGivenTensorProducts}(s, a, b, r)\).
‣ AddBraidingWithGivenTensorProducts ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation BraidingWithGivenTensorProducts
. \(F: ( s, a, b, r ) \mapsto \mathtt{BraidingWithGivenTensorProducts}(s, a, b, r)\).
‣ AddCoevaluationMorphism ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoevaluationMorphism
. \(F: ( a, b ) \mapsto \mathtt{CoevaluationMorphism}(a, b)\).
‣ AddCoevaluationMorphismWithGivenRange ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoevaluationMorphismWithGivenRange
. \(F: ( a, b, r ) \mapsto \mathtt{CoevaluationMorphismWithGivenRange}(a, b, r)\).
‣ AddDualOnMorphisms ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DualOnMorphisms
. \(F: ( alpha ) \mapsto \mathtt{DualOnMorphisms}(alpha)\).
‣ AddDualOnMorphismsWithGivenDuals ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DualOnMorphismsWithGivenDuals
. \(F: ( s, alpha, r ) \mapsto \mathtt{DualOnMorphismsWithGivenDuals}(s, alpha, r)\).
‣ AddDualOnObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DualOnObjects
. \(F: ( a ) \mapsto \mathtt{DualOnObjects}(a)\).
‣ AddEvaluationForDual ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EvaluationForDual
. \(F: ( a ) \mapsto \mathtt{EvaluationForDual}(a)\).
‣ AddEvaluationForDualWithGivenTensorProduct ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EvaluationForDualWithGivenTensorProduct
. \(F: ( s, a, r ) \mapsto \mathtt{EvaluationForDualWithGivenTensorProduct}(s, a, r)\).
‣ AddEvaluationMorphism ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EvaluationMorphism
. \(F: ( a, b ) \mapsto \mathtt{EvaluationMorphism}(a, b)\).
‣ AddEvaluationMorphismWithGivenSource ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EvaluationMorphismWithGivenSource
. \(F: ( a, b, s ) \mapsto \mathtt{EvaluationMorphismWithGivenSource}(a, b, s)\).
‣ AddInternalHomOnMorphisms ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InternalHomOnMorphisms
. \(F: ( alpha, beta ) \mapsto \mathtt{InternalHomOnMorphisms}(alpha, beta)\).
‣ AddInternalHomOnMorphismsWithGivenInternalHoms ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InternalHomOnMorphismsWithGivenInternalHoms
. \(F: ( s, alpha, beta, r ) \mapsto \mathtt{InternalHomOnMorphismsWithGivenInternalHoms}(s, alpha, beta, r)\).
‣ AddInternalHomOnObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InternalHomOnObjects
. \(F: ( a, b ) \mapsto \mathtt{InternalHomOnObjects}(a, b)\).
‣ AddInternalHomToTensorProductAdjunctionMap ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InternalHomToTensorProductAdjunctionMap
. \(F: ( b, c, g ) \mapsto \mathtt{InternalHomToTensorProductAdjunctionMap}(b, c, g)\).
‣ AddInternalHomToTensorProductAdjunctionMapWithGivenTensorProduct ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct
. \(F: ( b, c, g, t ) \mapsto \mathtt{InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct}(b, c, g, t)\).
‣ AddIsomorphismFromDualObjectToInternalHomIntoTensorUnit ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromDualObjectToInternalHomIntoTensorUnit
. \(F: ( a ) \mapsto \mathtt{IsomorphismFromDualObjectToInternalHomIntoTensorUnit}(a)\).
‣ AddIsomorphismFromInternalHomIntoTensorUnitToDualObject ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromInternalHomIntoTensorUnitToDualObject
. \(F: ( a ) \mapsto \mathtt{IsomorphismFromInternalHomIntoTensorUnitToDualObject}(a)\).
‣ AddIsomorphismFromInternalHomToObject ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromInternalHomToObject
. \(F: ( a ) \mapsto \mathtt{IsomorphismFromInternalHomToObject}(a)\).
‣ AddIsomorphismFromInternalHomToObjectWithGivenInternalHom ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromInternalHomToObjectWithGivenInternalHom
. \(F: ( a, s ) \mapsto \mathtt{IsomorphismFromInternalHomToObjectWithGivenInternalHom}(a, s)\).
‣ AddIsomorphismFromObjectToInternalHom ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromObjectToInternalHom
. \(F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToInternalHom}(a)\).
‣ AddIsomorphismFromObjectToInternalHomWithGivenInternalHom ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromObjectToInternalHomWithGivenInternalHom
. \(F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToInternalHomWithGivenInternalHom}(a, r)\).
‣ AddLambdaElimination ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LambdaElimination
. \(F: ( a, b, alpha ) \mapsto \mathtt{LambdaElimination}(a, b, alpha)\).
‣ AddLambdaIntroduction ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LambdaIntroduction
. \(F: ( alpha ) \mapsto \mathtt{LambdaIntroduction}(alpha)\).
‣ AddMonoidalPostComposeMorphism ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MonoidalPostComposeMorphism
. \(F: ( a, b, c ) \mapsto \mathtt{MonoidalPostComposeMorphism}(a, b, c)\).
‣ AddMonoidalPostComposeMorphismWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MonoidalPostComposeMorphismWithGivenObjects
. \(F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPostComposeMorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddMonoidalPreComposeMorphism ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MonoidalPreComposeMorphism
. \(F: ( a, b, c ) \mapsto \mathtt{MonoidalPreComposeMorphism}(a, b, c)\).
‣ AddMonoidalPreComposeMorphismWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MonoidalPreComposeMorphismWithGivenObjects
. \(F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPreComposeMorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddMorphismFromTensorProductToInternalHom ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismFromTensorProductToInternalHom
. \(F: ( a, b ) \mapsto \mathtt{MorphismFromTensorProductToInternalHom}(a, b)\).
‣ AddMorphismFromTensorProductToInternalHomWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismFromTensorProductToInternalHomWithGivenObjects
. \(F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromTensorProductToInternalHomWithGivenObjects}(s, a, b, r)\).
‣ AddMorphismToBidual ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismToBidual
. \(F: ( a ) \mapsto \mathtt{MorphismToBidual}(a)\).
‣ AddMorphismToBidualWithGivenBidual ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismToBidualWithGivenBidual
. \(F: ( a, r ) \mapsto \mathtt{MorphismToBidualWithGivenBidual}(a, r)\).
‣ AddTensorProductDualityCompatibilityMorphism ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TensorProductDualityCompatibilityMorphism
. \(F: ( a, b ) \mapsto \mathtt{TensorProductDualityCompatibilityMorphism}(a, b)\).
‣ AddTensorProductDualityCompatibilityMorphismWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TensorProductDualityCompatibilityMorphismWithGivenObjects
. \(F: ( s, a, b, r ) \mapsto \mathtt{TensorProductDualityCompatibilityMorphismWithGivenObjects}(s, a, b, r)\).
‣ AddTensorProductInternalHomCompatibilityMorphism ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TensorProductInternalHomCompatibilityMorphism
. \(F: ( list ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphism}(list)\).
‣ AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TensorProductInternalHomCompatibilityMorphismWithGivenObjects
. \(F: ( source, list, range ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphismWithGivenObjects}(source, list, range)\).
‣ AddTensorProductToInternalHomAdjunctionMap ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TensorProductToInternalHomAdjunctionMap
. \(F: ( a, b, f ) \mapsto \mathtt{TensorProductToInternalHomAdjunctionMap}(a, b, f)\).
‣ AddTensorProductToInternalHomAdjunctionMapWithGivenInternalHom ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TensorProductToInternalHomAdjunctionMapWithGivenInternalHom
. \(F: ( a, b, f, i ) \mapsto \mathtt{TensorProductToInternalHomAdjunctionMapWithGivenInternalHom}(a, b, f, i)\).
‣ AddUniversalPropertyOfDual ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation UniversalPropertyOfDual
. \(F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfDual}(t, a, alpha)\).
‣ AddCoDualOnMorphisms ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoDualOnMorphisms
. \(F: ( alpha ) \mapsto \mathtt{CoDualOnMorphisms}(alpha)\).
‣ AddCoDualOnMorphismsWithGivenCoDuals ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoDualOnMorphismsWithGivenCoDuals
. \(F: ( s, alpha, r ) \mapsto \mathtt{CoDualOnMorphismsWithGivenCoDuals}(s, alpha, r)\).
‣ AddCoDualOnObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoDualOnObjects
. \(F: ( a ) \mapsto \mathtt{CoDualOnObjects}(a)\).
‣ AddCoDualityTensorProductCompatibilityMorphism ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoDualityTensorProductCompatibilityMorphism
. \(F: ( a, b ) \mapsto \mathtt{CoDualityTensorProductCompatibilityMorphism}(a, b)\).
‣ AddCoDualityTensorProductCompatibilityMorphismWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoDualityTensorProductCompatibilityMorphismWithGivenObjects
. \(F: ( s, a, b, r ) \mapsto \mathtt{CoDualityTensorProductCompatibilityMorphismWithGivenObjects}(s, a, b, r)\).
‣ AddCoLambdaElimination ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoLambdaElimination
. \(F: ( a, b, alpha ) \mapsto \mathtt{CoLambdaElimination}(a, b, alpha)\).
‣ AddCoLambdaIntroduction ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoLambdaIntroduction
. \(F: ( alpha ) \mapsto \mathtt{CoLambdaIntroduction}(alpha)\).
‣ AddCoclosedCoevaluationMorphism ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoclosedCoevaluationMorphism
. \(F: ( a, b ) \mapsto \mathtt{CoclosedCoevaluationMorphism}(a, b)\).
‣ AddCoclosedCoevaluationMorphismWithGivenSource ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoclosedCoevaluationMorphismWithGivenSource
. \(F: ( a, b, s ) \mapsto \mathtt{CoclosedCoevaluationMorphismWithGivenSource}(a, b, s)\).
‣ AddCoclosedEvaluationForCoDual ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoclosedEvaluationForCoDual
. \(F: ( a ) \mapsto \mathtt{CoclosedEvaluationForCoDual}(a)\).
‣ AddCoclosedEvaluationForCoDualWithGivenTensorProduct ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoclosedEvaluationForCoDualWithGivenTensorProduct
. \(F: ( s, a, r ) \mapsto \mathtt{CoclosedEvaluationForCoDualWithGivenTensorProduct}(s, a, r)\).
‣ AddCoclosedEvaluationMorphism ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoclosedEvaluationMorphism
. \(F: ( a, b ) \mapsto \mathtt{CoclosedEvaluationMorphism}(a, b)\).
‣ AddCoclosedEvaluationMorphismWithGivenRange ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoclosedEvaluationMorphismWithGivenRange
. \(F: ( a, b, r ) \mapsto \mathtt{CoclosedEvaluationMorphismWithGivenRange}(a, b, r)\).
‣ AddInternalCoHomOnMorphisms ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InternalCoHomOnMorphisms
. \(F: ( alpha, beta ) \mapsto \mathtt{InternalCoHomOnMorphisms}(alpha, beta)\).
‣ AddInternalCoHomOnMorphismsWithGivenInternalCoHoms ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InternalCoHomOnMorphismsWithGivenInternalCoHoms
. \(F: ( s, alpha, beta, r ) \mapsto \mathtt{InternalCoHomOnMorphismsWithGivenInternalCoHoms}(s, alpha, beta, r)\).
‣ AddInternalCoHomOnObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InternalCoHomOnObjects
. \(F: ( a, b ) \mapsto \mathtt{InternalCoHomOnObjects}(a, b)\).
‣ AddInternalCoHomTensorProductCompatibilityMorphism ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InternalCoHomTensorProductCompatibilityMorphism
. \(F: ( list ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphism}(list)\).
‣ AddInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects
. \(F: ( source, list, range ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}(source, list, range)\).
‣ AddInternalCoHomToTensorProductAdjunctionMap ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InternalCoHomToTensorProductAdjunctionMap
. \(F: ( a, b, f ) \mapsto \mathtt{InternalCoHomToTensorProductAdjunctionMap}(a, b, f)\).
‣ AddInternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct
. \(F: ( a, b, f, t ) \mapsto \mathtt{InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct}(a, b, f, t)\).
‣ AddIsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit
. \(F: ( a ) \mapsto \mathtt{IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit}(a)\).
‣ AddIsomorphismFromInternalCoHomFromTensorUnitToCoDualObject ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject
. \(F: ( a ) \mapsto \mathtt{IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject}(a)\).
‣ AddIsomorphismFromInternalCoHomToObject ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromInternalCoHomToObject
. \(F: ( a ) \mapsto \mathtt{IsomorphismFromInternalCoHomToObject}(a)\).
‣ AddIsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom
. \(F: ( a, s ) \mapsto \mathtt{IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom}(a, s)\).
‣ AddIsomorphismFromObjectToInternalCoHom ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromObjectToInternalCoHom
. \(F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToInternalCoHom}(a)\).
‣ AddIsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom
. \(F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom}(a, r)\).
‣ AddMonoidalPostCoComposeMorphism ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MonoidalPostCoComposeMorphism
. \(F: ( a, b, c ) \mapsto \mathtt{MonoidalPostCoComposeMorphism}(a, b, c)\).
‣ AddMonoidalPostCoComposeMorphismWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MonoidalPostCoComposeMorphismWithGivenObjects
. \(F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPostCoComposeMorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddMonoidalPreCoComposeMorphism ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MonoidalPreCoComposeMorphism
. \(F: ( a, b, c ) \mapsto \mathtt{MonoidalPreCoComposeMorphism}(a, b, c)\).
‣ AddMonoidalPreCoComposeMorphismWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MonoidalPreCoComposeMorphismWithGivenObjects
. \(F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPreCoComposeMorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddMorphismFromCoBidual ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismFromCoBidual
. \(F: ( a ) \mapsto \mathtt{MorphismFromCoBidual}(a)\).
‣ AddMorphismFromCoBidualWithGivenCoBidual ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismFromCoBidualWithGivenCoBidual
. \(F: ( a, s ) \mapsto \mathtt{MorphismFromCoBidualWithGivenCoBidual}(a, s)\).
‣ AddMorphismFromInternalCoHomToTensorProduct ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismFromInternalCoHomToTensorProduct
. \(F: ( a, b ) \mapsto \mathtt{MorphismFromInternalCoHomToTensorProduct}(a, b)\).
‣ AddMorphismFromInternalCoHomToTensorProductWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismFromInternalCoHomToTensorProductWithGivenObjects
. \(F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromInternalCoHomToTensorProductWithGivenObjects}(s, a, b, r)\).
‣ AddTensorProductToInternalCoHomAdjunctionMap ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TensorProductToInternalCoHomAdjunctionMap
. \(F: ( c, b, g ) \mapsto \mathtt{TensorProductToInternalCoHomAdjunctionMap}(c, b, g)\).
‣ AddTensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom
. \(F: ( c, b, g, i ) \mapsto \mathtt{TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom}(c, b, g, i)\).
‣ AddUniversalPropertyOfCoDual ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation UniversalPropertyOfCoDual
. \(F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfCoDual}(t, a, alpha)\).
‣ AddAssociatorLeftToRight ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation AssociatorLeftToRight
. \(F: ( a, b, c ) \mapsto \mathtt{AssociatorLeftToRight}(a, b, c)\).
‣ AddAssociatorLeftToRightWithGivenTensorProducts ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation AssociatorLeftToRightWithGivenTensorProducts
. \(F: ( s, a, b, c, r ) \mapsto \mathtt{AssociatorLeftToRightWithGivenTensorProducts}(s, a, b, c, r)\).
‣ AddAssociatorRightToLeft ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation AssociatorRightToLeft
. \(F: ( a, b, c ) \mapsto \mathtt{AssociatorRightToLeft}(a, b, c)\).
‣ AddAssociatorRightToLeftWithGivenTensorProducts ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation AssociatorRightToLeftWithGivenTensorProducts
. \(F: ( s, a, b, c, r ) \mapsto \mathtt{AssociatorRightToLeftWithGivenTensorProducts}(s, a, b, c, r)\).
‣ AddLeftUnitor ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftUnitor
. \(F: ( a ) \mapsto \mathtt{LeftUnitor}(a)\).
‣ AddLeftUnitorInverse ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftUnitorInverse
. \(F: ( a ) \mapsto \mathtt{LeftUnitorInverse}(a)\).
‣ AddLeftUnitorInverseWithGivenTensorProduct ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftUnitorInverseWithGivenTensorProduct
. \(F: ( a, r ) \mapsto \mathtt{LeftUnitorInverseWithGivenTensorProduct}(a, r)\).
‣ AddLeftUnitorWithGivenTensorProduct ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftUnitorWithGivenTensorProduct
. \(F: ( a, s ) \mapsto \mathtt{LeftUnitorWithGivenTensorProduct}(a, s)\).
‣ AddRightUnitor ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightUnitor
. \(F: ( a ) \mapsto \mathtt{RightUnitor}(a)\).
‣ AddRightUnitorInverse ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightUnitorInverse
. \(F: ( a ) \mapsto \mathtt{RightUnitorInverse}(a)\).
‣ AddRightUnitorInverseWithGivenTensorProduct ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightUnitorInverseWithGivenTensorProduct
. \(F: ( a, r ) \mapsto \mathtt{RightUnitorInverseWithGivenTensorProduct}(a, r)\).
‣ AddRightUnitorWithGivenTensorProduct ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightUnitorWithGivenTensorProduct
. \(F: ( a, s ) \mapsto \mathtt{RightUnitorWithGivenTensorProduct}(a, s)\).
‣ AddTensorProductOnMorphisms ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TensorProductOnMorphisms
. \(F: ( alpha, beta ) \mapsto \mathtt{TensorProductOnMorphisms}(alpha, beta)\).
‣ AddTensorProductOnMorphismsWithGivenTensorProducts ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TensorProductOnMorphismsWithGivenTensorProducts
. \(F: ( s, alpha, beta, r ) \mapsto \mathtt{TensorProductOnMorphismsWithGivenTensorProducts}(s, alpha, beta, r)\).
‣ AddCoevaluationForDual ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoevaluationForDual
. \(F: ( a ) \mapsto \mathtt{CoevaluationForDual}(a)\).
‣ AddCoevaluationForDualWithGivenTensorProduct ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoevaluationForDualWithGivenTensorProduct
. \(F: ( s, a, r ) \mapsto \mathtt{CoevaluationForDualWithGivenTensorProduct}(s, a, r)\).
‣ AddIsomorphismFromInternalHomToTensorProductWithDualObject ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromInternalHomToTensorProductWithDualObject
. \(F: ( a, b ) \mapsto \mathtt{IsomorphismFromInternalHomToTensorProductWithDualObject}(a, b)\).
‣ AddIsomorphismFromTensorProductWithDualObjectToInternalHom ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromTensorProductWithDualObjectToInternalHom
. \(F: ( a, b ) \mapsto \mathtt{IsomorphismFromTensorProductWithDualObjectToInternalHom}(a, b)\).
‣ AddMorphismFromBidual ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismFromBidual
. \(F: ( a ) \mapsto \mathtt{MorphismFromBidual}(a)\).
‣ AddMorphismFromBidualWithGivenBidual ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismFromBidualWithGivenBidual
. \(F: ( a, s ) \mapsto \mathtt{MorphismFromBidualWithGivenBidual}(a, s)\).
‣ AddMorphismFromInternalHomToTensorProduct ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismFromInternalHomToTensorProduct
. \(F: ( a, b ) \mapsto \mathtt{MorphismFromInternalHomToTensorProduct}(a, b)\).
‣ AddMorphismFromInternalHomToTensorProductWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismFromInternalHomToTensorProductWithGivenObjects
. \(F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromInternalHomToTensorProductWithGivenObjects}(s, a, b, r)\).
‣ AddRankMorphism ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RankMorphism
. \(F: ( a ) \mapsto \mathtt{RankMorphism}(a)\).
‣ AddTensorProductInternalHomCompatibilityMorphismInverse ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TensorProductInternalHomCompatibilityMorphismInverse
. \(F: ( list ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphismInverse}(list)\).
‣ AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects
. \(F: ( source, list, range ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects}(source, list, range)\).
‣ AddTraceMap ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TraceMap
. \(F: ( alpha ) \mapsto \mathtt{TraceMap}(alpha)\).
‣ AddCoRankMorphism ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoRankMorphism
. \(F: ( a ) \mapsto \mathtt{CoRankMorphism}(a)\).
‣ AddCoTraceMap ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoTraceMap
. \(F: ( alpha ) \mapsto \mathtt{CoTraceMap}(alpha)\).
‣ AddCoclosedCoevaluationForCoDual ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoclosedCoevaluationForCoDual
. \(F: ( a ) \mapsto \mathtt{CoclosedCoevaluationForCoDual}(a)\).
‣ AddCoclosedCoevaluationForCoDualWithGivenTensorProduct ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoclosedCoevaluationForCoDualWithGivenTensorProduct
. \(F: ( s, a, r ) \mapsto \mathtt{CoclosedCoevaluationForCoDualWithGivenTensorProduct}(s, a, r)\).
‣ AddInternalCoHomTensorProductCompatibilityMorphismInverse ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InternalCoHomTensorProductCompatibilityMorphismInverse
. \(F: ( list ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphismInverse}(list)\).
‣ AddInternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects
. \(F: ( source, list, range ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects}(source, list, range)\).
‣ AddIsomorphismFromInternalCoHomToTensorProductWithCoDualObject ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromInternalCoHomToTensorProductWithCoDualObject
. \(F: ( a, b ) \mapsto \mathtt{IsomorphismFromInternalCoHomToTensorProductWithCoDualObject}(a, b)\).
‣ AddIsomorphismFromTensorProductWithCoDualObjectToInternalCoHom ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom
. \(F: ( a, b ) \mapsto \mathtt{IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom}(a, b)\).
‣ AddMorphismFromTensorProductToInternalCoHom ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismFromTensorProductToInternalCoHom
. \(F: ( a, b ) \mapsto \mathtt{MorphismFromTensorProductToInternalCoHom}(a, b)\).
‣ AddMorphismFromTensorProductToInternalCoHomWithGivenObjects ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismFromTensorProductToInternalCoHomWithGivenObjects
. \(F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromTensorProductToInternalCoHomWithGivenObjects}(s, a, b, r)\).
‣ AddMorphismToCoBidual ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismToCoBidual
. \(F: ( a ) \mapsto \mathtt{MorphismToCoBidual}(a)\).
‣ AddMorphismToCoBidualWithGivenCoBidual ( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismToCoBidualWithGivenCoBidual
. \(F: ( a, r ) \mapsto \mathtt{MorphismToCoBidualWithGivenCoBidual}(a, r)\).
generated by GAPDoc2HTML