Merge pull request #1492 from TKuh/adjunction_with_given

Add derivation for `*AdjunctionMapWithGivenTensorProduct`
homalg-project · Oct 17, 2023 · 91f0ae5 · 91f0ae5
2 parents add7ebd + cf75f32
commit 91f0ae5
Show file tree

Hide file tree

Showing 12 changed files with 174 additions and 6 deletions.
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( ):
 #! 
-#! 65 primitive operations were used to derive 309 operations for this category \
+#! 65 primitive operations were used to derive 311 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 309 operations for this category \
+#! 63 primitive operations were used to derive 311 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.08-14",
+Version := "2023.10-01",
 Date := ~.Version{[ 1 .. 10 ]},
 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",

diff --git a/CartesianCategories/examples/InfoStringOfInstalledOperationsOfCategory.g b/CartesianCategories/examples/InfoStringOfInstalledOperationsOfCategory.g
@@ -15,7 +15,7 @@ distributive := DummyCategory( rec(
   properties := [ "IsBicartesianClosedCategory", "IsSkeletalCategory" ] ) );;
 
 InfoOfInstalledOperationsOfCategory( distributive );
-#! 19 primitive operations were used to derive 112 operations for this category \
+#! 19 primitive operations were used to derive 113 operations for this category \
 #! which algorithmically
 #! * IsBicartesianClosedCategory
 #! and not yet algorithmically

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.08-11
+* from MonoidalCategories v2023.10-01
diff --git a/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi b/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi
@@ -94,6 +94,37 @@ AddDerivationToCAP( ExponentialToDirectProductAdjunctionMap,
 
 end : CategoryFilter := IsCartesianClosedCategory );
 
+##
+AddDerivationToCAP( ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct,
+                    "ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct using DirectProductOnMorphisms and CartesianEvaluationMorphism",
+                    [ [ PreCompose, 1 ],
+                      [ DirectProductOnMorphismsWithGivenDirectProducts, 1 ],
+                      [ IdentityMorphism, 1 ],
+                      [ CartesianEvaluationMorphism, 1 ] ],
+
+  function( cat, b, c, g, t )
+    local ev_bc;
+
+    # g: a → Exp(b,c)
+    #
+    #    a × b
+    #      |
+    #      | g × id_b
+    #      v
+    # Exp(b,c) × b
+    #      |
+    #      | ev_bc
+    #      v
+    #      c
+
+    ev_bc := CartesianEvaluationMorphism( cat, b, c );
+
+    return PreCompose( cat,
+             DirectProductOnMorphismsWithGivenDirectProducts( cat, t, g, IdentityMorphism( cat, b ), Source( ev_bc ) ),
+             ev_bc );
+
+end : CategoryFilter := IsCartesianClosedCategory );
+
 ##
 AddDerivationToCAP( UniversalPropertyOfCartesianDual,
                     "UniversalPropertyOfCartesianDual using the direct product-exponential adjunction",

diff --git a/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi b/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi
@@ -94,6 +94,37 @@ AddDerivationToCAP( CoexponentialToCoproductAdjunctionMap,
 
 end : CategoryFilter := IsCocartesianCoclosedCategory );
 
+##
+AddDerivationToCAP( CoexponentialToCoproductAdjunctionMapWithGivenCoproduct,
+                    "CoexponentialToCoproductAdjunctionMapWithGivenCoproduct using CoproductOnMorphisms and CocartesianEvaluationMorphism",
+                    [ [ PreCompose, 1 ],
+                      [ CocartesianEvaluationMorphism, 1 ],
+                      [ CoproductOnMorphismsWithGivenCoproducts, 1 ],
+                      [ IdentityMorphism, 1 ] ],
+
+  function( cat, a, b, f, t )
+    local cocaev_bc;
+
+    # f: Coexp(a,b) → c
+    #
+    #        a
+    #        |
+    #        | cocaev_ab
+    #        v
+    # Coexp(a,b) ⊔ b
+    #        |
+    #        | f ⊔ id_b
+    #        v
+    #      c ⊔ b
+
+    cocaev_bc := CocartesianEvaluationMorphism( cat, a, b );
+
+    return PreCompose( cat,
+             cocaev_bc,
+             CoproductOnMorphismsWithGivenCoproducts( cat, Range( cocaev_bc ), f, IdentityMorphism( cat, b ), t ) );
+
+end : CategoryFilter := IsCocartesianCoclosedCategory );
+
 ##
 AddDerivationToCAP( UniversalPropertyOfCocartesianDual,
                     "UniversalPropertyOfCocartesianDual using the coexponential-coproduct adjunction",

diff --git a/FreydCategoriesForCAP/gap/CategoryOfRows.autogen.gd b/FreydCategoriesForCAP/gap/CategoryOfRows.autogen.gd
@@ -251,10 +251,12 @@
 #! * <Ref BookName="MonoidalCategories" Func="InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects" Label="for Is" />
 #! * <Ref BookName="MonoidalCategories" Func="InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects" Label="for Is" />
 #! * <Ref BookName="MonoidalCategories" Func="InternalCoHomToTensorProductAdjunctionMap" Label="for Is" />
+#! * <Ref BookName="MonoidalCategories" Func="InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct" Label="for Is" />
 #! * <Ref BookName="MonoidalCategories" Func="InternalHomOnMorphisms" Label="for Is" />
 #! * <Ref BookName="MonoidalCategories" Func="InternalHomOnMorphismsWithGivenInternalHoms" Label="for Is" />
 #! * <Ref BookName="MonoidalCategories" Func="InternalHomOnObjects" Label="for Is" />
 #! * <Ref BookName="MonoidalCategories" Func="InternalHomToTensorProductAdjunctionMap" Label="for Is" />
+#! * <Ref BookName="MonoidalCategories" Func="InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct" Label="for Is" />
 #! * <Ref BookName="CAP" Func="IsIsomorphicForObjects" Label="for Is" />
 #! * <Ref BookName="MonoidalCategories" Func="IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit" Label="for Is" />
 #! * <Ref BookName="MonoidalCategories" Func="IsomorphismFromDualObjectToInternalHomIntoTensorUnit" Label="for Is" />

diff --git a/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi b/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi
@@ -1997,6 +1997,27 @@ end
 
     , 3513 : IsPrecompiledDerivation := true );
 
+    ##
+    AddInternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct( cat,
+
+########
+function ( cat_1, a_1, b_1, f_1, t_1 )
+    local deduped_3_1, deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1;
+    deduped_7_1 := Dimension( b_1 );
+    deduped_6_1 := UnderlyingRing( cat_1 );
+    deduped_5_1 := Dimension( a_1 );
+    deduped_4_1 := deduped_5_1 * deduped_7_1;
+    deduped_3_1 := HomalgIdentityMatrix( deduped_7_1, deduped_6_1 );
+    return CreateCapCategoryMorphismWithAttributes( cat_1, a_1, t_1, UnderlyingMatrix, KroneckerMat( HomalgIdentityMatrix( deduped_5_1, deduped_6_1 ), ConvertMatrixToRow( deduped_3_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_4_1 ], function ( i_2 )
+                            local deduped_1_2;
+                            deduped_1_2 := (i_2 - 1);
+                            return (REM_INT( deduped_1_2, deduped_7_1 ) * deduped_5_1 + QUO_INT( deduped_1_2, deduped_7_1 ) + 1);
+                        end ) ), deduped_4_1 ), deduped_4_1, deduped_4_1, deduped_6_1 ), deduped_3_1 ) * KroneckerMat( HomalgIdentityMatrix( (deduped_7_1 * deduped_5_1), deduped_6_1 ), deduped_3_1 ) * KroneckerMat( UnderlyingMatrix( f_1 ), deduped_3_1 ) );
+end
+########
+
+    , 3312 : IsPrecompiledDerivation := true );
+
     ##
     AddInternalHomOnMorphisms( cat,
 
@@ -2054,6 +2075,27 @@ end
 
     , 3513 : IsPrecompiledDerivation := true );
 
+    ##
+    AddInternalHomToTensorProductAdjunctionMapWithGivenTensorProduct( cat,
+
+########
+function ( cat_1, b_1, c_1, g_1, t_1 )
+    local deduped_3_1, deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1;
+    deduped_7_1 := Dimension( c_1 );
+    deduped_6_1 := UnderlyingRing( cat_1 );
+    deduped_5_1 := Dimension( b_1 );
+    deduped_4_1 := deduped_5_1 * deduped_7_1;
+    deduped_3_1 := HomalgIdentityMatrix( deduped_5_1, deduped_6_1 );
+    return CreateCapCategoryMorphismWithAttributes( cat_1, t_1, c_1, UnderlyingMatrix, KroneckerMat( UnderlyingMatrix( g_1 ), deduped_3_1 ) * (KroneckerMat( HomalgIdentityMatrix( deduped_4_1, deduped_6_1 ), deduped_3_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_4_1 ], function ( i_2 )
+                            local deduped_1_2;
+                            deduped_1_2 := (i_2 - 1);
+                            return (REM_INT( deduped_1_2, deduped_7_1 ) * deduped_5_1 + QUO_INT( deduped_1_2, deduped_7_1 ) + 1);
+                        end ) ), deduped_4_1 ), deduped_4_1, deduped_4_1, deduped_6_1 ), deduped_3_1 ) * KroneckerMat( HomalgIdentityMatrix( deduped_7_1, deduped_6_1 ), ConvertMatrixToColumn( deduped_3_1 ) )) );
+end
+########
+
+    , 3312 : IsPrecompiledDerivation := true );
+
     ##
     AddInterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( 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.08-11",
+Version := "2023.10-01",
 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",
 

diff --git a/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi
@@ -91,6 +91,37 @@ AddDerivationToCAP( InternalHomToTensorProductAdjunctionMap,
 
 end : CategoryFilter := IsSymmetricClosedMonoidalCategory );
 
+##
+AddDerivationToCAP( InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct,
+                    "InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct using TensorProductOnMorphisms and EvaluationMorphism",
+                    [ [ PreCompose, 1 ],
+                      [ TensorProductOnMorphismsWithGivenTensorProducts, 1 ],
+                      [ IdentityMorphism, 1 ],
+                      [ EvaluationMorphism, 1 ] ],
+
+  function( cat, b, c, g, t )
+    local ev_bc;
+
+    # g: a → Hom(b,c)
+    #
+    #    a ⊗ b
+    #      |
+    #      | g ⊗ id_b
+    #      v
+    # Hom(b,c) ⊗ b
+    #      |
+    #      | ev_bc
+    #      v
+    #      c
+
+    ev_bc := EvaluationMorphism( cat, b, c );
+
+    return PreCompose( cat,
+             TensorProductOnMorphismsWithGivenTensorProducts( cat, t, g, IdentityMorphism( cat, b ), Source( ev_bc ) ),
+             ev_bc );
+
+end : CategoryFilter := IsSymmetricClosedMonoidalCategory );
+
 ##
 AddDerivationToCAP( UniversalPropertyOfDual,
                     "UniversalPropertyOfDual using the tensor hom adjunction",

diff --git a/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi
@@ -91,6 +91,37 @@ AddDerivationToCAP( InternalCoHomToTensorProductAdjunctionMap,
 
 end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );
 
+##
+AddDerivationToCAP( InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct,
+                    "InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct using TensorProductOnMorphisms and CoclosedEvaluationMorphism",
+                    [ [ PreCompose, 1 ],
+                      [ CoclosedEvaluationMorphism, 1 ],
+                      [ TensorProductOnMorphismsWithGivenTensorProducts, 1 ],
+                      [ IdentityMorphism, 1 ] ],
+
+  function( cat, a, b, f, t )
+    local coclev_bc;
+
+    # f: Cohom(a,b) → c
+    #
+    #        a
+    #        |
+    #        | coclev_ab
+    #        v
+    # Cohom(a,b) ⊗ b
+    #        |
+    #        | f ⊗ id_b
+    #        v
+    #      c ⊗ b
+
+    coclev_bc := CoclosedEvaluationMorphism( cat, a, b );
+
+    return PreCompose( cat,
+             coclev_bc,
+             TensorProductOnMorphismsWithGivenTensorProducts( cat, Range( coclev_bc ), f, IdentityMorphism( cat, b ), t ) );
+
+end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );
+
 ##
 AddDerivationToCAP( UniversalPropertyOfCoDual,
                     "UniversalPropertyOfCoDual using the cohom tensor adjunction",