Merge pull request #1244 from mohamed-barakat/TensorProductToInternalHomAdjunctionMapWithGivenInternalHom

mohamed-barakat · web-flow · commit 093bbcd1032b · 2023-02-08T21:52:46.000+01:00
derived TensorProductToInternal(Co)HomAdjunctionMapWithGivenInternal(…Co)Hom
diff --git a/CAP/PackageInfo.g b/CAP/PackageInfo.g
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "CAP",
 Subtitle := "Categories, Algorithms, Programming",
-Version := "2023.02-04",
+Version := "2023.02-05",
 Date := Concatenation( "01/", ~.Version{[ 6, 7 ]}, "/", ~.Version{[ 1 .. 4 ]} ),
 License := "GPL-2.0-or-later",
 
diff --git a/CAP/examples/TerminalCategoryWithMultipleObjects.g b/CAP/examples/TerminalCategoryWithMultipleObjects.g
@@ -10,7 +10,7 @@ T := TerminalCategoryWithMultipleObjects( );
 Display( T );
 #! A CAP category with name TerminalCategoryWithMultipleObjects( ):
 #! 
-#! 63 primitive operations were used to derive 302 operations for this category
+#! 63 primitive operations were used to derive 304 operations for this category
 #! which algorithmically
 #! * IsCategoryWithDecidableColifts
 #! * IsCategoryWithDecidableLifts
diff --git a/CAP/examples/TerminalCategoryWithSingleObject.g b/CAP/examples/TerminalCategoryWithSingleObject.g
@@ -10,7 +10,7 @@ T := TerminalCategoryWithSingleObject( );
 Display( T );
 #! A CAP category with name TerminalCategoryWithSingleObject( ):
 #! 
-#! 63 primitive operations were used to derive 302 operations for this category
+#! 63 primitive operations were used to derive 304 operations for this category
 #! which algorithmically
 #! * IsCategoryWithDecidableColifts
 #! * IsCategoryWithDecidableLifts
diff --git a/CartesianCategories/PackageInfo.g b/CartesianCategories/PackageInfo.g
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "CartesianCategories",
 Subtitle := "Cartesian and cocartesian categories and various subdoctrines",
-Version := "2023.02-02",
+Version := "2023.02-03",
 Date := ~.Version{[ 1 .. 10 ]},
 Date := Concatenation( "01/", ~.Version{[ 6, 7 ]}, "/", ~.Version{[ 1 .. 4 ]} ),
 License := "GPL-2.0-or-later",
@@ -101,7 +101,7 @@ Dependencies := rec(
                 [ "CAP", ">= 2022.12-06" ],
                 ],
   SuggestedOtherPackages := [
-                [ "MonoidalCategories", ">= 2023.02-01" ],
+                [ "MonoidalCategories", ">= 2023.02-03" ],
                 ],
   ExternalConditions := [ ],
 ),
diff --git a/CartesianCategories/examples/InfoStringOfInstalledOperationsOfCategory.g b/CartesianCategories/examples/InfoStringOfInstalledOperationsOfCategory.g
@@ -16,7 +16,7 @@ distributive := DummyCategory( rec(
                   "IsSkeletalCategory" ] ) );;
 
 InfoOfInstalledOperationsOfCategory( distributive );
-#! 19 primitive operations were used to derive 109 operations for this category
+#! 19 primitive operations were used to derive 110 operations for this category
 #! which algorithmically
 #! * IsBicartesianClosedCategory
 #! and furthermore mathematically
diff --git a/CartesianCategories/gap/AUTOGENERATED_FROM.md b/CartesianCategories/gap/AUTOGENERATED_FROM.md
@@ -1,3 +1,3 @@
 The files of this package which include the line `THIS FILE WAS AUTOMATICALLY GENERATED` in their header have been autogenerated
 
-* from MonoidalCategories v2023.02-01
+* from MonoidalCategories v2023.02-03
diff --git a/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi b/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi
@@ -31,6 +31,33 @@ AddDerivationToCAP( DirectProductToExponentialAdjunctionMap,
 end : CategoryFilter := IsCartesianClosedCategory,
       Description := "DirectProductToExponentialAdjunctionMap using CartesianCoevaluationMorphism and Exponential" );
 
