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.
‣ TensorUnit ( C ) | ( attribute ) |
Returns: an object
The argument is a category \mathbf{C}. The output is the tensor unit 1 of \mathbf{C}.
‣ 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}_\ell}(b,-)) is called a left closed monoidal category.
If no operations involving left duals are installed manually, the left dual objects will be derived as a^\vee \coloneqq \mathrm{\underline{Hom}_\ell}(a,1).
The corresponding GAP property is called IsLeftClosedMonoidalCategory
.
‣ LeftInternalHomOnObjects ( a, b ) | ( operation ) |
Returns: an object
The arguments are two objects a,b. The output is the internal hom object \mathrm{\underline{Hom}_\ell}(a,b).
‣ LeftInternalHomOnMorphisms ( alpha, beta ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}_\ell}(a',b), \mathrm{\underline{Hom}_\ell}(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}_\ell}(\alpha,\beta): \mathrm{\underline{Hom}_\ell}(a',b) \rightarrow \mathrm{\underline{Hom}_\ell}(a,b').
‣ LeftInternalHomOnMorphismsWithGivenLeftInternalHoms ( s, alpha, beta, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r )
The arguments are an object s = \mathrm{\underline{Hom}_\ell}(a',b), two morphisms \alpha: a \rightarrow a', \beta: b \rightarrow b', and an object r = \mathrm{\underline{Hom}_\ell}(a,b'). The output is the internal hom morphism \mathrm{\underline{Hom}_\ell}(\alpha,\beta): \mathrm{\underline{Hom}_\ell}(a',b) \rightarrow \mathrm{\underline{Hom}_\ell}(a,b').
‣ LeftClosedMonoidalEvaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}_\ell}(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}_\ell}(a,b) \otimes a \rightarrow b, i.e., the counit of the tensor hom adjunction.
‣ LeftClosedMonoidalEvaluationMorphismWithGivenSource ( a, b, s ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, b ).
The arguments are two objects a,b and an object s = \mathrm{\underline{Hom}_\ell}(a,b) \otimes a. The output is the evaluation morphism \mathrm{ev}_{a,b}: \mathrm{\underline{Hom}_\ell}(a,b) \otimes a \rightarrow b, i.e., the counit of the tensor hom adjunction.
‣ LeftClosedMonoidalCoevaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( b, \mathrm{\underline{Hom}_\ell}(a, b \otimes a) ).
The arguments are two objects a,b. The output is the coevaluation morphism \mathrm{coev}_{a,b}: b \rightarrow \mathrm{\underline{Hom}_\ell}(a, b \otimes a), i.e., the unit of the tensor hom adjunction.
‣ LeftClosedMonoidalCoevaluationMorphismWithGivenRange ( a, b, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( b, r ).
The arguments are two objects a,b and an object r = \mathrm{\underline{Hom}_\ell}(a, b \otimes a). The output is the coevaluation morphism \mathrm{coev}_{a,b}: b \rightarrow \mathrm{\underline{Hom}_\ell}(a, b \otimes a), i.e., the unit of the tensor hom adjunction.
‣ TensorProductToLeftInternalHomAdjunctMorphism ( a, b, f ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( a, \mathrm{\underline{Hom}_\ell}(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}_\ell}(b,c) corresponding to f under the tensor hom adjunction.
‣ TensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom ( a, b, f, i ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( a, i ).
The arguments are two objects a,b, a morphism f: a \otimes b \rightarrow c and an object i = \mathrm{\underline{Hom}_\ell}(b,c). The output is a morphism g: a \rightarrow \mathrm{\underline{Hom}_\ell}(b,c) corresponding to f under the tensor hom adjunction.
‣ LeftInternalHomToTensorProductAdjunctMorphism ( 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}_\ell}(b,c). The output is a morphism f: a \otimes b \rightarrow c corresponding to g under the tensor hom adjunction.
‣ LeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct ( b, c, g, t ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}(t, c).
The arguments are two objects b,c, a morphism g: a \rightarrow \mathrm{\underline{Hom}_\ell}(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.
‣ LeftClosedMonoidalPreComposeMorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}_\ell}(a,b) \otimes \mathrm{\underline{Hom}_\ell}(b,c), \mathrm{\underline{Hom}_\ell}(a,c) ).
The arguments are three objects a,b,c. The output is the precomposition morphism \mathrm{LeftClosedMonoidalPreComposeMorphism}_{a,b,c}: \mathrm{\underline{Hom}_\ell}(a,b) \otimes \mathrm{\underline{Hom}_\ell}(b,c) \rightarrow \mathrm{\underline{Hom}_\ell}(a,c).
‣ LeftClosedMonoidalPreComposeMorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
The arguments are an object s = \mathrm{\underline{Hom}_\ell}(a,b) \otimes \mathrm{\underline{Hom}_\ell}(b,c), three objects a,b,c, and an object r = \mathrm{\underline{Hom}_\ell}(a,c). The output is the precomposition morphism \mathrm{LeftClosedMonoidalPreComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{Hom}_\ell}(a,b) \otimes \mathrm{\underline{Hom}_\ell}(b,c) \rightarrow \mathrm{\underline{Hom}_\ell}(a,c).
‣ LeftClosedMonoidalPostComposeMorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}_\ell}(b,c) \otimes \mathrm{\underline{Hom}_\ell}(a,b), \mathrm{\underline{Hom}_\ell}(a,c) ).
The arguments are three objects a,b,c. The output is the postcomposition morphism \mathrm{LeftClosedMonoidalPostComposeMorphism}_{a,b,c}: \mathrm{\underline{Hom}_\ell}(b,c) \otimes \mathrm{\underline{Hom}_\ell}(a,b) \rightarrow \mathrm{\underline{Hom}_\ell}(a,c).
‣ LeftClosedMonoidalPostComposeMorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
The arguments are an object s = \mathrm{\underline{Hom}_\ell}(b,c) \otimes \mathrm{\underline{Hom}_\ell}(a,b), three objects a,b,c, and an object r = \mathrm{\underline{Hom}_\ell}(a,c). The output is the postcomposition morphism \mathrm{LeftClosedMonoidalPostComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{Hom}_\ell}(b,c) \otimes \mathrm{\underline{Hom}_\ell}(a,b) \rightarrow \mathrm{\underline{Hom}_\ell}(a,c).
‣ LeftDualOnObjects ( a ) | ( attribute ) |
Returns: an object
The argument is an object a. The output is its dual object a^{\vee}.
‣ LeftDualOnMorphisms ( 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}.
‣ LeftDualOnMorphismsWithGivenLeftDuals ( s, alpha, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
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}.
‣ LeftClosedMonoidalEvaluationForLeftDual ( 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.
‣ LeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct ( s, a, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
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.
‣ MorphismToLeftBidual ( 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}.
‣ MorphismToLeftBidualWithGivenLeftBidual ( a, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}(a, r).
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}.
‣ TensorProductLeftInternalHomCompatibilityMorphism ( list ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{Hom}_\ell}(a,a') \otimes \mathrm{\underline{Hom}_\ell}(b,b'), \mathrm{\underline{Hom}_\ell}(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{TensorProductLeftInternalHomCompatibilityMorphism}_{a,a',b,b'}: \mathrm{\underline{Hom}_\ell}(a,a') \otimes \mathrm{\underline{Hom}_\ell}(b,b') \rightarrow \mathrm{\underline{Hom}_\ell}(a \otimes b,a' \otimes b').
‣ TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects ( s, list, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
The arguments are a list of four objects [ a, a', b, b' ], and two objects s = \mathrm{\underline{Hom}_\ell}(a,a') \otimes \mathrm{\underline{Hom}_\ell}(b,b') and r = \mathrm{\underline{Hom}_\ell}(a \otimes b,a' \otimes b'). The output is the natural morphism \mathrm{TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{Hom}_\ell}(a,a') \otimes \mathrm{\underline{Hom}_\ell}(b,b') \rightarrow \mathrm{\underline{Hom}_\ell}(a \otimes b,a' \otimes b').
‣ TensorProductLeftDualityCompatibilityMorphism ( 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{TensorProductLeftDualityCompatibilityMorphism}: a^{\vee} \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}.
‣ TensorProductLeftDualityCompatibilityMorphismWithGivenObjects ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
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{TensorProductLeftDualityCompatibilityMorphismWithGivenObjects}_{a,b}: a^{\vee} \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}.
‣ MorphismFromTensorProductToLeftInternalHom ( a, b ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( a^{\vee} \otimes b, \mathrm{\underline{Hom}_\ell}(a,b) ).
The arguments are two objects a,b. The output is the natural morphism \mathrm{MorphismFromTensorProductToLeftInternalHom}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}_\ell}(a,b).
‣ MorphismFromTensorProductToLeftInternalHomWithGivenObjects ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
The arguments are an object s = a^{\vee} \otimes b, two objects a,b, and an object r = \mathrm{\underline{Hom}_\ell}(a,b). The output is the natural morphism \mathrm{MorphismFromTensorProductToLeftInternalHomWithGivenObjects}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}_\ell}(a,b).
‣ IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit ( a ) | ( attribute ) |
Returns: a morphism in \mathrm{Hom}(a^{\vee}, \mathrm{\underline{Hom}_\ell}(a,1)).
The argument is an object a. The output is the isomorphism \mathrm{IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit}_{a}: a^{\vee} \rightarrow \mathrm{\underline{Hom}_\ell}(a,1).
‣ IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject ( a ) | ( attribute ) |
Returns: a morphism in \mathrm{Hom}(\mathrm{\underline{Hom}_\ell}(a,1), a^{\vee}).
The argument is an object a. The output is the isomorphism \mathrm{IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject}_{a}: \mathrm{\underline{Hom}_\ell}(a,1) \rightarrow a^{\vee}.
‣ UniversalPropertyOfLeftDual ( 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}.
‣ LeftClosedMonoidalLambdaIntroduction ( alpha ) | ( attribute ) |
Returns: a morphism in \mathrm{Hom}( 1, \mathrm{\underline{Hom}_\ell}(a,b) ).
The argument is a morphism \alpha: a \rightarrow b. The output is the corresponding morphism 1 \rightarrow \mathrm{\underline{Hom}_\ell}(a,b) under the tensor hom adjunction.
‣ LeftClosedMonoidalLambdaElimination ( 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}_\ell}(a,b). The output is a morphism a \rightarrow b corresponding to \alpha under the tensor hom adjunction.
‣ IsomorphismFromObjectToLeftInternalHom ( a ) | ( attribute ) |
Returns: a morphism in \mathrm{Hom}(a, \mathrm{\underline{Hom}_\ell}(1,a)).
The argument is an object a. The output is the natural isomorphism a \rightarrow \mathrm{\underline{Hom}_\ell}(1,a).
‣ IsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom ( a, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}(a, r).
The argument is an object a, and an object r = \mathrm{\underline{Hom}_\ell}(1,a). The output is the natural isomorphism a \rightarrow \mathrm{\underline{Hom}_\ell}(1,a).
‣ IsomorphismFromLeftInternalHomToObject ( a ) | ( attribute ) |
Returns: a morphism in \mathrm{Hom}(\mathrm{\underline{Hom}_\ell}(1,a),a).
The argument is an object a. The output is the natural isomorphism \mathrm{\underline{Hom}_\ell}(1,a) \rightarrow a.
‣ IsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom ( a, s ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}(s,a).
The argument is an object a, and an object s = \mathrm{\underline{Hom}_\ell}(1,a). The output is the natural isomorphism \mathrm{\underline{Hom}_\ell}(1,a) \rightarrow a.
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}_\ell}(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}_\ell}(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}( s, r )
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').
‣ ClosedMonoidalRightEvaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}(a \otimes \mathrm{\underline{Hom}}(a,b), b ).
The arguments are two objects a, b. The output is the right evaluation morphism \mathrm{ev}_{a,b}:a \otimes \mathrm{\underline{Hom}}(a,b) \rightarrow b, i.e., the counit of the tensor hom adjunction.
‣ ClosedMonoidalRightEvaluationMorphismWithGivenSource ( a, b, s ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, b ).
The arguments are two objects a,b and an object s = a \otimes \mathrm{\underline{Hom}}(a,b). The output is the right evaluation morphism \mathrm{ev}_{a,b}: a \otimes \mathrm{\underline{Hom}}(a,b) \rightarrow b, i.e., the counit of the tensor hom adjunction.
‣ ClosedMonoidalRightCoevaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( b, \mathrm{\underline{Hom}}(a, a \otimes b) ).
The arguments are two objects a,b. The output is the right coevaluation morphism \mathrm{coev}_{a,b}: b \rightarrow \mathrm{\underline{Hom}}(a, a \otimes b), i.e., the unit of the tensor hom adjunction.
‣ ClosedMonoidalRightCoevaluationMorphismWithGivenRange ( a, b, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( b, r ).
The arguments are two objects a,b and an object r = \mathrm{\underline{Hom}}(a, a \otimes b). The output is the right coevaluation morphism \mathrm{coev}_{a,b}: b \rightarrow \mathrm{\underline{Hom}}(a, a \otimes b), i.e., the unit of the tensor hom adjunction.
‣ TensorProductToInternalHomRightAdjunctMorphism ( a, b, f ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( b, \mathrm{\underline{Hom}}(a,c) ).
The arguments are two objects a,b and a morphism f: a \otimes b \rightarrow c. The output is a morphism g: b \rightarrow \mathrm{\underline{Hom}}(a,c) corresponding to f under the tensor hom adjunction.
‣ TensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom ( a, b, f, i ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( b, i ).
The arguments are two objects a,b, a morphism f: a \otimes b \rightarrow c and an object i = \mathrm{\underline{Hom}}(a,c). The output is a morphism g: b \rightarrow i corresponding to f under the tensor hom adjunction.
‣ TensorProductToInternalHomRightAdjunctionIsomorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( H(a \otimes b, c), H(b, \mathrm{\underline{Hom}}(a,c)) ).
The arguments are three objects a,b,c. The output is the tri-natural isomorphism H(a \otimes b, c) \to H(b, \mathrm{\underline{Hom}}(a,c)) in the range category of the homomorphism structure H.
‣ TensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
The arguments are fives objects s,a,b,c,r where s = H(a \otimes b, c) and r = H(b, \mathrm{\underline{Hom}}(a,c)). The output is the tri-natural isomorphism s \to r in the range category of the homomorphism structure H.
‣ InternalHomToTensorProductRightAdjunctMorphism ( a, c, g ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}(a \otimes b, c).
The arguments are two objects a,c and a morphism g: b \rightarrow \mathrm{\underline{Hom}}(a,c). The output is a morphism f: a \otimes b \rightarrow c corresponding to g under the tensor hom adjunction.
‣ InternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct ( a, c, g, s ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}(s, c).
The arguments are two objects a,c, a morphism g: b \rightarrow \mathrm{\underline{Hom}}(a,c) and an object s = a \otimes b. The output is a morphism f: s \rightarrow c corresponding to g under the tensor hom adjunction.
‣ InternalHomToTensorProductRightAdjunctionIsomorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( H(b, \mathrm{\underline{Hom}}(a,c)), H(a \otimes b, c) ).
The arguments are three objects a,b,c. The output is the tri-natural isomorphism H(b, \mathrm{\underline{Hom}}(a,c)) \to H(a \otimes b, c) in the range category of the homomorphism structure H.
‣ InternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
The arguments are fives objects s,a,b,c,r where s = H(b, \mathrm{\underline{Hom}}(a,c)) and r = H(a \otimes b, c). The output is the tri-natural isomorphism s \to r in the range category of the homomorphism structure H.
‣ ClosedMonoidalLeftEvaluationMorphism ( 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 left evaluation morphism \mathrm{ev}_{a,b}: \mathrm{\underline{Hom}}(a,b) \otimes a \rightarrow b, i.e., the counit of the tensor hom adjunction.
‣ ClosedMonoidalLeftEvaluationMorphismWithGivenSource ( a, b, s ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, b ).
The arguments are two objects a,b and an object s = \mathrm{\underline{Hom}}(a,b) \otimes a. The output is the left evaluation morphism \mathrm{ev}_{a,b}: \mathrm{\underline{Hom}}(a,b) \otimes a \rightarrow b, i.e., the counit of the tensor hom adjunction.
‣ ClosedMonoidalLeftCoevaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( b, \mathrm{\underline{Hom}}(a, b \otimes a) ).
The arguments are two objects a,b. The output is the left coevaluation morphism \mathrm{coev}_{a,b}: b \rightarrow \mathrm{\underline{Hom}}(a, b \otimes a), i.e., the unit of the tensor hom adjunction.
‣ ClosedMonoidalLeftCoevaluationMorphismWithGivenRange ( a, b, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( b, r ).
The arguments are two objects a,b and an object r = \mathrm{\underline{Hom}}(a, b \otimes a). The output is the left coevaluation morphism \mathrm{coev}_{a,b}: b \rightarrow \mathrm{\underline{Hom}}(a, b \otimes a), i.e., the unit of the tensor hom adjunction.
‣ TensorProductToInternalHomLeftAdjunctMorphism ( 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.
‣ TensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom ( a, b, f, i ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( a, i ).
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 i corresponding to f under the tensor hom adjunction.
‣ TensorProductToInternalHomLeftAdjunctionIsomorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( H(a \otimes b, c), H(a, \mathrm{\underline{Hom}}(b,c)) ).
The arguments are three objects a,b,c. The output is the tri-natural isomorphism H(a \otimes b, c) \to H(a, \mathrm{\underline{Hom}}(b,c)) in the range category of the homomorphism structure H.
‣ TensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
The arguments are fives objects s,a,b,c,r where s = H(a \otimes b, c) and r = H(a, \mathrm{\underline{Hom}}(b,c)). The output is the tri-natural isomorphism s \to r in the range category of the homomorphism structure H.
‣ InternalHomToTensorProductLeftAdjunctMorphism ( 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.
‣ InternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct ( b, c, g, s ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}(s, c).
The arguments are two objects b,c, a morphism g: a \rightarrow \mathrm{\underline{Hom}}(b,c) and an object s = a \otimes b. The output is a morphism f: s \rightarrow c corresponding to g under the tensor hom adjunction.
‣ InternalHomToTensorProductLeftAdjunctionIsomorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( H(a, \mathrm{\underline{Hom}}(b,c)), H(a \otimes b, c) ).
The arguments are three objects a,b,c. The output is the tri-natural isomorphism H(a, \mathrm{\underline{Hom}}(b,c)) \to H(a \otimes b, c) in the range category of the homomorphism structure H.
‣ InternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
The arguments are fives objects s,a,b,c,r where s = H(a, \mathrm{\underline{Hom}}(b,c)) and r = H(a \otimes b, c). The output is the tri-natural isomorphism s \to r in the range category of the homomorphism structure H.
‣ 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{MonoidalPreComposeMorphism}_{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}( s, r ).
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{MonoidalPostComposeMorphism}_{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}( s, r ).
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}( s, r ).
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}( s, r ).
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, r).
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{TensorProductInternalHomCompatibilityMorphism}_{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}( s, r ).
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{TensorProductDualityCompatibilityMorphism}: a^{\vee} \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}.
‣ TensorProductDualityCompatibilityMorphismWithGivenObjects ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
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{MorphismFromTensorProductToInternalHom}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}}(a,b).
‣ MorphismFromTensorProductToInternalHomWithGivenObjects ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
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, r).
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}(s,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 left coclosed monoidal category.
If no operations involving left coduals are installed manually, the left codual objects will be derived as a_\vee \coloneqq \mathrm{\underline{coHom}}(1,a).
The corresponding GAP property is called IsLeftCoclosedMonoidalCategory
.
‣ LeftInternalCoHomOnObjects ( a, b ) | ( operation ) |
Returns: an object
The arguments are two objects a,b. The output is the internal cohom object \mathrm{\underline{coHom}_\ell}(a,b).
‣ LeftInternalCoHomOnMorphisms ( alpha, beta ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a,b'), \mathrm{\underline{coHom}_\ell}(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}_\ell}(\alpha,\beta): \mathrm{\underline{coHom}_\ell}(a,b') \rightarrow \mathrm{\underline{coHom}_\ell}(a',b).
‣ LeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms ( s, alpha, beta, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r )
The arguments are an object s = \mathrm{\underline{coHom}_\ell}(a,b'), two morphisms \alpha: a \rightarrow a', \beta: b \rightarrow b', and an object r = \mathrm{\underline{coHom}_\ell}(a',b). The output is the internal cohom morphism \mathrm{\underline{coHom}_\ell}(\alpha,\beta): \mathrm{\underline{coHom}_\ell}(a,b') \rightarrow \mathrm{\underline{coHom}_\ell}(a',b).
‣ LeftCoclosedMonoidalEvaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( b, \mathrm{\underline{coHom}_\ell}(b,a) \otimes a ).
The arguments are two objects a, b. The output is the coclosed evaluation morphism \mathrm{coclev}_{a,b}: b \rightarrow \mathrm{\underline{coHom}_\ell}(b,a) \otimes a, i.e., the unit of the cohom tensor adjunction.
‣ LeftCoclosedMonoidalEvaluationMorphismWithGivenRange ( a, b, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( b, r ).
The arguments are two objects a,b and an object r = \mathrm{\underline{coHom}_\ell}(b,a) \otimes a. The output is the coclosed evaluation morphism \mathrm{coclev}_{a,b}: b \rightarrow \mathrm{\underline{coHom}_\ell}(b,a) \otimes a, i.e., the unit of the cohom tensor adjunction.
‣ LeftCoclosedMonoidalCoevaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(b \otimes a, a), b ).
The arguments are two objects a,b. The output is the coclosed coevaluation morphism \mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}_\ell}(b \otimes a, a) \rightarrow b, i.e., the counit of the cohom tensor adjunction.
‣ LeftCoclosedMonoidalCoevaluationMorphismWithGivenSource ( a, b, s ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, b ).
The arguments are two objects a,b and an object s = \mathrm{\underline{coHom}_\ell}(b \otimes a, a). The output is the coclosed coevaluation morphism \mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}_\ell}(b \otimes a, a) \rightarrow b, i.e., the unit of the cohom tensor adjunction.
‣ TensorProductToLeftInternalCoHomAdjunctMorphism ( b, c, g ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a,c), b ).
The arguments are two objects b,c and a morphism g: a \rightarrow b \otimes c. The output is a morphism f: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow b corresponding to g under the cohom tensor adjunction.
‣ TensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom ( b, c, g, i ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( i, b ).
The arguments are two objects b,c, a morphism g: a \rightarrow b \otimes c and an object i = \mathrm{\underline{coHom}_\ell}(a,c). The output is a morphism f: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow b corresponding to g under the cohom tensor adjunction.
‣ LeftInternalCoHomToTensorProductAdjunctMorphism ( a, c, f ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}(a, b \otimes c).
The arguments are two objects a,c and a morphism f: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow b. The output is a morphism g: a \rightarrow b \otimes c corresponding to f under the cohom tensor adjunction.
‣ LeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct ( a, c, f, t ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( a, t ).
The arguments are two objects a,c, a morphism f: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow b and an object t = b \otimes c. The output is a morphism g: a \rightarrow b \otimes c corresponding to f under the cohom tensor adjunction.
‣ LeftCoclosedMonoidalPreCoComposeMorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a,c), \mathrm{\underline{coHom}_\ell}(b,c) \otimes \mathrm{\underline{coHom}_\ell}(a,b) ).
The arguments are three objects a,b,c. The output is the precocomposition morphism \mathrm{LeftCoclosedMonoidalPreCoComposeMorphism}_{a,b,c}: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow \mathrm{\underline{coHom}_\ell}(b,c) \otimes \mathrm{\underline{coHom}_\ell}(a,b).
‣ LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
The arguments are an object s = \mathrm{\underline{coHom}_\ell}(a,c), three objects a,b,c, and an object r = \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(b,c). The output is the precocomposition morphism \mathrm{LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow \mathrm{\underline{coHom}_\ell}(b,c) \otimes \mathrm{\underline{coHom}_\ell}(a,b).
‣ LeftCoclosedMonoidalPostCoComposeMorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a,c), \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(b,c) ).
The arguments are three objects a,b,c. The output is the postcocomposition morphism \mathrm{LeftCoclosedMonoidalPostCoComposeMorphism}_{a,b,c}: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(b,c).
‣ LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
The arguments are an object s = \mathrm{\underline{coHom}_\ell}(a,c), three objects a,b,c, and an object r = \mathrm{\underline{coHom}_\ell}(b,c) \otimes \mathrm{\underline{coHom}_\ell}(a,b). The output is the postcocomposition morphism \mathrm{LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(b,c).
‣ LeftCoDualOnObjects ( a ) | ( attribute ) |
Returns: an object
The argument is an object a. The output is its codual object a_{\vee}.
‣ LeftCoDualOnMorphisms ( 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}.
‣ LeftCoDualOnMorphismsWithGivenLeftCoDuals ( s, alpha, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
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}.
‣ LeftCoclosedMonoidalEvaluationForLeftCoDual ( 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.
‣ LeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct ( s, a, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
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.
‣ MorphismFromLeftCoBidual ( 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.
‣ MorphismFromLeftCoBidualWithGivenLeftCoBidual ( a, s ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}(s, 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.
‣ LeftInternalCoHomTensorProductCompatibilityMorphism ( list ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a \otimes a', b \otimes b'), \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(a',b')).
The argument is a list of four objects [ a, a', b, b' ]. The output is the natural morphism \mathrm{LeftInternalCoHomTensorProductCompatibilityMorphism}_{a,a',b,b'}: \mathrm{\underline{coHom}_\ell}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(a',b').
‣ LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects ( s, list, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
The arguments are a list of four objects [ a, a', b, b' ], and two objects s = \mathrm{\underline{coHom}_\ell}(a \otimes a', b \otimes b') and r = \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(a',b'). The output is the natural morphism \mathrm{LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{coHom}_\ell}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(a',b').
‣ LeftCoDualityTensorProductCompatibilityMorphism ( 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{LeftCoDualityTensorProductCompatibilityMorphism}: (a \otimes b)_{\vee} \rightarrow a_{\vee} \otimes b_{\vee}.
‣ LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
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{LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects}_{a,b}: (a \otimes b)_{\vee} \rightarrow a_{\vee} \otimes b_{\vee}.
‣ MorphismFromLeftInternalCoHomToTensorProduct ( a, b ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a,b), b_{\vee} \otimes a ).
The arguments are two objects a,b. The output is the natural morphism \mathrm{MorphismFromLeftInternalCoHomToTensorProduct}_{a,b}: \mathrm{\underline{coHom}_\ell}(a,b) \rightarrow b_{\vee} \otimes a.
‣ MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
The arguments are an object s = \mathrm{\underline{coHom}_\ell}(a,b), two objects a,b, and an object r = b_{\vee} \otimes a. The output is the natural morphism \mathrm{MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects}_{a,b}: \mathrm{\underline{coHom}_\ell}(a,b) \rightarrow a \otimes b_{\vee}.
‣ IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit ( a ) | ( attribute ) |
Returns: a morphism in \mathrm{Hom}(a_{\vee}, \mathrm{\underline{coHom}_\ell}(1,a)).
The argument is an object a. The output is the isomorphism \mathrm{IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit}_{a}: a_{\vee} \rightarrow \mathrm{\underline{coHom}_\ell}(1,a).
‣ IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject ( a ) | ( attribute ) |
Returns: a morphism in \mathrm{Hom}(\mathrm{\underline{coHom}_\ell}(1,a), a_{\vee}).
The argument is an object a. The output is the isomorphism \mathrm{IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject}_{a}: \mathrm{\underline{coHom}_\ell}(1,a) \rightarrow a_{\vee}.
‣ UniversalPropertyOfLeftCoDual ( 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}.
‣ LeftCoclosedMonoidalLambdaIntroduction ( alpha ) | ( attribute ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a,b), 1 ).
The argument is a morphism \alpha: a \rightarrow b. The output is the corresponding morphism \mathrm{\underline{coHom}_\ell}(a,b) \rightarrow 1 under the cohom tensor adjunction.
‣ LeftCoclosedMonoidalLambdaElimination ( 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}_\ell}(a,b) \rightarrow 1. The output is a morphism a \rightarrow b corresponding to \alpha under the cohom tensor adjunction.
‣ IsomorphismFromObjectToLeftInternalCoHom ( a ) | ( attribute ) |
Returns: a morphism in \mathrm{Hom}(a, \mathrm{\underline{coHom}_\ell}(a,1)).
The argument is an object a. The output is the natural isomorphism a \rightarrow \mathrm{\underline{coHom}_\ell}(a,1).
‣ IsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom ( a, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}(a, r).
The argument is an object a, and an object r = \mathrm{\underline{coHom}_\ell}(a,1). The output is the natural isomorphism a \rightarrow \mathrm{\underline{coHom}_\ell}(a,1).
‣ IsomorphismFromLeftInternalCoHomToObject ( a ) | ( attribute ) |
Returns: a morphism in \mathrm{Hom}(\mathrm{\underline{coHom}_\ell}(a,1), a).
The argument is an object a. The output is the natural isomorphism \mathrm{\underline{coHom}_\ell}(a,1) \rightarrow a.
‣ IsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom ( a, s ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}(s, a).
The argument is an object a, and an object s = \mathrm{\underline{coHom}_\ell}(a,1). The output is the natural isomorphism \mathrm{\underline{coHom}_\ell}(a,1) \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}( s, r )
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).
‣ CoclosedMonoidalRightEvaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( b, a \otimes \mathrm{\underline{coHom}}(b,a) ).
The arguments are two objects a, b. The output is the coclosed right evaluation morphism \mathrm{coclev}_{a,b}: b \rightarrow a \otimes \mathrm{\underline{coHom}}(b,a), i.e., the unit of the cohom tensor adjunction.
‣ CoclosedMonoidalRightEvaluationMorphismWithGivenRange ( a, b, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( b, r ).
The arguments are two objects a,b and an object r = a \otimes \mathrm{\underline{coHom}}(b,a). The output is the coclosed right evaluation morphism \mathrm{coclev}_{a,b}: b \rightarrow a \otimes \mathrm{\underline{coHom}}(b,a), i.e., the unit of the cohom tensor adjunction.
‣ CoclosedMonoidalRightCoevaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{coHom}}(a \otimes b, a), b ).
The arguments are two objects a,b. The output is the coclosed right coevaluation morphism \mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}}(a \otimes b, a) \rightarrow b, i.e., the counit of the cohom tensor adjunction.
‣ CoclosedMonoidalRightCoevaluationMorphismWithGivenSource ( a, b, s ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, b ).
The arguments are two objects a,b and an object s = \mathrm{\underline{coHom}}(a \otimes b, a). The output is the coclosed right coevaluation morphism \mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}}(a \otimes b, a) \rightarrow b, i.e., the unit of the cohom tensor adjunction.
‣ TensorProductToInternalCoHomRightAdjunctMorphism ( b, c, g ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{coHom}}(a,b), c ).
The arguments are two objects b,c and a morphism g: a \rightarrow b \otimes c. The output is a morphism f: \mathrm{\underline{coHom}}(a,b) \rightarrow c corresponding to g under the cohom tensor adjunction.
‣ TensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom ( b, c, g, i ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( i, c ).
The arguments are two objects b,c, a morphism g: a \rightarrow b \otimes c 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.
‣ InternalCoHomToTensorProductRightAdjunctMorphism ( a, b, f ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}(a, b \otimes c).
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 b \otimes c corresponding to f under the cohom tensor adjunction.
‣ InternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct ( a, b, f, t ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( a, t ).
The arguments are two objects a,b, a morphism f: \mathrm{\underline{coHom}}(a,b) \rightarrow c and an object t = b \otimes c. The output is a morphism g: a \rightarrow t corresponding to f under the cohom tensor adjunction.
‣ CoclosedMonoidalLeftEvaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( b, \mathrm{\underline{coHom}}(b,a) \otimes a ).
The arguments are two objects a, b. The output is the coclosed left evaluation morphism \mathrm{coclev}_{a,b}: b \rightarrow \mathrm{\underline{coHom}}(b,a) \otimes a, i.e., the unit of the cohom tensor adjunction.
‣ CoclosedMonoidalLeftEvaluationMorphismWithGivenRange ( a, b, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( b, r ).
The arguments are two objects a,b and an object r = \mathrm{\underline{coHom}}(b,a) \otimes a. The output is the coclosed left evaluation morphism \mathrm{coclev}_{a,b}: b \rightarrow \mathrm{\underline{coHom}}(b,a) \otimes a, i.e., the unit of the cohom tensor adjunction.
‣ CoclosedMonoidalLeftCoevaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{coHom}}(b \otimes a, a), b ).
The arguments are two objects a,b. The output is the coclosed left coevaluation morphism \mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}}(b \otimes a, a) \rightarrow b, i.e., the counit of the cohom tensor adjunction.
‣ CoclosedMonoidalLeftCoevaluationMorphismWithGivenSource ( a, b, s ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, b ).
The arguments are two objects a,b and an object s = \mathrm{\underline{coHom}}(b \otimes a, a). The output is the coclosed left coevaluation morphism \mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}}(b \otimes a, a) \rightarrow b, i.e., the unit of the cohom tensor adjunction.
‣ TensorProductToInternalCoHomLeftAdjunctMorphism ( b, c, g ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( \mathrm{\underline{coHom}}(a,c), b ).
The arguments are two objects b,c and a morphism g: a \rightarrow b \otimes c. The output is a morphism f: \mathrm{\underline{coHom}}(a,c) \rightarrow b corresponding to g under the cohom tensor adjunction.
‣ TensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom ( b, c, g, i ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( i, b ).
The arguments are two objects b,c, a morphism g: a \rightarrow b \otimes c and an object i = \mathrm{\underline{coHom}}(a,c). The output is a morphism f: \mathrm{\underline{coHom}}(a,c) \rightarrow b corresponding to g under the cohom tensor adjunction.
‣ InternalCoHomToTensorProductLeftAdjunctMorphism ( a, c, f ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}(a, b \otimes c).
The arguments are two objects a,c and a morphism f: \mathrm{\underline{coHom}}(a,c) \rightarrow b. The output is a morphism g: a \rightarrow b \otimes c corresponding to f under the cohom tensor adjunction.
‣ InternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct ( a, c, f, t ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( a, t ).
The arguments are two objects a,c, a morphism f: \mathrm{\underline{coHom}}(a,c) \rightarrow b and an object t = b \otimes c. The output is a morphism g: a \rightarrow t 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{MonoidalPreCoComposeMorphism}_{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}( s, r ).
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{MonoidalPostCoComposeMorphism}_{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}( s, r ).
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}( s, r ).
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}( s, r ).
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}(s, 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{InternalCoHomTensorProductCompatibilityMorphism}_{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}( s, r ).
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{CoDualityTensorProductCompatibilityMorphism}: (a \otimes b)_{\vee} \rightarrow a_{\vee} \otimes b_{\vee}.
‣ CoDualityTensorProductCompatibilityMorphismWithGivenObjects ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
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{MorphismFromInternalCoHomToTensorProduct}_{a,b}: \mathrm{\underline{coHom}}(a,b) \rightarrow b_{\vee} \otimes a.
‣ MorphismFromInternalCoHomToTensorProductWithGivenObjects ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \mathrm{Hom}( s, r ).
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, r).
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}(s, 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}_\ell}(a, a') \otimes \mathrm{\underline{Hom}_\ell}(b, b') \rightarrow \mathrm{\underline{Hom}_\ell}(a \otimes b, a' \otimes b') is an isomorphism,
the natural morphism
a \rightarrow \mathrm{\underline{Hom}_\ell}(\mathrm{\underline{Hom}_\ell}(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}_\ell}(a,b) \coloneqq a^\vee \otimes b and, in particular, \mathrm{\underline{Hom}_\ell}(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.
‣ LeftInternalHom ( 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}_\ell}(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.
‣ LeftInternalCoHom ( 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}_\ell}(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 ) |
‣ AddLeftDistributivityExpanding ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, L ) \mapsto \mathtt{LeftDistributivityExpanding}(a, L).
‣ AddLeftDistributivityExpandingWithGivenObjects ( C, F ) | ( operation ) |
‣ AddLeftDistributivityExpandingWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, L, r ) \mapsto \mathtt{LeftDistributivityExpandingWithGivenObjects}(s, a, L, r).
‣ AddLeftDistributivityFactoring ( C, F ) | ( operation ) |
‣ AddLeftDistributivityFactoring ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, L ) \mapsto \mathtt{LeftDistributivityFactoring}(a, L).
‣ AddLeftDistributivityFactoringWithGivenObjects ( C, F ) | ( operation ) |
‣ AddLeftDistributivityFactoringWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, L, r ) \mapsto \mathtt{LeftDistributivityFactoringWithGivenObjects}(s, a, L, r).
‣ AddRightDistributivityExpanding ( C, F ) | ( operation ) |
‣ AddRightDistributivityExpanding ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( L, a ) \mapsto \mathtt{RightDistributivityExpanding}(L, a).
‣ AddRightDistributivityExpandingWithGivenObjects ( C, F ) | ( operation ) |
‣ AddRightDistributivityExpandingWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, L, a, r ) \mapsto \mathtt{RightDistributivityExpandingWithGivenObjects}(s, L, a, r).
‣ AddRightDistributivityFactoring ( C, F ) | ( operation ) |
‣ AddRightDistributivityFactoring ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( L, a ) \mapsto \mathtt{RightDistributivityFactoring}(L, a).
‣ AddRightDistributivityFactoringWithGivenObjects ( C, F ) | ( operation ) |
‣ AddRightDistributivityFactoringWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, L, a, r ) \mapsto \mathtt{RightDistributivityFactoringWithGivenObjects}(s, L, a, r).
‣ AddBraiding ( C, F ) | ( operation ) |
‣ AddBraiding ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{Braiding}(a, b).
‣ AddBraidingInverse ( C, F ) | ( operation ) |
‣ AddBraidingInverse ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{BraidingInverse}(a, b).
‣ AddBraidingInverseWithGivenTensorProducts ( C, F ) | ( operation ) |
‣ AddBraidingInverseWithGivenTensorProducts ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{BraidingInverseWithGivenTensorProducts}(s, a, b, r).
‣ AddBraidingWithGivenTensorProducts ( C, F ) | ( operation ) |
‣ AddBraidingWithGivenTensorProducts ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{BraidingWithGivenTensorProducts}(s, a, b, r).
‣ AddClosedMonoidalLeftCoevaluationMorphism ( C, F ) | ( operation ) |
‣ AddClosedMonoidalLeftCoevaluationMorphism ( C, F, weight ) | ( 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 ClosedMonoidalLeftCoevaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{ClosedMonoidalLeftCoevaluationMorphism}(a, b).
‣ AddClosedMonoidalLeftCoevaluationMorphismWithGivenRange ( C, F ) | ( operation ) |
‣ AddClosedMonoidalLeftCoevaluationMorphismWithGivenRange ( C, F, weight ) | ( 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 ClosedMonoidalLeftCoevaluationMorphismWithGivenRange
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, r ) \mapsto \mathtt{ClosedMonoidalLeftCoevaluationMorphismWithGivenRange}(a, b, r).
‣ AddClosedMonoidalLeftEvaluationMorphism ( C, F ) | ( operation ) |
‣ AddClosedMonoidalLeftEvaluationMorphism ( C, F, weight ) | ( 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 ClosedMonoidalLeftEvaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{ClosedMonoidalLeftEvaluationMorphism}(a, b).
‣ AddClosedMonoidalLeftEvaluationMorphismWithGivenSource ( C, F ) | ( operation ) |
‣ AddClosedMonoidalLeftEvaluationMorphismWithGivenSource ( C, F, weight ) | ( 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 ClosedMonoidalLeftEvaluationMorphismWithGivenSource
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, s ) \mapsto \mathtt{ClosedMonoidalLeftEvaluationMorphismWithGivenSource}(a, b, s).
‣ AddClosedMonoidalRightCoevaluationMorphism ( C, F ) | ( operation ) |
‣ AddClosedMonoidalRightCoevaluationMorphism ( C, F, weight ) | ( 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 ClosedMonoidalRightCoevaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{ClosedMonoidalRightCoevaluationMorphism}(a, b).
‣ AddClosedMonoidalRightCoevaluationMorphismWithGivenRange ( C, F ) | ( operation ) |
‣ AddClosedMonoidalRightCoevaluationMorphismWithGivenRange ( C, F, weight ) | ( 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 ClosedMonoidalRightCoevaluationMorphismWithGivenRange
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, r ) \mapsto \mathtt{ClosedMonoidalRightCoevaluationMorphismWithGivenRange}(a, b, r).
‣ AddClosedMonoidalRightEvaluationMorphism ( C, F ) | ( operation ) |
‣ AddClosedMonoidalRightEvaluationMorphism ( C, F, weight ) | ( 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 ClosedMonoidalRightEvaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{ClosedMonoidalRightEvaluationMorphism}(a, b).
‣ AddClosedMonoidalRightEvaluationMorphismWithGivenSource ( C, F ) | ( operation ) |
‣ AddClosedMonoidalRightEvaluationMorphismWithGivenSource ( C, F, weight ) | ( 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 ClosedMonoidalRightEvaluationMorphismWithGivenSource
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, s ) \mapsto \mathtt{ClosedMonoidalRightEvaluationMorphismWithGivenSource}(a, b, s).
‣ AddDualOnMorphisms ( C, F ) | ( operation ) |
‣ AddDualOnMorphisms ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{DualOnMorphisms}(alpha).
‣ AddDualOnMorphismsWithGivenDuals ( C, F ) | ( operation ) |
‣ AddDualOnMorphismsWithGivenDuals ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, r ) \mapsto \mathtt{DualOnMorphismsWithGivenDuals}(s, alpha, r).
‣ AddDualOnObjects ( C, F ) | ( operation ) |
‣ AddDualOnObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{DualOnObjects}(a).
‣ AddEvaluationForDual ( C, F ) | ( operation ) |
‣ AddEvaluationForDual ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{EvaluationForDual}(a).
‣ AddEvaluationForDualWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddEvaluationForDualWithGivenTensorProduct ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, r ) \mapsto \mathtt{EvaluationForDualWithGivenTensorProduct}(s, a, r).
‣ AddInternalHomOnMorphisms ( C, F ) | ( operation ) |
‣ AddInternalHomOnMorphisms ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha, beta ) \mapsto \mathtt{InternalHomOnMorphisms}(alpha, beta).
‣ AddInternalHomOnMorphismsWithGivenInternalHoms ( C, F ) | ( operation ) |
‣ AddInternalHomOnMorphismsWithGivenInternalHoms ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, beta, r ) \mapsto \mathtt{InternalHomOnMorphismsWithGivenInternalHoms}(s, alpha, beta, r).
‣ AddInternalHomOnObjects ( C, F ) | ( operation ) |
‣ AddInternalHomOnObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{InternalHomOnObjects}(a, b).
‣ AddInternalHomToTensorProductLeftAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductLeftAdjunctMorphism ( C, F, weight ) | ( 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 InternalHomToTensorProductLeftAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g ) \mapsto \mathtt{InternalHomToTensorProductLeftAdjunctMorphism}(b, c, g).
‣ AddInternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct ( C, F, weight ) | ( 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 InternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g, s ) \mapsto \mathtt{InternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct}(b, c, g, s).
‣ AddInternalHomToTensorProductLeftAdjunctionIsomorphism ( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductLeftAdjunctionIsomorphism ( C, F, weight ) | ( 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 InternalHomToTensorProductLeftAdjunctionIsomorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{InternalHomToTensorProductLeftAdjunctionIsomorphism}(a, b, c).
‣ AddInternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects ( C, F, weight ) | ( 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 InternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{InternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r).
‣ AddInternalHomToTensorProductRightAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductRightAdjunctMorphism ( C, F, weight ) | ( 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 InternalHomToTensorProductRightAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, c, g ) \mapsto \mathtt{InternalHomToTensorProductRightAdjunctMorphism}(a, c, g).
‣ AddInternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct ( C, F, weight ) | ( 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 InternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, c, g, s ) \mapsto \mathtt{InternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct}(a, c, g, s).
‣ AddInternalHomToTensorProductRightAdjunctionIsomorphism ( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductRightAdjunctionIsomorphism ( C, F, weight ) | ( 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 InternalHomToTensorProductRightAdjunctionIsomorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{InternalHomToTensorProductRightAdjunctionIsomorphism}(a, b, c).
‣ AddInternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects ( C, F, weight ) | ( 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 InternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{InternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r).
‣ AddIsomorphismFromDualObjectToInternalHomIntoTensorUnit ( C, F ) | ( operation ) |
‣ AddIsomorphismFromDualObjectToInternalHomIntoTensorUnit ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromDualObjectToInternalHomIntoTensorUnit}(a).
‣ AddIsomorphismFromInternalHomIntoTensorUnitToDualObject ( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalHomIntoTensorUnitToDualObject ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromInternalHomIntoTensorUnitToDualObject}(a).
‣ AddIsomorphismFromInternalHomToObject ( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalHomToObject ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromInternalHomToObject}(a).
‣ AddIsomorphismFromInternalHomToObjectWithGivenInternalHom ( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalHomToObjectWithGivenInternalHom ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{IsomorphismFromInternalHomToObjectWithGivenInternalHom}(a, s).
‣ AddIsomorphismFromObjectToInternalHom ( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToInternalHom ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToInternalHom}(a).
‣ AddIsomorphismFromObjectToInternalHomWithGivenInternalHom ( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToInternalHomWithGivenInternalHom ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToInternalHomWithGivenInternalHom}(a, r).
‣ AddLambdaElimination ( C, F ) | ( operation ) |
‣ AddLambdaElimination ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, alpha ) \mapsto \mathtt{LambdaElimination}(a, b, alpha).
‣ AddLambdaIntroduction ( C, F ) | ( operation ) |
‣ AddLambdaIntroduction ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{LambdaIntroduction}(alpha).
‣ AddMonoidalPostComposeMorphism ( C, F ) | ( operation ) |
‣ AddMonoidalPostComposeMorphism ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{MonoidalPostComposeMorphism}(a, b, c).
‣ AddMonoidalPostComposeMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddMonoidalPostComposeMorphismWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPostComposeMorphismWithGivenObjects}(s, a, b, c, r).
‣ AddMonoidalPreComposeMorphism ( C, F ) | ( operation ) |
‣ AddMonoidalPreComposeMorphism ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{MonoidalPreComposeMorphism}(a, b, c).
‣ AddMonoidalPreComposeMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddMonoidalPreComposeMorphismWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPreComposeMorphismWithGivenObjects}(s, a, b, c, r).
‣ AddMorphismFromTensorProductToInternalHom ( C, F ) | ( operation ) |
‣ AddMorphismFromTensorProductToInternalHom ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{MorphismFromTensorProductToInternalHom}(a, b).
‣ AddMorphismFromTensorProductToInternalHomWithGivenObjects ( C, F ) | ( operation ) |
‣ AddMorphismFromTensorProductToInternalHomWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromTensorProductToInternalHomWithGivenObjects}(s, a, b, r).
‣ AddMorphismToBidual ( C, F ) | ( operation ) |
‣ AddMorphismToBidual ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{MorphismToBidual}(a).
‣ AddMorphismToBidualWithGivenBidual ( C, F ) | ( operation ) |
‣ AddMorphismToBidualWithGivenBidual ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{MorphismToBidualWithGivenBidual}(a, r).
‣ AddTensorProductDualityCompatibilityMorphism ( C, F ) | ( operation ) |
‣ AddTensorProductDualityCompatibilityMorphism ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{TensorProductDualityCompatibilityMorphism}(a, b).
‣ AddTensorProductDualityCompatibilityMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddTensorProductDualityCompatibilityMorphismWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{TensorProductDualityCompatibilityMorphismWithGivenObjects}(s, a, b, r).
‣ AddTensorProductInternalHomCompatibilityMorphism ( C, F ) | ( operation ) |
‣ AddTensorProductInternalHomCompatibilityMorphism ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( list ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphism}(list).
‣ AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( source, list, range ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphismWithGivenObjects}(source, list, range).
‣ AddTensorProductToInternalHomLeftAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomLeftAdjunctMorphism ( C, F, weight ) | ( 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 TensorProductToInternalHomLeftAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f ) \mapsto \mathtt{TensorProductToInternalHomLeftAdjunctMorphism}(a, b, f).
‣ AddTensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom ( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom ( C, F, weight ) | ( 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 TensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f, i ) \mapsto \mathtt{TensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom}(a, b, f, i).
‣ AddTensorProductToInternalHomLeftAdjunctionIsomorphism ( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomLeftAdjunctionIsomorphism ( C, F, weight ) | ( 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 TensorProductToInternalHomLeftAdjunctionIsomorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{TensorProductToInternalHomLeftAdjunctionIsomorphism}(a, b, c).
‣ AddTensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects ( C, F, weight ) | ( 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 TensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{TensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r).
‣ AddTensorProductToInternalHomRightAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomRightAdjunctMorphism ( C, F, weight ) | ( 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 TensorProductToInternalHomRightAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f ) \mapsto \mathtt{TensorProductToInternalHomRightAdjunctMorphism}(a, b, f).
‣ AddTensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom ( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom ( C, F, weight ) | ( 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 TensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f, i ) \mapsto \mathtt{TensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom}(a, b, f, i).
‣ AddTensorProductToInternalHomRightAdjunctionIsomorphism ( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomRightAdjunctionIsomorphism ( C, F, weight ) | ( 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 TensorProductToInternalHomRightAdjunctionIsomorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{TensorProductToInternalHomRightAdjunctionIsomorphism}(a, b, c).
‣ AddTensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects ( C, F, weight ) | ( 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 TensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{TensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r).
‣ AddUniversalPropertyOfDual ( C, F ) | ( operation ) |
‣ AddUniversalPropertyOfDual ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfDual}(t, a, alpha).
‣ AddCoDualOnMorphisms ( C, F ) | ( operation ) |
‣ AddCoDualOnMorphisms ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{CoDualOnMorphisms}(alpha).
‣ AddCoDualOnMorphismsWithGivenCoDuals ( C, F ) | ( operation ) |
‣ AddCoDualOnMorphismsWithGivenCoDuals ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, r ) \mapsto \mathtt{CoDualOnMorphismsWithGivenCoDuals}(s, alpha, r).
‣ AddCoDualOnObjects ( C, F ) | ( operation ) |
‣ AddCoDualOnObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{CoDualOnObjects}(a).
‣ AddCoDualityTensorProductCompatibilityMorphism ( C, F ) | ( operation ) |
‣ AddCoDualityTensorProductCompatibilityMorphism ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{CoDualityTensorProductCompatibilityMorphism}(a, b).
‣ AddCoDualityTensorProductCompatibilityMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddCoDualityTensorProductCompatibilityMorphismWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{CoDualityTensorProductCompatibilityMorphismWithGivenObjects}(s, a, b, r).
‣ AddCoLambdaElimination ( C, F ) | ( operation ) |
‣ AddCoLambdaElimination ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, alpha ) \mapsto \mathtt{CoLambdaElimination}(a, b, alpha).
‣ AddCoLambdaIntroduction ( C, F ) | ( operation ) |
‣ AddCoLambdaIntroduction ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{CoLambdaIntroduction}(alpha).
‣ AddCoclosedEvaluationForCoDual ( C, F ) | ( operation ) |
‣ AddCoclosedEvaluationForCoDual ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{CoclosedEvaluationForCoDual}(a).
‣ AddCoclosedEvaluationForCoDualWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddCoclosedEvaluationForCoDualWithGivenTensorProduct ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, r ) \mapsto \mathtt{CoclosedEvaluationForCoDualWithGivenTensorProduct}(s, a, r).
‣ AddCoclosedMonoidalLeftCoevaluationMorphism ( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalLeftCoevaluationMorphism ( C, F, weight ) | ( 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 CoclosedMonoidalLeftCoevaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{CoclosedMonoidalLeftCoevaluationMorphism}(a, b).
‣ AddCoclosedMonoidalLeftCoevaluationMorphismWithGivenSource ( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalLeftCoevaluationMorphismWithGivenSource ( C, F, weight ) | ( 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 CoclosedMonoidalLeftCoevaluationMorphismWithGivenSource
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, s ) \mapsto \mathtt{CoclosedMonoidalLeftCoevaluationMorphismWithGivenSource}(a, b, s).
‣ AddCoclosedMonoidalLeftEvaluationMorphism ( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalLeftEvaluationMorphism ( C, F, weight ) | ( 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 CoclosedMonoidalLeftEvaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{CoclosedMonoidalLeftEvaluationMorphism}(a, b).
‣ AddCoclosedMonoidalLeftEvaluationMorphismWithGivenRange ( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalLeftEvaluationMorphismWithGivenRange ( C, F, weight ) | ( 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 CoclosedMonoidalLeftEvaluationMorphismWithGivenRange
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, r ) \mapsto \mathtt{CoclosedMonoidalLeftEvaluationMorphismWithGivenRange}(a, b, r).
‣ AddCoclosedMonoidalRightCoevaluationMorphism ( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalRightCoevaluationMorphism ( C, F, weight ) | ( 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 CoclosedMonoidalRightCoevaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{CoclosedMonoidalRightCoevaluationMorphism}(a, b).
‣ AddCoclosedMonoidalRightCoevaluationMorphismWithGivenSource ( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalRightCoevaluationMorphismWithGivenSource ( C, F, weight ) | ( 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 CoclosedMonoidalRightCoevaluationMorphismWithGivenSource
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, s ) \mapsto \mathtt{CoclosedMonoidalRightCoevaluationMorphismWithGivenSource}(a, b, s).
‣ AddCoclosedMonoidalRightEvaluationMorphism ( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalRightEvaluationMorphism ( C, F, weight ) | ( 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 CoclosedMonoidalRightEvaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{CoclosedMonoidalRightEvaluationMorphism}(a, b).
‣ AddCoclosedMonoidalRightEvaluationMorphismWithGivenRange ( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalRightEvaluationMorphismWithGivenRange ( C, F, weight ) | ( 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 CoclosedMonoidalRightEvaluationMorphismWithGivenRange
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, r ) \mapsto \mathtt{CoclosedMonoidalRightEvaluationMorphismWithGivenRange}(a, b, r).
‣ AddInternalCoHomOnMorphisms ( C, F ) | ( operation ) |
‣ AddInternalCoHomOnMorphisms ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha, beta ) \mapsto \mathtt{InternalCoHomOnMorphisms}(alpha, beta).
‣ AddInternalCoHomOnMorphismsWithGivenInternalCoHoms ( C, F ) | ( operation ) |
‣ AddInternalCoHomOnMorphismsWithGivenInternalCoHoms ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, beta, r ) \mapsto \mathtt{InternalCoHomOnMorphismsWithGivenInternalCoHoms}(s, alpha, beta, r).
‣ AddInternalCoHomOnObjects ( C, F ) | ( operation ) |
‣ AddInternalCoHomOnObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{InternalCoHomOnObjects}(a, b).
‣ AddInternalCoHomTensorProductCompatibilityMorphism ( C, F ) | ( operation ) |
‣ AddInternalCoHomTensorProductCompatibilityMorphism ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( list ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphism}(list).
‣ AddInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( source, list, range ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}(source, list, range).
‣ AddInternalCoHomToTensorProductLeftAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddInternalCoHomToTensorProductLeftAdjunctMorphism ( C, F, weight ) | ( 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 InternalCoHomToTensorProductLeftAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, c, f ) \mapsto \mathtt{InternalCoHomToTensorProductLeftAdjunctMorphism}(a, c, f).
‣ AddInternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddInternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct ( C, F, weight ) | ( 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 InternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, c, f, t ) \mapsto \mathtt{InternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct}(a, c, f, t).
‣ AddInternalCoHomToTensorProductRightAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddInternalCoHomToTensorProductRightAdjunctMorphism ( C, F, weight ) | ( 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 InternalCoHomToTensorProductRightAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f ) \mapsto \mathtt{InternalCoHomToTensorProductRightAdjunctMorphism}(a, b, f).
‣ AddInternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddInternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct ( C, F, weight ) | ( 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 InternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f, t ) \mapsto \mathtt{InternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct}(a, b, f, t).
‣ AddIsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit ( C, F ) | ( operation ) |
‣ AddIsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit}(a).
‣ AddIsomorphismFromInternalCoHomFromTensorUnitToCoDualObject ( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalCoHomFromTensorUnitToCoDualObject ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject}(a).
‣ AddIsomorphismFromInternalCoHomToObject ( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalCoHomToObject ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromInternalCoHomToObject}(a).
‣ AddIsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom ( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom}(a, s).
‣ AddIsomorphismFromObjectToInternalCoHom ( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToInternalCoHom ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToInternalCoHom}(a).
‣ AddIsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom ( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom}(a, r).
‣ AddMonoidalPostCoComposeMorphism ( C, F ) | ( operation ) |
‣ AddMonoidalPostCoComposeMorphism ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{MonoidalPostCoComposeMorphism}(a, b, c).
‣ AddMonoidalPostCoComposeMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddMonoidalPostCoComposeMorphismWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPostCoComposeMorphismWithGivenObjects}(s, a, b, c, r).
‣ AddMonoidalPreCoComposeMorphism ( C, F ) | ( operation ) |
‣ AddMonoidalPreCoComposeMorphism ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{MonoidalPreCoComposeMorphism}(a, b, c).
‣ AddMonoidalPreCoComposeMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddMonoidalPreCoComposeMorphismWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPreCoComposeMorphismWithGivenObjects}(s, a, b, c, r).
‣ AddMorphismFromCoBidual ( C, F ) | ( operation ) |
‣ AddMorphismFromCoBidual ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{MorphismFromCoBidual}(a).
‣ AddMorphismFromCoBidualWithGivenCoBidual ( C, F ) | ( operation ) |
‣ AddMorphismFromCoBidualWithGivenCoBidual ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{MorphismFromCoBidualWithGivenCoBidual}(a, s).
‣ AddMorphismFromInternalCoHomToTensorProduct ( C, F ) | ( operation ) |
‣ AddMorphismFromInternalCoHomToTensorProduct ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{MorphismFromInternalCoHomToTensorProduct}(a, b).
‣ AddMorphismFromInternalCoHomToTensorProductWithGivenObjects ( C, F ) | ( operation ) |
‣ AddMorphismFromInternalCoHomToTensorProductWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromInternalCoHomToTensorProductWithGivenObjects}(s, a, b, r).
‣ AddTensorProductToInternalCoHomLeftAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddTensorProductToInternalCoHomLeftAdjunctMorphism ( C, F, weight ) | ( 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 TensorProductToInternalCoHomLeftAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g ) \mapsto \mathtt{TensorProductToInternalCoHomLeftAdjunctMorphism}(b, c, g).
‣ AddTensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom ( C, F ) | ( operation ) |
‣ AddTensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom ( C, F, weight ) | ( 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 TensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g, i ) \mapsto \mathtt{TensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom}(b, c, g, i).
‣ AddTensorProductToInternalCoHomRightAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddTensorProductToInternalCoHomRightAdjunctMorphism ( C, F, weight ) | ( 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 TensorProductToInternalCoHomRightAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g ) \mapsto \mathtt{TensorProductToInternalCoHomRightAdjunctMorphism}(b, c, g).
‣ AddTensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom ( C, F ) | ( operation ) |
‣ AddTensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom ( C, F, weight ) | ( 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 TensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g, i ) \mapsto \mathtt{TensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom}(b, c, g, i).
‣ AddUniversalPropertyOfCoDual ( C, F ) | ( operation ) |
‣ AddUniversalPropertyOfCoDual ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfCoDual}(t, a, alpha).
‣ AddIsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit ( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit ( C, F, weight ) | ( 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 IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit}(a).
‣ AddIsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject ( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject ( C, F, weight ) | ( 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 IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject}(a).
‣ AddIsomorphismFromLeftInternalHomToObject ( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftInternalHomToObject ( C, F, weight ) | ( 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 IsomorphismFromLeftInternalHomToObject
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromLeftInternalHomToObject}(a).
‣ AddIsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom ( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom ( C, F, weight ) | ( 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 IsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{IsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom}(a, s).
‣ AddIsomorphismFromObjectToLeftInternalHom ( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToLeftInternalHom ( C, F, weight ) | ( 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 IsomorphismFromObjectToLeftInternalHom
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToLeftInternalHom}(a).
‣ AddIsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom ( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom ( C, F, weight ) | ( 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 IsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom}(a, r).
‣ AddLeftClosedMonoidalCoevaluationMorphism ( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalCoevaluationMorphism ( C, F, weight ) | ( 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 LeftClosedMonoidalCoevaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{LeftClosedMonoidalCoevaluationMorphism}(a, b).
‣ AddLeftClosedMonoidalCoevaluationMorphismWithGivenRange ( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalCoevaluationMorphismWithGivenRange ( C, F, weight ) | ( 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 LeftClosedMonoidalCoevaluationMorphismWithGivenRange
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, r ) \mapsto \mathtt{LeftClosedMonoidalCoevaluationMorphismWithGivenRange}(a, b, r).
‣ AddLeftClosedMonoidalEvaluationForLeftDual ( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalEvaluationForLeftDual ( C, F, weight ) | ( 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 LeftClosedMonoidalEvaluationForLeftDual
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{LeftClosedMonoidalEvaluationForLeftDual}(a).
‣ AddLeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct ( C, F, weight ) | ( 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 LeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, r ) \mapsto \mathtt{LeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct}(s, a, r).
‣ AddLeftClosedMonoidalEvaluationMorphism ( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalEvaluationMorphism ( C, F, weight ) | ( 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 LeftClosedMonoidalEvaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{LeftClosedMonoidalEvaluationMorphism}(a, b).
‣ AddLeftClosedMonoidalEvaluationMorphismWithGivenSource ( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalEvaluationMorphismWithGivenSource ( C, F, weight ) | ( 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 LeftClosedMonoidalEvaluationMorphismWithGivenSource
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, s ) \mapsto \mathtt{LeftClosedMonoidalEvaluationMorphismWithGivenSource}(a, b, s).
‣ AddLeftClosedMonoidalLambdaElimination ( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalLambdaElimination ( C, F, weight ) | ( 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 LeftClosedMonoidalLambdaElimination
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, alpha ) \mapsto \mathtt{LeftClosedMonoidalLambdaElimination}(a, b, alpha).
‣ AddLeftClosedMonoidalLambdaIntroduction ( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalLambdaIntroduction ( C, F, weight ) | ( 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 LeftClosedMonoidalLambdaIntroduction
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{LeftClosedMonoidalLambdaIntroduction}(alpha).
‣ AddLeftClosedMonoidalPostComposeMorphism ( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalPostComposeMorphism ( C, F, weight ) | ( 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 LeftClosedMonoidalPostComposeMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{LeftClosedMonoidalPostComposeMorphism}(a, b, c).
‣ AddLeftClosedMonoidalPostComposeMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalPostComposeMorphismWithGivenObjects ( C, F, weight ) | ( 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 LeftClosedMonoidalPostComposeMorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{LeftClosedMonoidalPostComposeMorphismWithGivenObjects}(s, a, b, c, r).
‣ AddLeftClosedMonoidalPreComposeMorphism ( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalPreComposeMorphism ( C, F, weight ) | ( 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 LeftClosedMonoidalPreComposeMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{LeftClosedMonoidalPreComposeMorphism}(a, b, c).
‣ AddLeftClosedMonoidalPreComposeMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalPreComposeMorphismWithGivenObjects ( C, F, weight ) | ( 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 LeftClosedMonoidalPreComposeMorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{LeftClosedMonoidalPreComposeMorphismWithGivenObjects}(s, a, b, c, r).
‣ AddLeftDualOnMorphisms ( C, F ) | ( operation ) |
‣ AddLeftDualOnMorphisms ( C, F, weight ) | ( 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 LeftDualOnMorphisms
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{LeftDualOnMorphisms}(alpha).
‣ AddLeftDualOnMorphismsWithGivenLeftDuals ( C, F ) | ( operation ) |
‣ AddLeftDualOnMorphismsWithGivenLeftDuals ( C, F, weight ) | ( 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 LeftDualOnMorphismsWithGivenLeftDuals
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, r ) \mapsto \mathtt{LeftDualOnMorphismsWithGivenLeftDuals}(s, alpha, r).
‣ AddLeftDualOnObjects ( C, F ) | ( operation ) |
‣ AddLeftDualOnObjects ( C, F, weight ) | ( 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 LeftDualOnObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{LeftDualOnObjects}(a).
‣ AddLeftInternalHomOnMorphisms ( C, F ) | ( operation ) |
‣ AddLeftInternalHomOnMorphisms ( C, F, weight ) | ( 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 LeftInternalHomOnMorphisms
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha, beta ) \mapsto \mathtt{LeftInternalHomOnMorphisms}(alpha, beta).
‣ AddLeftInternalHomOnMorphismsWithGivenLeftInternalHoms ( C, F ) | ( operation ) |
‣ AddLeftInternalHomOnMorphismsWithGivenLeftInternalHoms ( C, F, weight ) | ( 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 LeftInternalHomOnMorphismsWithGivenLeftInternalHoms
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, beta, r ) \mapsto \mathtt{LeftInternalHomOnMorphismsWithGivenLeftInternalHoms}(s, alpha, beta, r).
‣ AddLeftInternalHomOnObjects ( C, F ) | ( operation ) |
‣ AddLeftInternalHomOnObjects ( C, F, weight ) | ( 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 LeftInternalHomOnObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{LeftInternalHomOnObjects}(a, b).
‣ AddLeftInternalHomToTensorProductAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddLeftInternalHomToTensorProductAdjunctMorphism ( C, F, weight ) | ( 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 LeftInternalHomToTensorProductAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g ) \mapsto \mathtt{LeftInternalHomToTensorProductAdjunctMorphism}(b, c, g).
‣ AddLeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddLeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct ( C, F, weight ) | ( 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 LeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g, t ) \mapsto \mathtt{LeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct}(b, c, g, t).
‣ AddMorphismFromTensorProductToLeftInternalHom ( C, F ) | ( operation ) |
‣ AddMorphismFromTensorProductToLeftInternalHom ( C, F, weight ) | ( 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 MorphismFromTensorProductToLeftInternalHom
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{MorphismFromTensorProductToLeftInternalHom}(a, b).
‣ AddMorphismFromTensorProductToLeftInternalHomWithGivenObjects ( C, F ) | ( operation ) |
‣ AddMorphismFromTensorProductToLeftInternalHomWithGivenObjects ( C, F, weight ) | ( 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 MorphismFromTensorProductToLeftInternalHomWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromTensorProductToLeftInternalHomWithGivenObjects}(s, a, b, r).
‣ AddMorphismToLeftBidual ( C, F ) | ( operation ) |
‣ AddMorphismToLeftBidual ( C, F, weight ) | ( 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 MorphismToLeftBidual
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{MorphismToLeftBidual}(a).
‣ AddMorphismToLeftBidualWithGivenLeftBidual ( C, F ) | ( operation ) |
‣ AddMorphismToLeftBidualWithGivenLeftBidual ( C, F, weight ) | ( 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 MorphismToLeftBidualWithGivenLeftBidual
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{MorphismToLeftBidualWithGivenLeftBidual}(a, r).
‣ AddTensorProductLeftDualityCompatibilityMorphism ( C, F ) | ( operation ) |
‣ AddTensorProductLeftDualityCompatibilityMorphism ( C, F, weight ) | ( 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 TensorProductLeftDualityCompatibilityMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{TensorProductLeftDualityCompatibilityMorphism}(a, b).
‣ AddTensorProductLeftDualityCompatibilityMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddTensorProductLeftDualityCompatibilityMorphismWithGivenObjects ( C, F, weight ) | ( 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 TensorProductLeftDualityCompatibilityMorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{TensorProductLeftDualityCompatibilityMorphismWithGivenObjects}(s, a, b, r).
‣ AddTensorProductLeftInternalHomCompatibilityMorphism ( C, F ) | ( operation ) |
‣ AddTensorProductLeftInternalHomCompatibilityMorphism ( C, F, weight ) | ( 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 TensorProductLeftInternalHomCompatibilityMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( list ) \mapsto \mathtt{TensorProductLeftInternalHomCompatibilityMorphism}(list).
‣ AddTensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddTensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects ( C, F, weight ) | ( 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 TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( source, list, range ) \mapsto \mathtt{TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects}(source, list, range).
‣ AddTensorProductToLeftInternalHomAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddTensorProductToLeftInternalHomAdjunctMorphism ( C, F, weight ) | ( 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 TensorProductToLeftInternalHomAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f ) \mapsto \mathtt{TensorProductToLeftInternalHomAdjunctMorphism}(a, b, f).
‣ AddTensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom ( C, F ) | ( operation ) |
‣ AddTensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom ( C, F, weight ) | ( 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 TensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f, i ) \mapsto \mathtt{TensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom}(a, b, f, i).
‣ AddUniversalPropertyOfLeftDual ( C, F ) | ( operation ) |
‣ AddUniversalPropertyOfLeftDual ( C, F, weight ) | ( 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 UniversalPropertyOfLeftDual
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfLeftDual}(t, a, alpha).
‣ AddIsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit ( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit ( C, F, weight ) | ( 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 IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit}(a).
‣ AddIsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject ( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject ( C, F, weight ) | ( 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 IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject}(a).
‣ AddIsomorphismFromLeftInternalCoHomToObject ( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftInternalCoHomToObject ( C, F, weight ) | ( 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 IsomorphismFromLeftInternalCoHomToObject
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromLeftInternalCoHomToObject}(a).
‣ AddIsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom ( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom ( C, F, weight ) | ( 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 IsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{IsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom}(a, s).
‣ AddIsomorphismFromObjectToLeftInternalCoHom ( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToLeftInternalCoHom ( C, F, weight ) | ( 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 IsomorphismFromObjectToLeftInternalCoHom
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToLeftInternalCoHom}(a).
‣ AddIsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom ( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom ( C, F, weight ) | ( 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 IsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom}(a, r).
‣ AddLeftCoDualOnMorphisms ( C, F ) | ( operation ) |
‣ AddLeftCoDualOnMorphisms ( C, F, weight ) | ( 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 LeftCoDualOnMorphisms
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{LeftCoDualOnMorphisms}(alpha).
‣ AddLeftCoDualOnMorphismsWithGivenLeftCoDuals ( C, F ) | ( operation ) |
‣ AddLeftCoDualOnMorphismsWithGivenLeftCoDuals ( C, F, weight ) | ( 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 LeftCoDualOnMorphismsWithGivenLeftCoDuals
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, r ) \mapsto \mathtt{LeftCoDualOnMorphismsWithGivenLeftCoDuals}(s, alpha, r).
‣ AddLeftCoDualOnObjects ( C, F ) | ( operation ) |
‣ AddLeftCoDualOnObjects ( C, F, weight ) | ( 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 LeftCoDualOnObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{LeftCoDualOnObjects}(a).
‣ AddLeftCoDualityTensorProductCompatibilityMorphism ( C, F ) | ( operation ) |
‣ AddLeftCoDualityTensorProductCompatibilityMorphism ( C, F, weight ) | ( 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 LeftCoDualityTensorProductCompatibilityMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{LeftCoDualityTensorProductCompatibilityMorphism}(a, b).
‣ AddLeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddLeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects ( C, F, weight ) | ( 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 LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects}(s, a, b, r).
‣ AddLeftCoclosedMonoidalCoevaluationMorphism ( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalCoevaluationMorphism ( C, F, weight ) | ( 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 LeftCoclosedMonoidalCoevaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{LeftCoclosedMonoidalCoevaluationMorphism}(a, b).
‣ AddLeftCoclosedMonoidalCoevaluationMorphismWithGivenSource ( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalCoevaluationMorphismWithGivenSource ( C, F, weight ) | ( 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 LeftCoclosedMonoidalCoevaluationMorphismWithGivenSource
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, s ) \mapsto \mathtt{LeftCoclosedMonoidalCoevaluationMorphismWithGivenSource}(a, b, s).
‣ AddLeftCoclosedMonoidalEvaluationForLeftCoDual ( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalEvaluationForLeftCoDual ( C, F, weight ) | ( 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 LeftCoclosedMonoidalEvaluationForLeftCoDual
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{LeftCoclosedMonoidalEvaluationForLeftCoDual}(a).
‣ AddLeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct ( C, F, weight ) | ( 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 LeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, r ) \mapsto \mathtt{LeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct}(s, a, r).
‣ AddLeftCoclosedMonoidalEvaluationMorphism ( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalEvaluationMorphism ( C, F, weight ) | ( 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 LeftCoclosedMonoidalEvaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{LeftCoclosedMonoidalEvaluationMorphism}(a, b).
‣ AddLeftCoclosedMonoidalEvaluationMorphismWithGivenRange ( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalEvaluationMorphismWithGivenRange ( C, F, weight ) | ( 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 LeftCoclosedMonoidalEvaluationMorphismWithGivenRange
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, r ) \mapsto \mathtt{LeftCoclosedMonoidalEvaluationMorphismWithGivenRange}(a, b, r).
‣ AddLeftCoclosedMonoidalLambdaElimination ( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalLambdaElimination ( C, F, weight ) | ( 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 LeftCoclosedMonoidalLambdaElimination
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, alpha ) \mapsto \mathtt{LeftCoclosedMonoidalLambdaElimination}(a, b, alpha).
‣ AddLeftCoclosedMonoidalLambdaIntroduction ( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalLambdaIntroduction ( C, F, weight ) | ( 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 LeftCoclosedMonoidalLambdaIntroduction
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{LeftCoclosedMonoidalLambdaIntroduction}(alpha).
‣ AddLeftCoclosedMonoidalPostCoComposeMorphism ( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalPostCoComposeMorphism ( C, F, weight ) | ( 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 LeftCoclosedMonoidalPostCoComposeMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{LeftCoclosedMonoidalPostCoComposeMorphism}(a, b, c).
‣ AddLeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects ( C, F, weight ) | ( 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 LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects}(s, a, b, c, r).
‣ AddLeftCoclosedMonoidalPreCoComposeMorphism ( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalPreCoComposeMorphism ( C, F, weight ) | ( 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 LeftCoclosedMonoidalPreCoComposeMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{LeftCoclosedMonoidalPreCoComposeMorphism}(a, b, c).
‣ AddLeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects ( C, F, weight ) | ( 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 LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects}(s, a, b, c, r).
‣ AddLeftInternalCoHomOnMorphisms ( C, F ) | ( operation ) |
‣ AddLeftInternalCoHomOnMorphisms ( C, F, weight ) | ( 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 LeftInternalCoHomOnMorphisms
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha, beta ) \mapsto \mathtt{LeftInternalCoHomOnMorphisms}(alpha, beta).
‣ AddLeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms ( C, F ) | ( operation ) |
‣ AddLeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms ( C, F, weight ) | ( 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 LeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, beta, r ) \mapsto \mathtt{LeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms}(s, alpha, beta, r).
‣ AddLeftInternalCoHomOnObjects ( C, F ) | ( operation ) |
‣ AddLeftInternalCoHomOnObjects ( C, F, weight ) | ( 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 LeftInternalCoHomOnObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{LeftInternalCoHomOnObjects}(a, b).
‣ AddLeftInternalCoHomTensorProductCompatibilityMorphism ( C, F ) | ( operation ) |
‣ AddLeftInternalCoHomTensorProductCompatibilityMorphism ( C, F, weight ) | ( 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 LeftInternalCoHomTensorProductCompatibilityMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( list ) \mapsto \mathtt{LeftInternalCoHomTensorProductCompatibilityMorphism}(list).
‣ AddLeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddLeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects ( C, F, weight ) | ( 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 LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( source, list, range ) \mapsto \mathtt{LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}(source, list, range).
‣ AddLeftInternalCoHomToTensorProductAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddLeftInternalCoHomToTensorProductAdjunctMorphism ( C, F, weight ) | ( 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 LeftInternalCoHomToTensorProductAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, c, f ) \mapsto \mathtt{LeftInternalCoHomToTensorProductAdjunctMorphism}(a, c, f).
‣ AddLeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddLeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct ( C, F, weight ) | ( 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 LeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, c, f, t ) \mapsto \mathtt{LeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct}(a, c, f, t).
‣ AddMorphismFromLeftCoBidual ( C, F ) | ( operation ) |
‣ AddMorphismFromLeftCoBidual ( C, F, weight ) | ( 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 MorphismFromLeftCoBidual
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{MorphismFromLeftCoBidual}(a).
‣ AddMorphismFromLeftCoBidualWithGivenLeftCoBidual ( C, F ) | ( operation ) |
‣ AddMorphismFromLeftCoBidualWithGivenLeftCoBidual ( C, F, weight ) | ( 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 MorphismFromLeftCoBidualWithGivenLeftCoBidual
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{MorphismFromLeftCoBidualWithGivenLeftCoBidual}(a, s).
‣ AddMorphismFromLeftInternalCoHomToTensorProduct ( C, F ) | ( operation ) |
‣ AddMorphismFromLeftInternalCoHomToTensorProduct ( C, F, weight ) | ( 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 MorphismFromLeftInternalCoHomToTensorProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{MorphismFromLeftInternalCoHomToTensorProduct}(a, b).
‣ AddMorphismFromLeftInternalCoHomToTensorProductWithGivenObjects ( C, F ) | ( operation ) |
‣ AddMorphismFromLeftInternalCoHomToTensorProductWithGivenObjects ( C, F, weight ) | ( 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 MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects}(s, a, b, r).
‣ AddTensorProductToLeftInternalCoHomAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddTensorProductToLeftInternalCoHomAdjunctMorphism ( C, F, weight ) | ( 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 TensorProductToLeftInternalCoHomAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g ) \mapsto \mathtt{TensorProductToLeftInternalCoHomAdjunctMorphism}(b, c, g).
‣ AddTensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom ( C, F ) | ( operation ) |
‣ AddTensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom ( C, F, weight ) | ( 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 TensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g, i ) \mapsto \mathtt{TensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom}(b, c, g, i).
‣ AddUniversalPropertyOfLeftCoDual ( C, F ) | ( operation ) |
‣ AddUniversalPropertyOfLeftCoDual ( C, F, weight ) | ( 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 UniversalPropertyOfLeftCoDual
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfLeftCoDual}(t, a, alpha).
‣ AddAssociatorLeftToRight ( C, F ) | ( operation ) |
‣ AddAssociatorLeftToRight ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{AssociatorLeftToRight}(a, b, c).
‣ AddAssociatorLeftToRightWithGivenTensorProducts ( C, F ) | ( operation ) |
‣ AddAssociatorLeftToRightWithGivenTensorProducts ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{AssociatorLeftToRightWithGivenTensorProducts}(s, a, b, c, r).
‣ AddAssociatorRightToLeft ( C, F ) | ( operation ) |
‣ AddAssociatorRightToLeft ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{AssociatorRightToLeft}(a, b, c).
‣ AddAssociatorRightToLeftWithGivenTensorProducts ( C, F ) | ( operation ) |
‣ AddAssociatorRightToLeftWithGivenTensorProducts ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{AssociatorRightToLeftWithGivenTensorProducts}(s, a, b, c, r).
‣ AddLeftUnitor ( C, F ) | ( operation ) |
‣ AddLeftUnitor ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{LeftUnitor}(a).
‣ AddLeftUnitorInverse ( C, F ) | ( operation ) |
‣ AddLeftUnitorInverse ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{LeftUnitorInverse}(a).
‣ AddLeftUnitorInverseWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddLeftUnitorInverseWithGivenTensorProduct ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{LeftUnitorInverseWithGivenTensorProduct}(a, r).
‣ AddLeftUnitorWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddLeftUnitorWithGivenTensorProduct ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{LeftUnitorWithGivenTensorProduct}(a, s).
‣ AddRightUnitor ( C, F ) | ( operation ) |
‣ AddRightUnitor ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{RightUnitor}(a).
‣ AddRightUnitorInverse ( C, F ) | ( operation ) |
‣ AddRightUnitorInverse ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{RightUnitorInverse}(a).
‣ AddRightUnitorInverseWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddRightUnitorInverseWithGivenTensorProduct ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{RightUnitorInverseWithGivenTensorProduct}(a, r).
‣ AddRightUnitorWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddRightUnitorWithGivenTensorProduct ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{RightUnitorWithGivenTensorProduct}(a, s).
‣ AddTensorProductOnMorphisms ( C, F ) | ( operation ) |
‣ AddTensorProductOnMorphisms ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha, beta ) \mapsto \mathtt{TensorProductOnMorphisms}(alpha, beta).
‣ AddTensorProductOnMorphismsWithGivenTensorProducts ( C, F ) | ( operation ) |
‣ AddTensorProductOnMorphismsWithGivenTensorProducts ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, beta, r ) \mapsto \mathtt{TensorProductOnMorphismsWithGivenTensorProducts}(s, alpha, beta, r).
‣ AddTensorProductOnObjects ( C, F ) | ( operation ) |
‣ AddTensorProductOnObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( arg2, arg3 ) \mapsto \mathtt{TensorProductOnObjects}(arg2, arg3).
‣ AddTensorUnit ( C, F ) | ( operation ) |
‣ AddTensorUnit ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( ) \mapsto \mathtt{TensorUnit}().
‣ AddCoevaluationForDual ( C, F ) | ( operation ) |
‣ AddCoevaluationForDual ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{CoevaluationForDual}(a).
‣ AddCoevaluationForDualWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddCoevaluationForDualWithGivenTensorProduct ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, r ) \mapsto \mathtt{CoevaluationForDualWithGivenTensorProduct}(s, a, r).
‣ AddIsomorphismFromInternalHomToTensorProductWithDualObject ( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalHomToTensorProductWithDualObject ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{IsomorphismFromInternalHomToTensorProductWithDualObject}(a, b).
‣ AddIsomorphismFromTensorProductWithDualObjectToInternalHom ( C, F ) | ( operation ) |
‣ AddIsomorphismFromTensorProductWithDualObjectToInternalHom ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{IsomorphismFromTensorProductWithDualObjectToInternalHom}(a, b).
‣ AddMorphismFromBidual ( C, F ) | ( operation ) |
‣ AddMorphismFromBidual ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{MorphismFromBidual}(a).
‣ AddMorphismFromBidualWithGivenBidual ( C, F ) | ( operation ) |
‣ AddMorphismFromBidualWithGivenBidual ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{MorphismFromBidualWithGivenBidual}(a, s).
‣ AddMorphismFromInternalHomToTensorProduct ( C, F ) | ( operation ) |
‣ AddMorphismFromInternalHomToTensorProduct ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{MorphismFromInternalHomToTensorProduct}(a, b).
‣ AddMorphismFromInternalHomToTensorProductWithGivenObjects ( C, F ) | ( operation ) |
‣ AddMorphismFromInternalHomToTensorProductWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromInternalHomToTensorProductWithGivenObjects}(s, a, b, r).
‣ AddRankMorphism ( C, F ) | ( operation ) |
‣ AddRankMorphism ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{RankMorphism}(a).
‣ AddTensorProductInternalHomCompatibilityMorphismInverse ( C, F ) | ( operation ) |
‣ AddTensorProductInternalHomCompatibilityMorphismInverse ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( list ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphismInverse}(list).
‣ AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects ( C, F ) | ( operation ) |
‣ AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( source, list, range ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects}(source, list, range).
‣ AddTraceMap ( C, F ) | ( operation ) |
‣ AddTraceMap ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{TraceMap}(alpha).
‣ AddCoRankMorphism ( C, F ) | ( operation ) |
‣ AddCoRankMorphism ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{CoRankMorphism}(a).
‣ AddCoTraceMap ( C, F ) | ( operation ) |
‣ AddCoTraceMap ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{CoTraceMap}(alpha).
‣ AddCoclosedCoevaluationForCoDual ( C, F ) | ( operation ) |
‣ AddCoclosedCoevaluationForCoDual ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{CoclosedCoevaluationForCoDual}(a).
‣ AddCoclosedCoevaluationForCoDualWithGivenTensorProduct ( C, F ) | ( operation ) |
‣ AddCoclosedCoevaluationForCoDualWithGivenTensorProduct ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, r ) \mapsto \mathtt{CoclosedCoevaluationForCoDualWithGivenTensorProduct}(s, a, r).
‣ AddInternalCoHomTensorProductCompatibilityMorphismInverse ( C, F ) | ( operation ) |
‣ AddInternalCoHomTensorProductCompatibilityMorphismInverse ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( list ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphismInverse}(list).
‣ AddInternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects ( C, F ) | ( operation ) |
‣ AddInternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( source, list, range ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects}(source, list, range).
‣ AddIsomorphismFromInternalCoHomToTensorProductWithCoDualObject ( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalCoHomToTensorProductWithCoDualObject ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{IsomorphismFromInternalCoHomToTensorProductWithCoDualObject}(a, b).
‣ AddIsomorphismFromTensorProductWithCoDualObjectToInternalCoHom ( C, F ) | ( operation ) |
‣ AddIsomorphismFromTensorProductWithCoDualObjectToInternalCoHom ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom}(a, b).
‣ AddMorphismFromTensorProductToInternalCoHom ( C, F ) | ( operation ) |
‣ AddMorphismFromTensorProductToInternalCoHom ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{MorphismFromTensorProductToInternalCoHom}(a, b).
‣ AddMorphismFromTensorProductToInternalCoHomWithGivenObjects ( C, F ) | ( operation ) |
‣ AddMorphismFromTensorProductToInternalCoHomWithGivenObjects ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromTensorProductToInternalCoHomWithGivenObjects}(s, a, b, r).
‣ AddMorphismToCoBidual ( C, F ) | ( operation ) |
‣ AddMorphismToCoBidual ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{MorphismToCoBidual}(a).
‣ AddMorphismToCoBidualWithGivenCoBidual ( C, F ) | ( operation ) |
‣ AddMorphismToCoBidualWithGivenCoBidual ( C, F, weight ) | ( 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
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{MorphismToCoBidualWithGivenCoBidual}(a, r).
generated by GAPDoc2HTML