diff --git a/CAP/examples/TerminalCategoryWithMultipleObjects.g b/CAP/examples/TerminalCategoryWithMultipleObjects.g index d19ed48aac..66776c90d3 100644 --- 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 index b704615f9b..6200794623 100644 --- 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 index 247ebc9ebd..01612ec834 100644 --- 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 index 1a09eebd73..d2742c9527 100644 --- 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 index a88ef77df3..2e06c77203 100644 --- 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 index c7fb927b20..97914446f6 100644 --- 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 index 916d7485b3..d7b171053c 100644 --- 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 index 293c1f72ee..14b6dadf63 100644 --- a/FreydCategoriesForCAP/gap/CategoryOfRows.autogen.gd +++ b/FreydCategoriesForCAP/gap/CategoryOfRows.autogen.gd @@ -251,10 +251,12 @@ #! * #! * #! * +#! * #! * #! * #! * #! * +#! * #! * #! * #! * diff --git a/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi b/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi index 8d4c777ee4..84c0c9c914 100644 --- 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 index b9a6e5e232..7f671df4fc 100644 --- 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 index 4f3152194f..34e1bebdf7 100644 --- 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 index 34b8ad4470..2dc4016d68 100644 --- 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",