+##
+AddDerivationToCAP( DirectProductToExponentialAdjunctionMapWithGivenExponential,
+                    
+  function( cat, a, b, f, i )
+    local coev_ab;
+    
+    # f: a × b → c
+    #
+    #      a
+    #      |
+    #      | coev_ab
+    #      v
+    # Exp(b,a × b)
+    #      |
+    #      | Exp(id_b, f)
+    #      v
+    #   Exp(b,c)
+    
+    coev_ab := CartesianCoevaluationMorphism( cat, a, b );
+    
+    return PreCompose( cat,
+             coev_ab,
+             ExponentialOnMorphismsWithGivenExponentials( cat, Range( coev_ab ), IdentityMorphism( cat, b ), f, i ) );
+    
+end : CategoryFilter := IsCartesianClosedCategory,
+      Description := "DirectProductToExponentialAdjunctionMapWithGivenExponential using CartesianCoevaluationMorphism and Exponential" );
+
 ##
 AddDerivationToCAP( ExponentialToDirectProductAdjunctionMap,
                     
diff --git a/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi b/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi
@@ -31,6 +31,33 @@ AddDerivationToCAP( CoproductToCoexponentialAdjunctionMap,
 end : CategoryFilter := IsCocartesianCoclosedCategory,
       Description := "CoproductToCoexponentialAdjunctionMap using CocartesianCoevaluationMorphism and Coexponential" );
 
+##
+AddDerivationToCAP( CoproductToCoexponentialAdjunctionMapWithGivenCoexponential,
+
+  function( cat, c, b, g, i )
+    local cocacoev_cb;
+    
+    # g: a → c ⊔ b
+    #
+    #    Coexp(a,b)
+    #        |
+    #        | Coexp(g, id_b)
+    #        v
+    # Coexp(c ⊔ b, b)
+    #        |
+    #        | cocacoev_cb
+    #        v
+    #        c
+    
+    cocacoev_cb := CocartesianCoevaluationMorphism( cat, c, b );
+    
+    return PreCompose( cat,
+             CoexponentialOnMorphismsWithGivenCoexponentials( cat, i, g, IdentityMorphism( cat, b ), Source( cocacoev_cb ) ),
+             cocacoev_cb );
+    
+end : CategoryFilter := IsCocartesianCoclosedCategory,
+      Description := "CoproductToCoexponentialAdjunctionMapWithGivenCoexponential using CocartesianCoevaluationMorphism and Coexponential" );
+
 ##
 AddDerivationToCAP( CoexponentialToCoproductAdjunctionMap,
 
diff --git a/FreydCategoriesForCAP/gap/CategoryOfRows.autogen.gd b/FreydCategoriesForCAP/gap/CategoryOfRows.autogen.gd
@@ -323,7 +323,9 @@
 #! * <Ref BookName="MonoidalCategories" Func="TensorProductOnMorphismsWithGivenTensorProducts" Label="for Is" />
 #! * <Ref BookName="MonoidalCategories" Func="TensorProductOnObjects" Label="for Is" />
 #! * <Ref BookName="MonoidalCategories" Func="TensorProductToInternalCoHomAdjunctionMap" Label="for Is" />
+#! * <Ref BookName="MonoidalCategories" Func="TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom" Label="for Is" />
 #! * <Ref BookName="MonoidalCategories" Func="TensorProductToInternalHomAdjunctionMap" Label="for Is" />
+#! * <Ref BookName="MonoidalCategories" Func="TensorProductToInternalHomAdjunctionMapWithGivenInternalHom" Label="for Is" />
 #! * <Ref BookName="MonoidalCategories" Func="TensorUnit" Label="for Is" />
 #! * <Ref BookName="MonoidalCategories" Func="TraceMap" Label="for Is" />
 #! * <Ref BookName="MonoidalCategories" Func="UniversalPropertyOfCoDual" Label="for Is" />
diff --git a/LinearAlgebraForCAP/PackageInfo.g b/LinearAlgebraForCAP/PackageInfo.g
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "LinearAlgebraForCAP",
 Subtitle := "Category of Matrices over a Field for CAP",
-Version := "2023.02-01",
+Version := "2023.02-02",
 Date := Concatenation( "01/", ~.Version{[ 6, 7 ]}, "/", ~.Version{[ 1 .. 4 ]} ),
 License := "GPL-2.0-or-later",
 
@@ -90,7 +90,7 @@ Dependencies := rec(
                            [ "MatricesForHomalg", ">= 2023.01-01" ],
                            [ "GaussForHomalg", ">= 2021.04-02" ],
                            [ "CAP", ">= 2022.12-07" ],
-                           [ "MonoidalCategories", ">= 2022.06-01" ],
+                           [ "MonoidalCategories", ">= 2023.02-03" ],
                            ],
   SuggestedOtherPackages := [
     [ "FreydCategoriesForCAP", ">= 2022.12-02" ],
diff --git a/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi b/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi
@@ -5853,6 +5853,36 @@ end
         
     , 5024 : IsPrecompiledDerivation := true );
     
+    ##
+    AddTensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom( cat,
+        
+########
+function ( cat_1, c_1, b_1, g_1, i_1 )
+    local morphism_attr_1_1, hoisted_2_1, hoisted_3_1, deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1, deduped_8_1, deduped_9_1, deduped_10_1;
+    deduped_10_1 := Dimension( c_1 );
+    deduped_9_1 := UnderlyingRing( cat_1 );
+    deduped_8_1 := Dimension( b_1 );
+    deduped_7_1 := HomalgIdentityMatrix( deduped_10_1, deduped_9_1 );
+    deduped_6_1 := deduped_8_1 * deduped_8_1;
+    deduped_5_1 := deduped_10_1 * deduped_8_1;
+    deduped_4_1 := HomalgIdentityMatrix( deduped_8_1, deduped_9_1 );
+    hoisted_3_1 := deduped_10_1;
+    hoisted_2_1 := deduped_8_1;
+    morphism_attr_1_1 := KroneckerMat( TransposedMatrix( deduped_4_1 ), UnderlyingMatrix( g_1 ) ) * (KroneckerMat( deduped_4_1, HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_5_1 ], function ( i_2 )
+                          local deduped_1_2;
+                          deduped_1_2 := (i_2 - 1);
+                          return (REM_INT( deduped_1_2, hoisted_2_1 ) * hoisted_3_1 + QUO_INT( deduped_1_2, hoisted_2_1 ) + 1);
+                      end ) ), deduped_5_1 ), deduped_5_1, deduped_5_1, deduped_9_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_6_1 ], function ( i_2 )
+                          local deduped_1_2;
+                          deduped_1_2 := (i_2 - 1);
+                          return (REM_INT( deduped_1_2, hoisted_2_1 ) * hoisted_2_1 + QUO_INT( deduped_1_2, hoisted_2_1 ) + 1);
+                      end ) ), deduped_6_1 ), deduped_6_1, deduped_6_1, deduped_9_1 ), deduped_7_1 ) * KroneckerMat( ConvertMatrixToColumn( deduped_4_1 ), deduped_7_1 ));
+    return CreateCapCategoryMorphismWithAttributes( cat_1, CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberRows( morphism_attr_1_1 ) ), CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberColumns( morphism_attr_1_1 ) ), UnderlyingMatrix, morphism_attr_1_1 );
+end
+########
+        
+    , 4419 : IsPrecompiledDerivation := true );
+    
     ##
     AddTensorProductToInternalHomAdjunctionMap( cat,
         
@@ -5883,6 +5913,36 @@ end
         
     , 5024 : IsPrecompiledDerivation := true );
     
+    ##
+    AddTensorProductToInternalHomAdjunctionMapWithGivenInternalHom( cat,
+        
+########
+function ( cat_1, a_1, b_1, f_1, i_1 )
+    local morphism_attr_1_1, hoisted_2_1, hoisted_3_1, deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1, deduped_8_1, deduped_9_1, deduped_10_1;
+    deduped_10_1 := Dimension( a_1 );
+    deduped_9_1 := UnderlyingRing( cat_1 );
+    deduped_8_1 := Dimension( b_1 );
+    deduped_7_1 := deduped_8_1 * deduped_10_1;
+    deduped_6_1 := deduped_8_1 * deduped_8_1;
+    deduped_5_1 := HomalgIdentityMatrix( deduped_10_1, deduped_9_1 );
+    deduped_4_1 := HomalgIdentityMatrix( deduped_8_1, deduped_9_1 );
+    hoisted_3_1 := deduped_10_1;
+    hoisted_2_1 := deduped_8_1;
+    morphism_attr_1_1 := KroneckerMat( ConvertMatrixToRow( deduped_4_1 ), deduped_5_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_6_1 ], function ( i_2 )
+                          local deduped_1_2;
+                          deduped_1_2 := (i_2 - 1);
+                          return (REM_INT( deduped_1_2, hoisted_2_1 ) * hoisted_2_1 + QUO_INT( deduped_1_2, hoisted_2_1 ) + 1);
+                      end ) ), deduped_6_1 ), deduped_6_1, deduped_6_1, deduped_9_1 ), deduped_5_1 ) * KroneckerMat( deduped_4_1, HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_7_1 ], function ( i_2 )
+                        local deduped_1_2;
+                        deduped_1_2 := (i_2 - 1);
+                        return (REM_INT( deduped_1_2, hoisted_3_1 ) * hoisted_2_1 + QUO_INT( deduped_1_2, hoisted_3_1 ) + 1);
+                    end ) ), deduped_7_1 ), deduped_7_1, deduped_7_1, deduped_9_1 ) ) * KroneckerMat( TransposedMatrix( deduped_4_1 ), UnderlyingMatrix( f_1 ) );
+    return CreateCapCategoryMorphismWithAttributes( cat_1, CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberRows( morphism_attr_1_1 ) ), CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberColumns( morphism_attr_1_1 ) ), UnderlyingMatrix, morphism_attr_1_1 );
+end
+########
+        
+    , 4419 : IsPrecompiledDerivation := true );
+    
     ##
     AddTensorUnit( cat,
         
diff --git a/MonoidalCategories/PackageInfo.g b/MonoidalCategories/PackageInfo.g
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "MonoidalCategories",
 Subtitle := "Monoidal and monoidal (co)closed categories",
-Version := "2023.02-02",
+Version := "2023.02-03",
 Date := Concatenation( "01/", ~.Version{[ 6, 7 ]}, "/", ~.Version{[ 1 .. 4 ]} ),
 License := "GPL-2.0-or-later",
 
diff --git a/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi
@@ -28,6 +28,33 @@ AddDerivationToCAP( TensorProductToInternalHomAdjunctionMap,
 end : CategoryFilter := IsSymmetricClosedMonoidalCategory,
       Description := "TensorProductToInternalHomAdjunctionMap using CoevaluationMorphism and InternalHom" );
 
+##
+AddDerivationToCAP( TensorProductToInternalHomAdjunctionMapWithGivenInternalHom,
+                    
+  function( cat, a, b, f, i )
+    local coev_ab;
+    
+    # f: a ⊗ b → c
+    #
+    #      a
+    #      |
+    #      | coev_ab
+    #      v
+    # Hom(b,a ⊗ b)
+    #      |
+    #      | Hom(id_b, f)
+    #      v
+    #   Hom(b,c)
+    
+    coev_ab := CoevaluationMorphism( cat, a, b );
+    
+    return PreCompose( cat,
+             coev_ab,
+             InternalHomOnMorphismsWithGivenInternalHoms( cat, Range( coev_ab ), IdentityMorphism( cat, b ), f, i ) );
+    
+end : CategoryFilter := IsSymmetricClosedMonoidalCategory,
+      Description := "TensorProductToInternalHomAdjunctionMapWithGivenInternalHom using CoevaluationMorphism and InternalHom" );
+
 ##
 AddDerivationToCAP( InternalHomToTensorProductAdjunctionMap,
                     
diff --git a/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi
@@ -28,6 +28,33 @@ AddDerivationToCAP( TensorProductToInternalCoHomAdjunctionMap,
 end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory,
       Description := "TensorProductToInternalCoHomAdjunctionMap using CoclosedCoevaluationMorphism and InternalCoHom" );
 
+##
+AddDerivationToCAP( TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom,
+
+  function( cat, c, b, g, i )
+    local coclcoev_cb;
+    
+    # g: a → c ⊗ b
+    #
+    #    Cohom(a,b)
+    #        |
+    #        | Cohom(g, id_b)
+    #        v
+    # Cohom(c ⊗ b, b)
+    #        |
+    #        | coclcoev_cb
+    #        v
+    #        c
+    
+    coclcoev_cb := CoclosedCoevaluationMorphism( cat, c, b );
+    
+    return PreCompose( cat,
+             InternalCoHomOnMorphismsWithGivenInternalCoHoms( cat, i, g, IdentityMorphism( cat, b ), Source( coclcoev_cb ) ),
+             coclcoev_cb );
+    
+end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory,
+      Description := "TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom using CoclosedCoevaluationMorphism and InternalCoHom" );
+
 ##
 AddDerivationToCAP( InternalCoHomToTensorProductAdjunctionMap,
 

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,3 @@`
`1`	`1`	The files of this package which include the line `THIS FILE WAS AUTOMATICALLY GENERATED` in their header have been autogenerated
`2`	`2`
`3`		`-* from MonoidalCategories v2023.02-01`
	`3`	`+* from MonoidalCategories v2023.02-03`