Add UniversalPropertyOf(Co)DualWithGiven(Co)DualObject

Author: Tom Kuhmichel

MonoidalCategories/PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "MonoidalCategories",
 Subtitle := "Monoidal and monoidal (co)closed categories",
-Version := "2023.11-02",
+Version := "2023.11-03",
 Date := (function ( ) if IsBound( GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE ) then return GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE; else return Concatenation( ~.Version{[ 1 .. 4 ]}, "-", ~.Version{[ 6, 7 ]}, "-01" ); fi; end)( ),
 License := "GPL-2.0-or-later",
 

MonoidalCategories/gap/ClosedMonoidalCategories.autogen.gd

@@ -711,3 +711,22 @@ DeclareOperation( "AddUniversalPropertyOfDual",
 
 DeclareOperation( "AddUniversalPropertyOfDual",
                   [ IsCapCategory, IsList ] );
+
+#! @Description
+#! The arguments are a category $C$ and a function $F$.
+#! This operation adds the given function $F$
+#! to the category for the basic operation `UniversalPropertyOfDualWithGivenDualObject`.
+#! $F: ( t, a, alpha, d ) \mapsto \mathtt{UniversalPropertyOfDualWithGivenDualObject}(t, a, alpha, d)$.
+#! @Returns nothing
+#! @Arguments C, F
+DeclareOperation( "AddUniversalPropertyOfDualWithGivenDualObject",
+                  [ IsCapCategory, IsFunction ] );
+
+DeclareOperation( "AddUniversalPropertyOfDualWithGivenDualObject",
+                  [ IsCapCategory, IsFunction, IsInt ] );
+
+DeclareOperation( "AddUniversalPropertyOfDualWithGivenDualObject",
+                  [ IsCapCategory, IsList, IsInt ] );
+
+DeclareOperation( "AddUniversalPropertyOfDualWithGivenDualObject",
+                  [ IsCapCategory, IsList ] );

MonoidalCategories/gap/ClosedMonoidalCategories.gd

@@ -314,6 +314,17 @@ DeclareAttribute( "IsomorphismFromInternalHomIntoTensorUnitToDualObject",
 DeclareOperation( "UniversalPropertyOfDual",
                   [ IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryMorphism ] );
 
+#! @Description
+#! The arguments are two objects $t,a$,
+#! a morphism $\alpha: t \otimes a \rightarrow 1$ and
+#! the dual object $d = a^{\vee}$.
+#! The output is the morphism $t \rightarrow a^{\vee}$
+#! given by the universal property of $a^{\vee}$.
+#! @Returns a morphism in $\mathrm{Hom}(t, a^{\vee})$.
+#! @Arguments t, a, alpha, d
+DeclareOperation( "UniversalPropertyOfDualWithGivenDualObject",
+                  [ IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryMorphism, IsCapCategoryObject ] );
+
 #! @Description
 #! The argument is a morphism $\alpha: a \rightarrow b$.
 #! The output is the corresponding morphism $1 \rightarrow \mathrm{\underline{Hom}}(a,b)$

MonoidalCategories/gap/ClosedMonoidalCategoriesMethodRecord.gi

@@ -400,6 +400,18 @@ UniversalPropertyOfDual := rec(
   # Test in ClosedMonoidalCategoriesTest
 ),
 
+UniversalPropertyOfDualWithGivenDualObject:= rec(
+  filter_list := [ "category", "object", "object", "morphism", "object" ],
+  input_arguments_names := [ "cat", "t", "a", "alpha", "d" ],
+  output_source_getter_string := "t",
+  output_source_getter_preconditions := [ ],
+  output_range_getter_string := "d",
+  output_range_getter_preconditions := [ ],
+  return_type := "morphism",
+  dual_operation := "UniversalPropertyOfCoDualWithGivenCoDualObject",
+  dual_arguments_reversed := false,
+),
+
 LambdaIntroduction := rec(
   filter_list := [ "category", "morphism" ],
   return_type := "morphism",

MonoidalCategories/gap/CoclosedMonoidalCategories.autogen.gd

@@ -711,3 +711,22 @@ DeclareOperation( "AddUniversalPropertyOfCoDual",
 
 DeclareOperation( "AddUniversalPropertyOfCoDual",
                   [ IsCapCategory, IsList ] );
+
+#! @Description
+#! The arguments are a category $C$ and a function $F$.
+#! This operation adds the given function $F$
+#! to the category for the basic operation `UniversalPropertyOfCoDualWithGivenCoDualObject`.
+#! $F: ( t, a, alpha, c ) \mapsto \mathtt{UniversalPropertyOfCoDualWithGivenCoDualObject}(t, a, alpha, c)$.
+#! @Returns nothing
+#! @Arguments C, F
+DeclareOperation( "AddUniversalPropertyOfCoDualWithGivenCoDualObject",
+                  [ IsCapCategory, IsFunction ] );
+
+DeclareOperation( "AddUniversalPropertyOfCoDualWithGivenCoDualObject",
+                  [ IsCapCategory, IsFunction, IsInt ] );
+
+DeclareOperation( "AddUniversalPropertyOfCoDualWithGivenCoDualObject",
+                  [ IsCapCategory, IsList, IsInt ] );
+
+DeclareOperation( "AddUniversalPropertyOfCoDualWithGivenCoDualObject",
+                  [ IsCapCategory, IsList ] );

MonoidalCategories/gap/CoclosedMonoidalCategories.gd

@@ -311,6 +311,17 @@ DeclareAttribute( "IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject",
 DeclareOperation( "UniversalPropertyOfCoDual",
                   [ IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryMorphism ] );
 
+#! @Description
+#! The arguments are two objects $t,a$,
+#! a morphism $\alpha: 1 \rightarrow t \otimes a$ and
+#! the codual object $c = a_{\vee}$.
+#! The output is the morphism $a_{\vee} \rightarrow t$
+#! given by the universal property of $a_{\vee}$.
+#! @Returns a morphism in $\mathrm{Hom}(a_{\vee}, t)$.
+#! @Arguments t, a, alpha, c
+DeclareOperation( "UniversalPropertyOfCoDualWithGivenCoDualObject",
+                  [ IsCapCategoryObject, IsCapCategoryObject, IsCapCategoryMorphism, IsCapCategoryObject] );
+
 #! @Description
 #! The argument is a morphism $\alpha: a \rightarrow b$.
 #! The output is the corresponding morphism $ \mathrm{\underline{coHom}}(a,b) \rightarrow 1$

MonoidalCategories/gap/CoclosedMonoidalCategoriesMethodRecord.gi

@@ -400,6 +400,18 @@ UniversalPropertyOfCoDual := rec(
   # Test in CoclosedMonoidalCategoriesTest
 ),
 
+UniversalPropertyOfCoDualWithGivenCoDualObject := rec(
+  filter_list := [ "category", "object", "object", "morphism", "object" ],
+  input_arguments_names := [ "cat", "t", "a", "alpha", "c" ],
+  output_source_getter_string := "c",
+  output_source_getter_preconditions := [ ],
+  output_range_getter_string := "t",
+  output_range_getter_preconditions := [ ],
+  return_type := "morphism",
+  dual_operation := "UniversalPropertyOfDualWithGivenDualObject",
+  dual_arguments_reversed := false,
+),
+
 CoLambdaIntroduction := rec(
   filter_list := [ "category", "morphism" ],
   return_type := "morphism",

MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi

@@ -148,7 +148,7 @@ AddDerivationToCAP( MorphismToBidualWithGivenBidual,
                       [ Braiding, 1 ],
                       [ DualOnObjects, 2 ],
                       [ EvaluationForDual, 1 ],
-                      [ UniversalPropertyOfDual, 1 ] ],
+                      [ UniversalPropertyOfDualWithGivenDualObject, 1 ] ],
 
   function( cat, a, avv )
     local alpha;
@@ -168,7 +168,7 @@ AddDerivationToCAP( MorphismToBidualWithGivenBidual,
     alpha := PreCompose( cat, Braiding( cat, a, DualOnObjects( cat, a ) ),
                             EvaluationForDual( cat, a ) );
 
-    return UniversalPropertyOfDual( cat, a, DualOnObjects( cat, a ), alpha );
+    return UniversalPropertyOfDualWithGivenDualObject( cat, a, DualOnObjects( cat, a ), alpha, avv );
 
 end : CategoryFilter := IsSymmetricClosedMonoidalCategory );
 

MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi

@@ -148,7 +148,7 @@ AddDerivationToCAP( MorphismFromCoBidualWithGivenCoBidual,
                       [ CoclosedEvaluationForCoDual, 1 ],
                       [ Braiding, 1 ],
                       [ CoDualOnObjects, 2 ],
-                      [ UniversalPropertyOfCoDual, 1 ] ],
+                      [ UniversalPropertyOfCoDualWithGivenCoDualObject, 1 ] ],
 
   function( cat, a, avv )
     local alpha;
@@ -170,7 +170,7 @@ AddDerivationToCAP( MorphismFromCoBidualWithGivenCoBidual,
                   CoclosedEvaluationForCoDual( cat, a ),
                   Braiding( cat, CoDualOnObjects( cat, a ), a ) );
 
-    return UniversalPropertyOfCoDual( cat, a, CoDualOnObjects( cat, a ), alpha );
+    return UniversalPropertyOfCoDualWithGivenCoDualObject( cat, a, CoDualOnObjects( cat, a ), alpha, avv );
 
 end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );