diff --git a/CartesianCategories/PackageInfo.g b/CartesianCategories/PackageInfo.g index ec089791d6..db0b4b6cbd 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.11-02", +Version := "2023.11-03", 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/gap/BraidedCartesianCategoriesDerivedMethods.gi b/CartesianCategories/gap/BraidedCartesianCategoriesDerivedMethods.gi index 65e4d52f39..cb9a97d158 100644 --- a/CartesianCategories/gap/BraidedCartesianCategoriesDerivedMethods.gi +++ b/CartesianCategories/gap/BraidedCartesianCategoriesDerivedMethods.gi @@ -11,11 +11,11 @@ AddDerivationToCAP( CartesianBraidingInverseWithGivenDirectProducts, "CartesianBraidingInverseWithGivenDirectProducts as the inverse of the braiding", [ [ InverseForMorphisms, 1 ], - [ CartesianBraiding, 1 ] ], + [ CartesianBraidingWithGivenDirectProducts, 1 ] ], function( cat, object_2_x_object_1, object_1, object_2, object_1_x_object_2 ) - ##TODO: Use CartesianBraidingWithGiven - return InverseForMorphisms( cat, CartesianBraiding( cat, object_1, object_2 ) ); + + return InverseForMorphisms( cat, CartesianBraidingWithGivenDirectProducts( cat, object_1_x_object_2, object_1, object_2, object_2_x_object_1 ) ); end : CategoryFilter := IsCartesianCategory ); @@ -23,10 +23,11 @@ end : CategoryFilter := IsCartesianCategory ); AddDerivationToCAP( CartesianBraidingWithGivenDirectProducts, "CartesianBraidingWithGivenDirectProducts as the inverse of CartesianBraidingInverse", [ [ InverseForMorphisms, 1 ], - [ CartesianBraidingInverse, 1 ] ], + [ CartesianBraidingInverseWithGivenDirectProducts, 1 ] ], function( cat, object_1_x_object_2, object_1, object_2, object_2_x_object_1 ) - ##TODO: Use CartesianBraidingInverseWithGiven - return InverseForMorphisms( cat, CartesianBraidingInverse( cat, object_1, object_2 ) ); + + return InverseForMorphisms( cat, CartesianBraidingInverseWithGivenDirectProducts( cat, object_2_x_object_1, object_1, object_2, object_1_x_object_2 ) ); end : CategoryFilter := IsCartesianCategory ); + diff --git a/CartesianCategories/gap/BraidedCocartesianCategoriesDerivedMethods.gi b/CartesianCategories/gap/BraidedCocartesianCategoriesDerivedMethods.gi index 2bf1285d9c..59265e5097 100644 --- a/CartesianCategories/gap/BraidedCocartesianCategoriesDerivedMethods.gi +++ b/CartesianCategories/gap/BraidedCocartesianCategoriesDerivedMethods.gi @@ -11,11 +11,11 @@ AddDerivationToCAP( CocartesianBraidingInverseWithGivenCoproducts, "CocartesianBraidingInverseWithGivenCoproducts as the inverse of the braiding", [ [ InverseForMorphisms, 1 ], - [ CocartesianBraiding, 1 ] ], + [ CocartesianBraidingWithGivenCoproducts, 1 ] ], function( cat, object_2_u_object_1, object_1, object_2, object_1_u_object_2 ) - ##TODO: Use CocartesianBraidingWithGiven - return InverseForMorphisms( cat, CocartesianBraiding( cat, object_1, object_2 ) ); + + return InverseForMorphisms( cat, CocartesianBraidingWithGivenCoproducts( cat, object_1_u_object_2, object_1, object_2, object_2_u_object_1 ) ); end : CategoryFilter := IsCocartesianCategory ); @@ -23,10 +23,11 @@ end : CategoryFilter := IsCocartesianCategory ); AddDerivationToCAP( CocartesianBraidingWithGivenCoproducts, "CocartesianBraidingWithGivenCoproducts as the inverse of CocartesianBraidingInverse", [ [ InverseForMorphisms, 1 ], - [ CocartesianBraidingInverse, 1 ] ], + [ CocartesianBraidingInverseWithGivenCoproducts, 1 ] ], function( cat, object_1_u_object_2, object_1, object_2, object_2_u_object_1 ) - ##TODO: Use CocartesianBraidingInverseWithGiven - return InverseForMorphisms( cat, CocartesianBraidingInverse( cat, object_1, object_2 ) ); + + return InverseForMorphisms( cat, CocartesianBraidingInverseWithGivenCoproducts( cat, object_2_u_object_1, object_1, object_2, object_1_u_object_2 ) ); end : CategoryFilter := IsCocartesianCategory ); + diff --git a/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi b/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi index 97914446f6..3b0ca74006 100644 --- a/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi +++ b/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi @@ -291,7 +291,7 @@ end : CategoryFilter := IsCartesianClosedCategory ); ## AddDerivationToCAP( CartesianEvaluationForCartesianDualWithGivenDirectProduct, "CartesianEvaluationForCartesianDualWithGivenDirectProduct using the direct product-exponential adjunction and IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject", - [ [ ExponentialToDirectProductAdjunctionMap, 1 ], + [ [ ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct, 1 ], [ IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject, 1 ] ], function( cat, s, a, r ) @@ -300,8 +300,11 @@ AddDerivationToCAP( CartesianEvaluationForCartesianDualWithGivenDirectProduct, # # Adjoint( a^v → Exp(a,1) ) = ( a^v × a → 1 ) - return ExponentialToDirectProductAdjunctionMap( cat, a, r, - IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject( cat, a ) ); + return ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct( cat, + a, + r, + IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject( cat, a ), + s ); end : CategoryFilter := IsCartesianClosedCategory ); @@ -531,14 +534,16 @@ end : CategoryFilter := IsCartesianClosedCategory ); AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential, "IsomorphismFromObjectToExponentialWithGivenExponential using the coevaluation morphism", [ [ TerminalObject, 1 ], + [ DirectProduct, 1 ], + [ ExponentialOnObjects, 1 ], [ PreCompose, 1 ], - [ CartesianCoevaluationMorphism, 1 ], - [ ExponentialOnMorphisms, 1 ], + [ CartesianCoevaluationMorphismWithGivenRange, 1 ], + [ ExponentialOnMorphismsWithGivenExponentials, 1 ], [ IdentityMorphism, 1 ], - [ CartesianRightUnitor, 1 ] ], + [ CartesianRightUnitorWithGivenDirectProduct, 1 ] ], function( cat, a, internal_hom ) - local unit; + local unit, a_x_1, exp_1_ax1; # a # | @@ -551,12 +556,16 @@ AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential, # Exp(1, a) unit := TerminalObject( cat ); + a_x_1 := BinaryDirectProduct( cat, a, unit ); + exp_1_ax1:= ExponentialOnObjects( cat, unit, a_x_1 ); return PreCompose( cat, - CartesianCoevaluationMorphism( cat, a, unit ), - ExponentialOnMorphisms( cat, - IdentityMorphism( cat, unit ), - CartesianRightUnitor( cat, a ) ) ); + CartesianCoevaluationMorphismWithGivenRange( cat, a, unit, exp_1_ax1 ), + ExponentialOnMorphismsWithGivenExponentials( cat, + exp_1_ax1, + IdentityMorphism( cat, unit ), + CartesianRightUnitorWithGivenDirectProduct( cat, a, a_x_1 ), + internal_hom ) ); end : CategoryFilter := IsCartesianClosedCategory ); @@ -564,7 +573,7 @@ end : CategoryFilter := IsCartesianClosedCategory ); AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential, "IsomorphismFromObjectToExponentialWithGivenExponential as the adjoint of the right unitor", [ [ TerminalObject, 1 ], - [ DirectProductToExponentialAdjunctionMap, 1 ], + [ DirectProductToExponentialAdjunctionMapWithGivenExponential, 1 ], [ CartesianRightUnitor, 1 ] ], function( cat, a, internal_hom ) @@ -573,10 +582,11 @@ AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential, # # Adjoint( ρ_a ) = ( a → Exp(1,a) ) - return DirectProductToExponentialAdjunctionMap( cat, + return DirectProductToExponentialAdjunctionMapWithGivenExponential( cat, a, TerminalObject( cat ), - CartesianRightUnitor( cat, a ) ); + CartesianRightUnitor( cat, a ), + internal_hom ); end : CategoryFilter := IsCartesianClosedCategory ); @@ -598,10 +608,13 @@ AddDerivationToCAP( IsomorphismFromExponentialToObjectWithGivenExponential, "IsomorphismFromExponentialToObjectWithGivenExponential using the evaluation morphism", [ [ TerminalObject, 1 ], [ PreCompose, 1 ], - [ CartesianRightUnitorInverse, 1 ], - [ CartesianEvaluationMorphism, 1 ] ], + [ DirectProduct, 1 ], + [ ExponentialOnObjects, 1 ], + [ CartesianRightUnitorInverseWithGivenDirectProduct, 1 ], + [ CartesianEvaluationMorphismWithGivenSource, 1 ] ], function( cat, a, internal_hom ) + local unit, exp_1a, exp_1a_x_1; # Exp(1,a) # | @@ -613,9 +626,13 @@ AddDerivationToCAP( IsomorphismFromExponentialToObjectWithGivenExponential, # v # a + unit := TerminalObject( cat ); + exp_1a := ExponentialOnObjects( cat, unit, a ); + exp_1a_x_1 := BinaryDirectProduct( cat, exp_1a, unit ); + return PreCompose( cat, - CartesianRightUnitorInverse( cat, internal_hom ), - CartesianEvaluationMorphism( cat, TerminalObject( cat ), a ) ); + CartesianRightUnitorInverseWithGivenDirectProduct( cat, internal_hom, exp_1a_x_1 ), + CartesianEvaluationMorphismWithGivenSource( cat, unit, a, exp_1a_x_1 ) ); end : CategoryFilter := IsCartesianClosedCategory ); @@ -682,7 +699,7 @@ end : CategoryFilter := IsCartesianClosedCategory ); ## AddDerivationToCAP( CartesianEvaluationMorphismWithGivenSource, "CartesianEvaluationMorphismWithGivenSource using the direct product-exponential adjunction on the identity", - [ [ ExponentialToDirectProductAdjunctionMap, 1 ], + [ [ ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct, 1 ], [ IdentityMorphism, 1 ], [ ExponentialOnObjects, 1 ] ], @@ -690,16 +707,18 @@ AddDerivationToCAP( CartesianEvaluationMorphismWithGivenSource, # Adjoint( id_Exp(a,b): Exp(a,b) → Exp(a,b) ) = ( Exp(a,b) × a → b ) - return ExponentialToDirectProductAdjunctionMap( cat, - a, b, - IdentityMorphism( cat, ExponentialOnObjects( cat, a, b ) ) ); + return ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct( cat, + a, + b, + IdentityMorphism( cat, ExponentialOnObjects( cat, a, b ) ), + direct_product_object ); end : CategoryFilter := IsCartesianClosedCategory ); ## AddDerivationToCAP( CartesianCoevaluationMorphismWithGivenRange, "CartesianCoevaluationMorphismWithGivenRange using the direct product-exponential adjunction on the identity", - [ [ DirectProductToExponentialAdjunctionMap, 1 ], + [ [ DirectProductToExponentialAdjunctionMapWithGivenExponential, 1 ], [ IdentityMorphism, 1 ], [ DirectProduct, 1 ] ], @@ -707,9 +726,11 @@ AddDerivationToCAP( CartesianCoevaluationMorphismWithGivenRange, # Adjoint( id_(a × b): a × b → a × b ) = ( a → Exp(b, a × b) ) - return DirectProductToExponentialAdjunctionMap( cat, - a, b, - IdentityMorphism( cat, BinaryDirectProduct( cat, a, b ) ) ); + return DirectProductToExponentialAdjunctionMapWithGivenExponential( cat, + a, + b, + IdentityMorphism( cat, BinaryDirectProduct( cat, a, b ) ), + internal_hom ); end : CategoryFilter := IsCartesianClosedCategory ); @@ -852,13 +873,14 @@ end : CategoryFilter := IsCartesianClosedCategory ); ## AddDerivationToCAP( CartesianPostComposeMorphismWithGivenObjects, "CartesianPostComposeMorphismWithGivenObjects using CartesianPreComposeMorphism and braiding", - [ [ CartesianBraiding, 1 ], + [ [ CartesianBraidingWithGivenDirectProducts, 1 ], [ ExponentialOnObjects, 2 ], [ PreCompose, 1 ], - [ CartesianPreComposeMorphism, 1 ] ], + [ DirectProduct, 1], + [ CartesianPreComposeMorphismWithGivenObjects, 1 ] ], function( cat, source, a, b, c, range ) - local braiding; + local exp_ab, exp_bc, exp_ab_x_exp_bc, braiding; # Exp(b,c) × Exp(a,b) # | @@ -870,22 +892,27 @@ AddDerivationToCAP( CartesianPostComposeMorphismWithGivenObjects, # v # Exp(a,c) - braiding := CartesianBraiding( cat, ExponentialOnObjects( cat, b, c ), ExponentialOnObjects( cat, a, b ) ); + exp_ab := ExponentialOnObjects( cat, a, b ); + exp_bc := ExponentialOnObjects( cat, b, c ); + exp_ab_x_exp_bc := BinaryDirectProduct( cat, exp_ab, exp_bc ); + + braiding := CartesianBraidingWithGivenDirectProducts( cat, source, exp_bc, exp_ab, exp_ab_x_exp_bc ); - return PreCompose( cat, braiding, CartesianPreComposeMorphism( cat, a, b, c ) ); + return PreCompose( cat, braiding, CartesianPreComposeMorphismWithGivenObjects( cat, exp_ab_x_exp_bc, a, b, c, range ) ); end : CategoryFilter := IsCartesianClosedCategory ); ## AddDerivationToCAP( CartesianPreComposeMorphismWithGivenObjects, "CartesianPreComposeMorphismWithGivenObjects using CartesianPostComposeMorphism and braiding", - [ [ CartesianBraiding, 1 ], + [ [ CartesianBraidingWithGivenDirectProducts, 1 ], [ ExponentialOnObjects, 2 ], [ PreCompose, 1 ], - [ CartesianPostComposeMorphism, 1 ] ], + [ DirectProduct, 1], + [ CartesianPostComposeMorphismWithGivenObjects, 1 ] ], function( cat, source, a, b, c, range ) - local braiding; + local exp_ab, exp_bc, exp_bc_x_exp_ab, braiding; # Exp(a,b) × Exp(b,c) # | @@ -897,9 +924,13 @@ AddDerivationToCAP( CartesianPreComposeMorphismWithGivenObjects, # v # Exp(a,c) - braiding := CartesianBraiding( cat, ExponentialOnObjects( cat, a, b ), ExponentialOnObjects( cat, b, c ) ); + exp_ab := ExponentialOnObjects( cat, a, b ); + exp_bc := ExponentialOnObjects( cat, b, c ); + exp_bc_x_exp_ab := BinaryDirectProduct( cat, exp_bc, exp_ab ); + + braiding := CartesianBraidingWithGivenDirectProducts( cat, source, exp_bc, exp_ab, exp_bc_x_exp_ab ); - return PreCompose( cat, braiding, CartesianPostComposeMorphism( cat, a, b, c ) ); + return PreCompose( cat, braiding, CartesianPostComposeMorphismWithGivenObjects( cat, exp_bc_x_exp_ab, a, b, c, range ) ); end : CategoryFilter := IsCartesianClosedCategory ); diff --git a/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi b/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi index d7b171053c..9d0c17727d 100644 --- a/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi +++ b/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi @@ -296,7 +296,7 @@ end : CategoryFilter := IsCocartesianCoclosedCategory ); ## AddDerivationToCAP( CocartesianEvaluationForCocartesianDualWithGivenCoproduct, "CocartesianEvaluationForCocartesianDualWithGivenCoproduct using the coexponential-coproduct adjunction and IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject", - [ [ CoexponentialToCoproductAdjunctionMap, 1 ], + [ [ CoexponentialToCoproductAdjunctionMapWithGivenCoproduct, 1 ], [ IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject, 1 ] ], function( cat, s, a, r ) @@ -305,10 +305,11 @@ AddDerivationToCAP( CocartesianEvaluationForCocartesianDualWithGivenCoproduct, # Adjoint( Coexp(1,a) → a_v ) = ( 1 → a_v ⊔ a ) - return CoexponentialToCoproductAdjunctionMap( cat, + return CoexponentialToCoproductAdjunctionMapWithGivenCoproduct( cat, s, a, - IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject( cat, a ) ); + IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject( cat, a ), + r ); end : CategoryFilter := IsCocartesianCoclosedCategory ); @@ -542,13 +543,15 @@ AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential, "IsomorphismFromCoexponentialToObjectWithGivenCoexponential using the cocartesian coevaluation morphism", [ [ InitialObject, 1 ], [ PreCompose, 1 ], - [ CoexponentialOnMorphisms, 1 ], - [ CocartesianRightUnitorInverse, 1 ], + [ Coproduct, 1 ], + [ CoexponentialOnObjects, 1 ], + [ CoexponentialOnMorphismsWithGivenCoexponentials, 1 ], + [ CocartesianRightUnitorInverseWithGivenCoproduct, 1 ], [ IdentityMorphism, 1 ], - [ CocartesianCoevaluationMorphism, 1 ] ], + [ CocartesianCoevaluationMorphismWithGivenSource, 1 ] ], function( cat, a, internal_cohom ) - local unit; + local unit, a_x_1, coexp_a1_1; # Coexp(a, 1) # | @@ -561,13 +564,16 @@ AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential, # a unit := InitialObject( cat ); + a_x_1 := BinaryCoproduct( cat, a, unit ); + coexp_a1_1 := CoexponentialOnObjects( cat, a_x_1, unit ); return PreCompose( cat, - CoexponentialOnMorphisms( cat, - CocartesianRightUnitorInverse( cat, a ), - IdentityMorphism( cat, unit ) ), - - CocartesianCoevaluationMorphism( cat, a, unit ) ); + CoexponentialOnMorphismsWithGivenCoexponentials( cat, + internal_cohom, + CocartesianRightUnitorInverseWithGivenCoproduct( cat, a, a_x_1 ), + IdentityMorphism( cat, unit ), + coexp_a1_1 ), + CocartesianCoevaluationMorphismWithGivenSource( cat, a, unit, coexp_a1_1 ) ); end : CategoryFilter := IsCocartesianCoclosedCategory ); @@ -575,7 +581,7 @@ end : CategoryFilter := IsCocartesianCoclosedCategory ); AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential, "IsomorphismFromCoexponentialToObjectWithGivenCoexponential as the adjoint of the right inverse unitor", [ [ InitialObject, 1 ], - [ CoproductToCoexponentialAdjunctionMap, 1 ], + [ CoproductToCoexponentialAdjunctionMapWithGivenCoexponential, 1 ], [ CocartesianRightUnitorInverse, 1 ] ], function( cat, a, internal_cohom ) @@ -584,10 +590,11 @@ AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential, # # Adjoint( (ρ_a)^-1 ) = ( Coexp(a,1) → a ) - return CoproductToCoexponentialAdjunctionMap( cat, + return CoproductToCoexponentialAdjunctionMapWithGivenCoexponential( cat, a, InitialObject( cat ), - CocartesianRightUnitorInverse( cat, a ) ); + CocartesianRightUnitorInverse( cat, a ), + internal_cohom ); end : CategoryFilter := IsCocartesianCoclosedCategory ); @@ -609,11 +616,12 @@ AddDerivationToCAP( IsomorphismFromObjectToCoexponentialWithGivenCoexponential, "IsomorphismFromObjectToCoexponentialWithGivenCoexponential using the cocartesian evaluation morphism", [ [ InitialObject, 1 ], [ PreCompose, 1 ], - [ CocartesianEvaluationMorphism, 1 ], - [ CocartesianRightUnitor, 1 ] ], + [ CoexponentialOnObjects, 1 ], + [ CocartesianEvaluationMorphismWithGivenRange, 1 ], + [ CocartesianRightUnitorWithGivenCoproduct, 1 ] ], function( cat, a, internal_cohom ) - + local unit, coexp_a1_x_1; # a # | # | cocaev_(a,1) @@ -624,9 +632,12 @@ AddDerivationToCAP( IsomorphismFromObjectToCoexponentialWithGivenCoexponential, # v # Coexp(a,1) + unit := InitialObject( cat ); + coexp_a1_x_1 := CoexponentialOnObjects( cat, internal_cohom, unit ); + return PreCompose( cat, - CocartesianEvaluationMorphism( cat, a, InitialObject( cat ) ), - CocartesianRightUnitor( cat, internal_cohom ) ); + CocartesianEvaluationMorphismWithGivenRange( cat, a, unit, coexp_a1_x_1 ), + CocartesianRightUnitorWithGivenCoproduct( cat, internal_cohom, coexp_a1_x_1 ) ); end : CategoryFilter := IsCocartesianCoclosedCategory ); @@ -693,7 +704,7 @@ end : CategoryFilter := IsCocartesianCoclosedCategory ); ## AddDerivationToCAP( CocartesianEvaluationMorphismWithGivenRange, "CocartesianEvaluationMorphismWithGivenRange using the coexponential-coproduct adjunction on the identity", - [ [ CoexponentialToCoproductAdjunctionMap, 1 ], + [ [ CoexponentialToCoproductAdjunctionMapWithGivenCoproduct, 1 ], [ IdentityMorphism, 1 ], [ CoexponentialOnObjects, 1 ] ], @@ -701,16 +712,17 @@ AddDerivationToCAP( CocartesianEvaluationMorphismWithGivenRange, # Adjoint( id_Coexp(a,b): Coexp(a,b) → Coexp(a,b) ) = ( a → Coexp(a,b) ⊔ b ) - return CoexponentialToCoproductAdjunctionMap( cat, - a, b, - IdentityMorphism( cat, CoexponentialOnObjects( cat, a, b ) ) - ); + return CoexponentialToCoproductAdjunctionMapWithGivenCoproduct( cat, + a, + b, + IdentityMorphism( cat, CoexponentialOnObjects( cat, a, b ) ), + coproduct_object ); end : CategoryFilter := IsCocartesianCoclosedCategory ); AddDerivationToCAP( CocartesianCoevaluationMorphismWithGivenSource, "CocartesianCoevaluationMorphismWithGivenSource using the coexponential-coproduct adjunction on the identity", - [ [ CoproductToCoexponentialAdjunctionMap, 1 ], + [ [ CoproductToCoexponentialAdjunctionMapWithGivenCoexponential, 1 ], [ IdentityMorphism, 1 ], [ Coproduct, 1 ] ], @@ -718,10 +730,11 @@ AddDerivationToCAP( CocartesianCoevaluationMorphismWithGivenSource, # Adjoint( id_(a ⊔ b): a ⊔ b → a ⊔ b ) = ( Coexp(a ⊔ b, b) → a ) - return CoproductToCoexponentialAdjunctionMap( cat, - a, b, - IdentityMorphism( cat, BinaryCoproduct( cat, a, b ) ) - ); + return CoproductToCoexponentialAdjunctionMapWithGivenCoexponential( cat, + a, + b, + IdentityMorphism( cat, BinaryCoproduct( cat, a, b ) ), + internal_cohom ); end : CategoryFilter := IsCocartesianCoclosedCategory ); @@ -864,13 +877,14 @@ end : CategoryFilter := IsCocartesianCoclosedCategory ); ## AddDerivationToCAP( CocartesianPostCoComposeMorphismWithGivenObjects, "CocartesianPostCoComposeMorphismWithGivenObjects using CocartesianPreCoComposeMorphism and braiding", - [ [ CocartesianBraiding, 1 ], + [ [ CocartesianBraidingWithGivenCoproducts, 1 ], [ CoexponentialOnObjects, 2 ], [ PreCompose, 1 ], - [ CocartesianPreCoComposeMorphism, 1 ] ], + [ Coproduct, 1 ], + [ CocartesianPreCoComposeMorphismWithGivenObjects, 1 ] ], function( cat, source, a, b, c, range ) - local braiding; + local coexp_ab, coexp_bc, coexp_bc_x_coexp_ab, braiding; # Coexp(a,c) # | @@ -882,22 +896,27 @@ AddDerivationToCAP( CocartesianPostCoComposeMorphismWithGivenObjects, # v # Coexp(a,b) ⊔ Coexp(b,c) - braiding := CocartesianBraiding( cat, CoexponentialOnObjects( cat, b, c ), CoexponentialOnObjects( cat, a, b ) ); + coexp_ab := CoexponentialOnObjects( cat, a, b ); + coexp_bc := CoexponentialOnObjects( cat, b, c ); + coexp_bc_x_coexp_ab := BinaryCoproduct( cat, coexp_bc, coexp_ab ); - return PreCompose( cat, CocartesianPreCoComposeMorphism( cat, a, b, c ), braiding ); + braiding := CocartesianBraidingWithGivenCoproducts( cat, coexp_bc_x_coexp_ab, coexp_bc, coexp_ab, range ); + + return PreCompose( cat, CocartesianPreCoComposeMorphismWithGivenObjects( cat, source, a, b, c, coexp_bc_x_coexp_ab ), braiding ); end : CategoryFilter := IsCocartesianCoclosedCategory ); ## AddDerivationToCAP( CocartesianPreCoComposeMorphismWithGivenObjects, "CocartesianPreCoComposeMorphismWithGivenObjects using CocartesianPostCoComposeMorphism and braiding", - [ [ CocartesianBraiding, 1 ], + [ [ CocartesianBraidingWithGivenCoproducts, 1 ], [ CoexponentialOnObjects, 2 ], [ PreCompose, 1 ], - [ CocartesianPostCoComposeMorphism, 1 ] ], + [ Coproduct, 1 ], + [ CocartesianPostCoComposeMorphismWithGivenObjects, 1 ] ], function( cat, source, a, b, c, range ) - local braiding; + local coexp_ab, coexp_bc, coexp_ab_x_coexp_bc, braiding; # Coexp(a,c) # | @@ -908,10 +927,14 @@ AddDerivationToCAP( CocartesianPreCoComposeMorphismWithGivenObjects, # | B_( Coexp(a,b), Coexp(b,c) ) # v # Coexp(b,c) ⊔ Coexp(a,b) - - braiding := CocartesianBraiding( cat, CoexponentialOnObjects( cat, a, b ), CoexponentialOnObjects( cat, b, c ) ); - return PreCompose( cat, CocartesianPostCoComposeMorphism( cat, a, b, c ), braiding ); + coexp_ab := CoexponentialOnObjects( cat, a, b ); + coexp_bc := CoexponentialOnObjects( cat, b, c ); + coexp_ab_x_coexp_bc := BinaryCoproduct( cat, coexp_ab, coexp_bc ); + + braiding := CocartesianBraidingWithGivenCoproducts( cat, coexp_ab_x_coexp_bc, coexp_ab, coexp_bc, range ); + + return PreCompose( cat, CocartesianPostCoComposeMorphismWithGivenObjects( cat, source, a, b, c, coexp_ab_x_coexp_bc ), braiding ); end : CategoryFilter := IsCocartesianCoclosedCategory ); diff --git a/LinearAlgebraForCAP/PackageInfo.g b/LinearAlgebraForCAP/PackageInfo.g index 36fc7ec640..0f7c26b5dd 100644 --- 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.11-01", +Version := "2023.11-02", 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/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi b/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi index fdf7af5bb6..bec97b1d21 100644 --- a/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi +++ b/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi @@ -2861,54 +2861,52 @@ end ######## function ( cat_1, a_1 ) - local morphism_attr_1_1, deduped_3_1, deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1, deduped_8_1; - deduped_8_1 := 1 * 1; - deduped_7_1 := Dimension( a_1 ); - deduped_6_1 := UnderlyingRing( cat_1 ); - deduped_5_1 := deduped_7_1 * 1; - deduped_4_1 := HomalgIdentityMatrix( deduped_7_1, deduped_6_1 ); - deduped_3_1 := HomalgIdentityMatrix( 1, deduped_6_1 ); - morphism_attr_1_1 := KroneckerMat( TransposedMatrix( deduped_3_1 ), deduped_4_1 ) * (KroneckerMat( deduped_3_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, 1 ) * deduped_7_1 + QUO_INT( deduped_1_2, 1 ) + 1); - end ) ), deduped_5_1 ), deduped_5_1, deduped_5_1, deduped_6_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_8_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, 1 ) * 1 + QUO_INT( deduped_1_2, 1 ) + 1); - end ) ), deduped_8_1 ), deduped_8_1, deduped_8_1, deduped_6_1 ), deduped_4_1 ) * KroneckerMat( ConvertMatrixToColumn( deduped_3_1 ), deduped_4_1 )); - return CreateCapCategoryMorphismWithAttributes( cat_1, CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberRows( morphism_attr_1_1 ) ), a_1, UnderlyingMatrix, morphism_attr_1_1 ); + local deduped_2_1, deduped_3_1, deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1; + deduped_7_1 := 1 * 1; + deduped_6_1 := Dimension( a_1 ); + deduped_5_1 := UnderlyingRing( cat_1 ); + deduped_4_1 := deduped_6_1 * 1; + deduped_3_1 := HomalgIdentityMatrix( deduped_6_1, deduped_5_1 ); + deduped_2_1 := HomalgIdentityMatrix( 1, deduped_5_1 ); + return CreateCapCategoryMorphismWithAttributes( cat_1, a_1, a_1, UnderlyingMatrix, KroneckerMat( TransposedMatrix( deduped_2_1 ), deduped_3_1 ) * (KroneckerMat( deduped_2_1, 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, 1 ) * deduped_6_1 + QUO_INT( deduped_1_2, 1 ) + 1); + end ) ), deduped_4_1 ), deduped_4_1, deduped_4_1, deduped_5_1 ) ) * KroneckerMat( 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, 1 ) * 1 + QUO_INT( deduped_1_2, 1 ) + 1); + end ) ), deduped_7_1 ), deduped_7_1, deduped_7_1, deduped_5_1 ), deduped_3_1 ) * KroneckerMat( ConvertMatrixToColumn( deduped_2_1 ), deduped_3_1 )) ); end ######## - , 5526 : IsPrecompiledDerivation := true ); + , 5220 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom( cat, ######## function ( cat_1, a_1, s_1 ) - local morphism_attr_1_1, deduped_3_1, deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1, deduped_8_1; - deduped_8_1 := 1 * 1; - deduped_7_1 := Dimension( a_1 ); - deduped_6_1 := UnderlyingRing( cat_1 ); - deduped_5_1 := deduped_7_1 * 1; - deduped_4_1 := HomalgIdentityMatrix( deduped_7_1, deduped_6_1 ); - deduped_3_1 := HomalgIdentityMatrix( 1, deduped_6_1 ); - morphism_attr_1_1 := KroneckerMat( TransposedMatrix( deduped_3_1 ), deduped_4_1 ) * (KroneckerMat( deduped_3_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, 1 ) * deduped_7_1 + QUO_INT( deduped_1_2, 1 ) + 1); - end ) ), deduped_5_1 ), deduped_5_1, deduped_5_1, deduped_6_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_8_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, 1 ) * 1 + QUO_INT( deduped_1_2, 1 ) + 1); - end ) ), deduped_8_1 ), deduped_8_1, deduped_8_1, deduped_6_1 ), deduped_4_1 ) * KroneckerMat( ConvertMatrixToColumn( deduped_3_1 ), deduped_4_1 )); - return CreateCapCategoryMorphismWithAttributes( cat_1, CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberRows( morphism_attr_1_1 ) ), a_1, UnderlyingMatrix, morphism_attr_1_1 ); + local deduped_2_1, deduped_3_1, deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1; + deduped_7_1 := 1 * 1; + deduped_6_1 := Dimension( a_1 ); + deduped_5_1 := UnderlyingRing( cat_1 ); + deduped_4_1 := deduped_6_1 * 1; + deduped_3_1 := HomalgIdentityMatrix( deduped_6_1, deduped_5_1 ); + deduped_2_1 := HomalgIdentityMatrix( 1, deduped_5_1 ); + return CreateCapCategoryMorphismWithAttributes( cat_1, s_1, a_1, UnderlyingMatrix, KroneckerMat( TransposedMatrix( deduped_2_1 ), deduped_3_1 ) * (KroneckerMat( deduped_2_1, 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, 1 ) * deduped_6_1 + QUO_INT( deduped_1_2, 1 ) + 1); + end ) ), deduped_4_1 ), deduped_4_1, deduped_4_1, deduped_5_1 ) ) * KroneckerMat( 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, 1 ) * 1 + QUO_INT( deduped_1_2, 1 ) + 1); + end ) ), deduped_7_1 ), deduped_7_1, deduped_7_1, deduped_5_1 ), deduped_3_1 ) * KroneckerMat( ConvertMatrixToColumn( deduped_2_1 ), deduped_3_1 )) ); end ######## - , 5525 : IsPrecompiledDerivation := true ); + , 5219 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromInternalCoHomToTensorProductWithCoDualObject( cat, @@ -2952,7 +2950,7 @@ function ( cat_1, a_1 ) end ######## - , 3315 : IsPrecompiledDerivation := true ); + , 3313 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromInternalHomToObjectWithGivenInternalHom( cat, @@ -2972,7 +2970,7 @@ function ( cat_1, a_1, s_1 ) end ######## - , 3314 : IsPrecompiledDerivation := true ); + , 3312 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromInternalHomToTensorProductWithDualObject( cat, @@ -3050,7 +3048,7 @@ function ( cat_1, a_1 ) end ######## - , 3315 : IsPrecompiledDerivation := true ); + , 3213 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom( cat, @@ -3070,61 +3068,59 @@ function ( cat_1, a_1, r_1 ) end ######## - , 3314 : IsPrecompiledDerivation := true ); + , 3212 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromObjectToInternalHom( cat, ######## function ( cat_1, a_1 ) - local morphism_attr_1_1, deduped_3_1, deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1, deduped_8_1; - deduped_8_1 := 1 * 1; - deduped_7_1 := Dimension( a_1 ); - deduped_6_1 := UnderlyingRing( cat_1 ); - deduped_5_1 := 1 * deduped_7_1; - deduped_4_1 := HomalgIdentityMatrix( deduped_7_1, deduped_6_1 ); - deduped_3_1 := HomalgIdentityMatrix( 1, deduped_6_1 ); - morphism_attr_1_1 := KroneckerMat( ConvertMatrixToRow( deduped_3_1 ), deduped_4_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_8_1 ], function ( i_2 ) + local deduped_2_1, deduped_3_1, deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1; + deduped_7_1 := 1 * 1; + deduped_6_1 := Dimension( a_1 ); + deduped_5_1 := UnderlyingRing( cat_1 ); + deduped_4_1 := 1 * deduped_6_1; + deduped_3_1 := HomalgIdentityMatrix( deduped_6_1, deduped_5_1 ); + deduped_2_1 := HomalgIdentityMatrix( 1, deduped_5_1 ); + return CreateCapCategoryMorphismWithAttributes( cat_1, a_1, a_1, UnderlyingMatrix, KroneckerMat( ConvertMatrixToRow( deduped_2_1 ), deduped_3_1 ) * KroneckerMat( 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, 1 ) * 1 + QUO_INT( deduped_1_2, 1 ) + 1); + end ) ), deduped_7_1 ), deduped_7_1, deduped_7_1, deduped_5_1 ), deduped_3_1 ) * KroneckerMat( deduped_2_1, 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, 1 ) * 1 + QUO_INT( deduped_1_2, 1 ) + 1); - end ) ), deduped_8_1 ), deduped_8_1, deduped_8_1, deduped_6_1 ), deduped_4_1 ) * KroneckerMat( deduped_3_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, deduped_7_1 ) * 1 + QUO_INT( deduped_1_2, deduped_7_1 ) + 1); - end ) ), deduped_5_1 ), deduped_5_1, deduped_5_1, deduped_6_1 ) ) * KroneckerMat( TransposedMatrix( deduped_3_1 ), deduped_4_1 ); - return CreateCapCategoryMorphismWithAttributes( cat_1, a_1, CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberColumns( morphism_attr_1_1 ) ), UnderlyingMatrix, morphism_attr_1_1 ); + return (REM_INT( deduped_1_2, deduped_6_1 ) * 1 + QUO_INT( deduped_1_2, deduped_6_1 ) + 1); + end ) ), deduped_4_1 ), deduped_4_1, deduped_4_1, deduped_5_1 ) ) * KroneckerMat( TransposedMatrix( deduped_2_1 ), deduped_3_1 ) ); end ######## - , 5526 : IsPrecompiledDerivation := true ); + , 5220 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromObjectToInternalHomWithGivenInternalHom( cat, ######## function ( cat_1, a_1, r_1 ) - local morphism_attr_1_1, deduped_3_1, deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1, deduped_8_1; - deduped_8_1 := 1 * 1; - deduped_7_1 := Dimension( a_1 ); - deduped_6_1 := UnderlyingRing( cat_1 ); - deduped_5_1 := 1 * deduped_7_1; - deduped_4_1 := HomalgIdentityMatrix( deduped_7_1, deduped_6_1 ); - deduped_3_1 := HomalgIdentityMatrix( 1, deduped_6_1 ); - morphism_attr_1_1 := KroneckerMat( ConvertMatrixToRow( deduped_3_1 ), deduped_4_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_8_1 ], function ( i_2 ) + local deduped_2_1, deduped_3_1, deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1; + deduped_7_1 := 1 * 1; + deduped_6_1 := Dimension( a_1 ); + deduped_5_1 := UnderlyingRing( cat_1 ); + deduped_4_1 := 1 * deduped_6_1; + deduped_3_1 := HomalgIdentityMatrix( deduped_6_1, deduped_5_1 ); + deduped_2_1 := HomalgIdentityMatrix( 1, deduped_5_1 ); + return CreateCapCategoryMorphismWithAttributes( cat_1, a_1, r_1, UnderlyingMatrix, KroneckerMat( ConvertMatrixToRow( deduped_2_1 ), deduped_3_1 ) * KroneckerMat( 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, 1 ) * 1 + QUO_INT( deduped_1_2, 1 ) + 1); + end ) ), deduped_7_1 ), deduped_7_1, deduped_7_1, deduped_5_1 ), deduped_3_1 ) * KroneckerMat( deduped_2_1, 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, 1 ) * 1 + QUO_INT( deduped_1_2, 1 ) + 1); - end ) ), deduped_8_1 ), deduped_8_1, deduped_8_1, deduped_6_1 ), deduped_4_1 ) * KroneckerMat( deduped_3_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, deduped_7_1 ) * 1 + QUO_INT( deduped_1_2, deduped_7_1 ) + 1); - end ) ), deduped_5_1 ), deduped_5_1, deduped_5_1, deduped_6_1 ) ) * KroneckerMat( TransposedMatrix( deduped_3_1 ), deduped_4_1 ); - return CreateCapCategoryMorphismWithAttributes( cat_1, a_1, CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberColumns( morphism_attr_1_1 ) ), UnderlyingMatrix, morphism_attr_1_1 ); + return (REM_INT( deduped_1_2, deduped_6_1 ) * 1 + QUO_INT( deduped_1_2, deduped_6_1 ) + 1); + end ) ), deduped_4_1 ), deduped_4_1, deduped_4_1, deduped_5_1 ) ) * KroneckerMat( TransposedMatrix( deduped_2_1 ), deduped_3_1 ) ); end ######## - , 5525 : IsPrecompiledDerivation := true ); + , 5219 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromPushoutToCoequalizerOfCoproductDiagram( cat, @@ -3767,206 +3763,182 @@ end ######## function ( cat_1, a_1, b_1, c_1 ) - local morphism_attr_1_1, deduped_7_1, deduped_8_1, deduped_9_1, deduped_10_1, deduped_11_1, deduped_12_1, deduped_13_1, deduped_14_1, deduped_15_1, deduped_16_1, deduped_17_1, deduped_18_1, deduped_19_1, deduped_20_1; - deduped_20_1 := Dimension( b_1 ); - deduped_19_1 := Dimension( a_1 ); - deduped_18_1 := UnderlyingRing( cat_1 ); - deduped_17_1 := Dimension( c_1 ); - deduped_16_1 := deduped_17_1 * deduped_17_1; - deduped_15_1 := deduped_20_1 * deduped_17_1; - deduped_14_1 := deduped_19_1 * deduped_20_1; - deduped_13_1 := HomalgIdentityMatrix( deduped_20_1, deduped_18_1 ); - deduped_12_1 := HomalgIdentityMatrix( deduped_17_1, deduped_18_1 ); - deduped_11_1 := deduped_15_1 * deduped_14_1; - deduped_10_1 := deduped_17_1 * deduped_14_1; - deduped_9_1 := deduped_14_1 * deduped_20_1; - deduped_8_1 := HomalgIdentityMatrix( deduped_11_1, deduped_18_1 ); - deduped_7_1 := deduped_11_1 * deduped_17_1; - morphism_attr_1_1 := KroneckerMat( TransposedMatrix( deduped_12_1 ), KroneckerMat( HomalgIdentityMatrix( deduped_19_1, deduped_18_1 ), ConvertMatrixToRow( deduped_13_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_14_1 ], function ( i_2 ) + local morphism_attr_1_1, deduped_8_1, deduped_9_1, deduped_10_1, deduped_11_1, deduped_12_1, deduped_13_1, deduped_14_1, deduped_15_1, deduped_16_1, deduped_17_1, deduped_18_1, deduped_19_1; + deduped_19_1 := Dimension( b_1 ); + deduped_18_1 := Dimension( a_1 ); + deduped_17_1 := UnderlyingRing( cat_1 ); + deduped_16_1 := Dimension( c_1 ); + deduped_15_1 := deduped_16_1 * deduped_16_1; + deduped_14_1 := deduped_19_1 * deduped_16_1; + deduped_13_1 := deduped_18_1 * deduped_19_1; + deduped_12_1 := HomalgIdentityMatrix( deduped_19_1, deduped_17_1 ); + deduped_11_1 := HomalgIdentityMatrix( deduped_16_1, deduped_17_1 ); + deduped_10_1 := deduped_13_1 * deduped_14_1; + deduped_9_1 := HomalgIdentityMatrix( deduped_10_1, deduped_17_1 ); + deduped_8_1 := deduped_10_1 * deduped_16_1; + morphism_attr_1_1 := KroneckerMat( TransposedMatrix( deduped_11_1 ), KroneckerMat( HomalgIdentityMatrix( deduped_18_1, deduped_17_1 ), ConvertMatrixToRow( deduped_12_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_13_1 ], function ( i_2 ) + local deduped_1_2; + deduped_1_2 := (i_2 - 1); + return (REM_INT( deduped_1_2, deduped_19_1 ) * deduped_18_1 + QUO_INT( deduped_1_2, deduped_19_1 ) + 1); + end ) ), deduped_13_1 ), deduped_13_1, deduped_13_1, deduped_17_1 ), deduped_12_1 ) * KroneckerMat( HomalgIdentityMatrix( (deduped_19_1 * deduped_18_1), deduped_17_1 ), deduped_12_1 ) * KroneckerMat( HomalgIdentityMatrix( deduped_13_1, deduped_17_1 ), (KroneckerMat( deduped_12_1, ConvertMatrixToRow( deduped_11_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_14_1 ], function ( i_2 ) local deduped_1_2; deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_20_1 ) * deduped_19_1 + QUO_INT( deduped_1_2, deduped_20_1 ) + 1); - end ) ), deduped_14_1 ), deduped_14_1, deduped_14_1, deduped_18_1 ), deduped_13_1 ) * KroneckerMat( HomalgIdentityMatrix( (deduped_20_1 * deduped_19_1), deduped_18_1 ), deduped_13_1 ) * HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_9_1 ], function ( i_2 ) + return (REM_INT( deduped_1_2, deduped_16_1 ) * deduped_19_1 + QUO_INT( deduped_1_2, deduped_16_1 ) + 1); + end ) ), deduped_14_1 ), deduped_14_1, deduped_14_1, deduped_17_1 ), deduped_11_1 ) * KroneckerMat( HomalgIdentityMatrix( (deduped_16_1 * deduped_19_1), deduped_17_1 ), deduped_11_1 )) ) ) * (KroneckerMat( deduped_11_1, HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_8_1 ], function ( i_2 ) local deduped_1_2; deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_20_1 ) * deduped_14_1 + QUO_INT( deduped_1_2, deduped_20_1 ) + 1); - end ) ), deduped_9_1 ), deduped_9_1, deduped_9_1, deduped_18_1 ) * KroneckerMat( (KroneckerMat( deduped_13_1, ConvertMatrixToRow( deduped_12_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_15_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_17_1 ) * deduped_20_1 + QUO_INT( deduped_1_2, deduped_17_1 ) + 1); - end ) ), deduped_15_1 ), deduped_15_1, deduped_15_1, deduped_18_1 ), deduped_12_1 ) * KroneckerMat( HomalgIdentityMatrix( (deduped_17_1 * deduped_20_1), deduped_18_1 ), deduped_12_1 )), HomalgIdentityMatrix( deduped_14_1, deduped_18_1 ) ) * KroneckerMat( HomalgIdentityMatrix( deduped_15_1, deduped_18_1 ), HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_10_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_14_1 ) * deduped_17_1 + QUO_INT( deduped_1_2, deduped_14_1 ) + 1); - end ) ), deduped_10_1 ), deduped_10_1, deduped_10_1, deduped_18_1 ) ) ) * (KroneckerMat( deduped_12_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, deduped_17_1 ) * deduped_11_1 + QUO_INT( deduped_1_2, deduped_17_1 ) + 1); - end ) ), deduped_7_1 ), deduped_7_1, deduped_7_1, deduped_18_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_16_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_17_1 ) * deduped_17_1 + QUO_INT( deduped_1_2, deduped_17_1 ) + 1); - end ) ), deduped_16_1 ), deduped_16_1, deduped_16_1, deduped_18_1 ), deduped_8_1 ) * KroneckerMat( ConvertMatrixToColumn( deduped_12_1 ), deduped_8_1 )); + return (REM_INT( deduped_1_2, deduped_16_1 ) * deduped_10_1 + QUO_INT( deduped_1_2, deduped_16_1 ) + 1); + end ) ), deduped_8_1 ), deduped_8_1, deduped_8_1, deduped_17_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_15_1 ], function ( i_2 ) + local deduped_1_2; + deduped_1_2 := (i_2 - 1); + return (REM_INT( deduped_1_2, deduped_16_1 ) * deduped_16_1 + QUO_INT( deduped_1_2, deduped_16_1 ) + 1); + end ) ), deduped_15_1 ), deduped_15_1, deduped_15_1, deduped_17_1 ), deduped_9_1 ) * KroneckerMat( ConvertMatrixToColumn( deduped_11_1 ), deduped_9_1 )) * HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_10_1 ], function ( i_2 ) + local deduped_1_2; + deduped_1_2 := (i_2 - 1); + return (REM_INT( deduped_1_2, deduped_14_1 ) * deduped_13_1 + QUO_INT( deduped_1_2, deduped_14_1 ) + 1); + end ) ), deduped_10_1 ), deduped_10_1, deduped_10_1, deduped_17_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 ######## - , 14358 : IsPrecompiledDerivation := true ); + , 14158 : IsPrecompiledDerivation := true ); ## AddMonoidalPreCoComposeMorphismWithGivenObjects( cat, ######## function ( cat_1, s_1, a_1, b_1, c_1, r_1 ) - local deduped_6_1, deduped_7_1, deduped_8_1, deduped_9_1, deduped_10_1, deduped_11_1, deduped_12_1, deduped_13_1, deduped_14_1, deduped_15_1, deduped_16_1, deduped_17_1, deduped_18_1, deduped_19_1; - deduped_19_1 := Dimension( r_1 ); + local deduped_7_1, deduped_8_1, deduped_9_1, deduped_10_1, deduped_11_1, deduped_12_1, deduped_13_1, deduped_14_1, deduped_15_1, deduped_16_1, deduped_17_1, deduped_18_1; deduped_18_1 := Dimension( b_1 ); deduped_17_1 := Dimension( a_1 ); deduped_16_1 := UnderlyingRing( cat_1 ); deduped_15_1 := Dimension( c_1 ); - deduped_14_1 := HomalgIdentityMatrix( deduped_19_1, deduped_16_1 ); - deduped_13_1 := deduped_15_1 * deduped_15_1; - deduped_12_1 := deduped_19_1 * deduped_15_1; - deduped_11_1 := deduped_18_1 * deduped_15_1; - deduped_10_1 := deduped_17_1 * deduped_18_1; - deduped_9_1 := HomalgIdentityMatrix( deduped_18_1, deduped_16_1 ); - deduped_8_1 := HomalgIdentityMatrix( deduped_15_1, deduped_16_1 ); - deduped_7_1 := deduped_15_1 * deduped_10_1; - deduped_6_1 := deduped_10_1 * deduped_18_1; - return CreateCapCategoryMorphismWithAttributes( cat_1, s_1, r_1, UnderlyingMatrix, KroneckerMat( TransposedMatrix( deduped_8_1 ), KroneckerMat( HomalgIdentityMatrix( deduped_17_1, deduped_16_1 ), ConvertMatrixToRow( deduped_9_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_10_1 ], function ( i_2 ) + deduped_14_1 := deduped_15_1 * deduped_15_1; + deduped_13_1 := deduped_18_1 * deduped_15_1; + deduped_12_1 := deduped_17_1 * deduped_18_1; + deduped_11_1 := HomalgIdentityMatrix( deduped_18_1, deduped_16_1 ); + deduped_10_1 := HomalgIdentityMatrix( deduped_15_1, deduped_16_1 ); + deduped_9_1 := deduped_12_1 * deduped_13_1; + deduped_8_1 := HomalgIdentityMatrix( deduped_9_1, deduped_16_1 ); + deduped_7_1 := deduped_9_1 * deduped_15_1; + return CreateCapCategoryMorphismWithAttributes( cat_1, s_1, r_1, UnderlyingMatrix, KroneckerMat( TransposedMatrix( deduped_10_1 ), KroneckerMat( HomalgIdentityMatrix( deduped_17_1, deduped_16_1 ), ConvertMatrixToRow( deduped_11_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_12_1 ], function ( i_2 ) + local deduped_1_2; + deduped_1_2 := (i_2 - 1); + return (REM_INT( deduped_1_2, deduped_18_1 ) * deduped_17_1 + QUO_INT( deduped_1_2, deduped_18_1 ) + 1); + end ) ), deduped_12_1 ), deduped_12_1, deduped_12_1, deduped_16_1 ), deduped_11_1 ) * KroneckerMat( HomalgIdentityMatrix( (deduped_18_1 * deduped_17_1), deduped_16_1 ), deduped_11_1 ) * KroneckerMat( HomalgIdentityMatrix( deduped_12_1, deduped_16_1 ), (KroneckerMat( deduped_11_1, ConvertMatrixToRow( deduped_10_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_13_1 ], function ( i_2 ) local deduped_1_2; deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_18_1 ) * deduped_17_1 + QUO_INT( deduped_1_2, deduped_18_1 ) + 1); - end ) ), deduped_10_1 ), deduped_10_1, deduped_10_1, deduped_16_1 ), deduped_9_1 ) * KroneckerMat( HomalgIdentityMatrix( (deduped_18_1 * deduped_17_1), deduped_16_1 ), deduped_9_1 ) * HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_6_1 ], function ( i_2 ) + return (REM_INT( deduped_1_2, deduped_15_1 ) * deduped_18_1 + QUO_INT( deduped_1_2, deduped_15_1 ) + 1); + end ) ), deduped_13_1 ), deduped_13_1, deduped_13_1, deduped_16_1 ), deduped_10_1 ) * KroneckerMat( HomalgIdentityMatrix( (deduped_15_1 * deduped_18_1), deduped_16_1 ), deduped_10_1 )) ) ) * (KroneckerMat( deduped_10_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, deduped_18_1 ) * deduped_10_1 + QUO_INT( deduped_1_2, deduped_18_1 ) + 1); - end ) ), deduped_6_1 ), deduped_6_1, deduped_6_1, deduped_16_1 ) * KroneckerMat( (KroneckerMat( deduped_9_1, ConvertMatrixToRow( deduped_8_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_11_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_15_1 ) * deduped_18_1 + QUO_INT( deduped_1_2, deduped_15_1 ) + 1); - end ) ), deduped_11_1 ), deduped_11_1, deduped_11_1, deduped_16_1 ), deduped_8_1 ) * KroneckerMat( HomalgIdentityMatrix( (deduped_15_1 * deduped_18_1), deduped_16_1 ), deduped_8_1 )), HomalgIdentityMatrix( deduped_10_1, deduped_16_1 ) ) * KroneckerMat( HomalgIdentityMatrix( deduped_11_1, deduped_16_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, deduped_10_1 ) * deduped_15_1 + QUO_INT( deduped_1_2, deduped_10_1 ) + 1); - end ) ), deduped_7_1 ), deduped_7_1, deduped_7_1, deduped_16_1 ) ) ) * (KroneckerMat( deduped_8_1, HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_12_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_15_1 ) * deduped_19_1 + QUO_INT( deduped_1_2, deduped_15_1 ) + 1); - end ) ), deduped_12_1 ), deduped_12_1, deduped_12_1, deduped_16_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_13_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_15_1 ) * deduped_15_1 + QUO_INT( deduped_1_2, deduped_15_1 ) + 1); - end ) ), deduped_13_1 ), deduped_13_1, deduped_13_1, deduped_16_1 ), deduped_14_1 ) * KroneckerMat( ConvertMatrixToColumn( deduped_8_1 ), deduped_14_1 )) ); + return (REM_INT( deduped_1_2, deduped_15_1 ) * deduped_9_1 + QUO_INT( deduped_1_2, deduped_15_1 ) + 1); + end ) ), deduped_7_1 ), deduped_7_1, deduped_7_1, deduped_16_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_14_1 ], function ( i_2 ) + local deduped_1_2; + deduped_1_2 := (i_2 - 1); + return (REM_INT( deduped_1_2, deduped_15_1 ) * deduped_15_1 + QUO_INT( deduped_1_2, deduped_15_1 ) + 1); + end ) ), deduped_14_1 ), deduped_14_1, deduped_14_1, deduped_16_1 ), deduped_8_1 ) * KroneckerMat( ConvertMatrixToColumn( deduped_10_1 ), deduped_8_1 )) * HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_9_1 ], function ( i_2 ) + local deduped_1_2; + deduped_1_2 := (i_2 - 1); + return (REM_INT( deduped_1_2, deduped_13_1 ) * deduped_12_1 + QUO_INT( deduped_1_2, deduped_13_1 ) + 1); + end ) ), deduped_9_1 ), deduped_9_1, deduped_9_1, deduped_16_1 ) ); end ######## - , 13351 : IsPrecompiledDerivation := true ); + , 13151 : IsPrecompiledDerivation := true ); ## AddMonoidalPreComposeMorphism( cat, ######## function ( cat_1, a_1, b_1, c_1 ) - local morphism_attr_1_1, deduped_7_1, deduped_8_1, deduped_9_1, deduped_10_1, deduped_11_1, deduped_12_1, deduped_13_1, deduped_14_1, deduped_15_1, deduped_16_1, deduped_17_1, deduped_18_1, deduped_19_1, deduped_20_1, deduped_21_1, deduped_22_1; - deduped_22_1 := Dimension( c_1 ); - deduped_21_1 := Dimension( b_1 ); - deduped_20_1 := UnderlyingRing( cat_1 ); - deduped_19_1 := Dimension( a_1 ); - deduped_18_1 := HomalgIdentityMatrix( deduped_21_1, deduped_20_1 ); - deduped_17_1 := deduped_19_1 * deduped_19_1; - deduped_16_1 := deduped_21_1 * deduped_22_1; - deduped_15_1 := deduped_19_1 * deduped_21_1; - deduped_14_1 := HomalgIdentityMatrix( deduped_19_1, deduped_20_1 ); - deduped_13_1 := deduped_21_1 * deduped_16_1; - deduped_12_1 := HomalgIdentityMatrix( deduped_16_1, deduped_20_1 ); - deduped_11_1 := deduped_16_1 * deduped_19_1; - deduped_10_1 := HomalgIdentityMatrix( deduped_15_1, deduped_20_1 ); - deduped_9_1 := deduped_15_1 * deduped_16_1; - deduped_8_1 := deduped_19_1 * deduped_9_1; - deduped_7_1 := HomalgIdentityMatrix( deduped_9_1, deduped_20_1 ); - morphism_attr_1_1 := KroneckerMat( ConvertMatrixToRow( deduped_14_1 ), deduped_7_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_17_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_19_1 ) * deduped_19_1 + QUO_INT( deduped_1_2, deduped_19_1 ) + 1); - end ) ), deduped_17_1 ), deduped_17_1, deduped_17_1, deduped_20_1 ), deduped_7_1 ) * KroneckerMat( deduped_14_1, HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_8_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_9_1 ) * deduped_19_1 + QUO_INT( deduped_1_2, deduped_9_1 ) + 1); - end ) ), deduped_8_1 ), deduped_8_1, deduped_8_1, deduped_20_1 ) ) * KroneckerMat( TransposedMatrix( deduped_14_1 ), (KroneckerMat( deduped_10_1, HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_11_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_19_1 ) * deduped_16_1 + QUO_INT( deduped_1_2, deduped_19_1 ) + 1); - end ) ), deduped_11_1 ), deduped_11_1, deduped_11_1, deduped_20_1 ) ) * KroneckerMat( (KroneckerMat( deduped_10_1, deduped_14_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_15_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_21_1 ) * deduped_19_1 + QUO_INT( deduped_1_2, deduped_21_1 ) + 1); - end ) ), deduped_15_1 ), deduped_15_1, deduped_15_1, deduped_20_1 ), deduped_14_1 ) * KroneckerMat( deduped_18_1, ConvertMatrixToColumn( deduped_14_1 ) )), deduped_12_1 ) * HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_13_1 ], function ( i_2 ) + local morphism_attr_1_1, deduped_8_1, deduped_9_1, deduped_10_1, deduped_11_1, deduped_12_1, deduped_13_1, deduped_14_1, deduped_15_1, deduped_16_1, deduped_17_1, deduped_18_1, deduped_19_1, deduped_20_1, deduped_21_1; + deduped_21_1 := UnderlyingRing( cat_1 ); + deduped_20_1 := Dimension( c_1 ); + deduped_19_1 := Dimension( b_1 ); + deduped_18_1 := Dimension( a_1 ); + deduped_17_1 := HomalgIdentityMatrix( deduped_19_1, deduped_21_1 ); + deduped_16_1 := deduped_18_1 * deduped_18_1; + deduped_15_1 := HomalgIdentityMatrix( deduped_18_1, deduped_21_1 ); + deduped_14_1 := deduped_19_1 * deduped_20_1; + deduped_13_1 := deduped_18_1 * deduped_19_1; + deduped_12_1 := HomalgIdentityMatrix( deduped_14_1, deduped_21_1 ); + deduped_11_1 := deduped_14_1 * deduped_13_1; + deduped_10_1 := deduped_13_1 * deduped_14_1; + deduped_9_1 := deduped_18_1 * deduped_11_1; + deduped_8_1 := HomalgIdentityMatrix( deduped_11_1, deduped_21_1 ); + morphism_attr_1_1 := HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_10_1 ], function ( i_2 ) + local deduped_1_2; + deduped_1_2 := (i_2 - 1); + return (REM_INT( deduped_1_2, deduped_14_1 ) * deduped_13_1 + QUO_INT( deduped_1_2, deduped_14_1 ) + 1); + end ) ), deduped_10_1 ), deduped_10_1, deduped_10_1, deduped_21_1 ) * (KroneckerMat( ConvertMatrixToRow( deduped_15_1 ), deduped_8_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_16_1 ], function ( i_2 ) + local deduped_1_2; + deduped_1_2 := (i_2 - 1); + return (REM_INT( deduped_1_2, deduped_18_1 ) * deduped_18_1 + QUO_INT( deduped_1_2, deduped_18_1 ) + 1); + end ) ), deduped_16_1 ), deduped_16_1, deduped_16_1, deduped_21_1 ), deduped_8_1 ) * KroneckerMat( deduped_15_1, HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_9_1 ], function ( i_2 ) local deduped_1_2; deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_16_1 ) * deduped_21_1 + QUO_INT( deduped_1_2, deduped_16_1 ) + 1); - end ) ), deduped_13_1 ), deduped_13_1, deduped_13_1, deduped_20_1 ) * (KroneckerMat( deduped_12_1, deduped_18_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_16_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_22_1 ) * deduped_21_1 + QUO_INT( deduped_1_2, deduped_22_1 ) + 1); - end ) ), deduped_16_1 ), deduped_16_1, deduped_16_1, deduped_20_1 ), deduped_18_1 ) * KroneckerMat( HomalgIdentityMatrix( deduped_22_1, deduped_20_1 ), ConvertMatrixToColumn( deduped_18_1 ) ))) ); + return (REM_INT( deduped_1_2, deduped_11_1 ) * deduped_18_1 + QUO_INT( deduped_1_2, deduped_11_1 ) + 1); + end ) ), deduped_9_1 ), deduped_9_1, deduped_9_1, deduped_21_1 ) ) * KroneckerMat( TransposedMatrix( deduped_15_1 ), (KroneckerMat( deduped_12_1, KroneckerMat( HomalgIdentityMatrix( deduped_13_1, deduped_21_1 ), deduped_15_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_13_1 ], function ( i_2 ) + local deduped_1_2; + deduped_1_2 := (i_2 - 1); + return (REM_INT( deduped_1_2, deduped_19_1 ) * deduped_18_1 + QUO_INT( deduped_1_2, deduped_19_1 ) + 1); + end ) ), deduped_13_1 ), deduped_13_1, deduped_13_1, deduped_21_1 ), deduped_15_1 ) * KroneckerMat( deduped_17_1, ConvertMatrixToColumn( deduped_15_1 ) ) ) * (KroneckerMat( deduped_12_1, deduped_17_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_14_1 ], function ( i_2 ) + local deduped_1_2; + deduped_1_2 := (i_2 - 1); + return (REM_INT( deduped_1_2, deduped_20_1 ) * deduped_19_1 + QUO_INT( deduped_1_2, deduped_20_1 ) + 1); + end ) ), deduped_14_1 ), deduped_14_1, deduped_14_1, deduped_21_1 ), deduped_17_1 ) * KroneckerMat( HomalgIdentityMatrix( deduped_20_1, deduped_21_1 ), ConvertMatrixToColumn( deduped_17_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 ######## - , 14358 : IsPrecompiledDerivation := true ); + , 14158 : IsPrecompiledDerivation := true ); ## AddMonoidalPreComposeMorphismWithGivenObjects( cat, ######## function ( cat_1, s_1, a_1, b_1, c_1, r_1 ) - local deduped_6_1, deduped_7_1, deduped_8_1, deduped_9_1, deduped_10_1, deduped_11_1, deduped_12_1, deduped_13_1, deduped_14_1, deduped_15_1, deduped_16_1, deduped_17_1, deduped_18_1, deduped_19_1, deduped_20_1, deduped_21_1; - deduped_21_1 := Dimension( c_1 ); - deduped_20_1 := Dimension( b_1 ); - deduped_19_1 := Dimension( s_1 ); - deduped_18_1 := UnderlyingRing( cat_1 ); - deduped_17_1 := Dimension( a_1 ); - deduped_16_1 := HomalgIdentityMatrix( deduped_20_1, deduped_18_1 ); - deduped_15_1 := deduped_20_1 * deduped_21_1; - deduped_14_1 := deduped_17_1 * deduped_20_1; - deduped_13_1 := deduped_17_1 * deduped_19_1; - deduped_12_1 := deduped_17_1 * deduped_17_1; - deduped_11_1 := HomalgIdentityMatrix( deduped_19_1, deduped_18_1 ); - deduped_10_1 := HomalgIdentityMatrix( deduped_17_1, deduped_18_1 ); - deduped_9_1 := deduped_20_1 * deduped_15_1; - deduped_8_1 := HomalgIdentityMatrix( deduped_15_1, deduped_18_1 ); - deduped_7_1 := deduped_15_1 * deduped_17_1; - deduped_6_1 := HomalgIdentityMatrix( deduped_14_1, deduped_18_1 ); - return CreateCapCategoryMorphismWithAttributes( cat_1, s_1, r_1, UnderlyingMatrix, KroneckerMat( ConvertMatrixToRow( deduped_10_1 ), deduped_11_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_12_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_17_1 ) * deduped_17_1 + QUO_INT( deduped_1_2, deduped_17_1 ) + 1); - end ) ), deduped_12_1 ), deduped_12_1, deduped_12_1, deduped_18_1 ), deduped_11_1 ) * KroneckerMat( deduped_10_1, HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_13_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_19_1 ) * deduped_17_1 + QUO_INT( deduped_1_2, deduped_19_1 ) + 1); - end ) ), deduped_13_1 ), deduped_13_1, deduped_13_1, deduped_18_1 ) ) * KroneckerMat( TransposedMatrix( deduped_10_1 ), (KroneckerMat( deduped_6_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, deduped_17_1 ) * deduped_15_1 + QUO_INT( deduped_1_2, deduped_17_1 ) + 1); - end ) ), deduped_7_1 ), deduped_7_1, deduped_7_1, deduped_18_1 ) ) * KroneckerMat( (KroneckerMat( deduped_6_1, deduped_10_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_14_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_20_1 ) * deduped_17_1 + QUO_INT( deduped_1_2, deduped_20_1 ) + 1); - end ) ), deduped_14_1 ), deduped_14_1, deduped_14_1, deduped_18_1 ), deduped_10_1 ) * KroneckerMat( deduped_16_1, ConvertMatrixToColumn( deduped_10_1 ) )), deduped_8_1 ) * HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_9_1 ], function ( i_2 ) + local deduped_7_1, deduped_8_1, deduped_9_1, deduped_10_1, deduped_11_1, deduped_12_1, deduped_13_1, deduped_14_1, deduped_15_1, deduped_16_1, deduped_17_1, deduped_18_1, deduped_19_1, deduped_20_1; + deduped_20_1 := Dimension( c_1 ); + deduped_19_1 := Dimension( b_1 ); + deduped_18_1 := Dimension( a_1 ); + deduped_17_1 := UnderlyingRing( cat_1 ); + deduped_16_1 := Dimension( s_1 ); + deduped_15_1 := HomalgIdentityMatrix( deduped_19_1, deduped_17_1 ); + deduped_14_1 := deduped_18_1 * deduped_18_1; + deduped_13_1 := deduped_18_1 * deduped_19_1; + deduped_12_1 := deduped_19_1 * deduped_20_1; + deduped_11_1 := HomalgIdentityMatrix( deduped_18_1, deduped_17_1 ); + deduped_10_1 := HomalgIdentityMatrix( deduped_12_1, deduped_17_1 ); + deduped_9_1 := deduped_12_1 * deduped_13_1; + deduped_8_1 := deduped_18_1 * deduped_9_1; + deduped_7_1 := HomalgIdentityMatrix( deduped_9_1, deduped_17_1 ); + return CreateCapCategoryMorphismWithAttributes( cat_1, s_1, r_1, UnderlyingMatrix, HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_16_1 ], function ( i_2 ) + local deduped_1_2; + deduped_1_2 := (i_2 - 1); + return (REM_INT( deduped_1_2, deduped_12_1 ) * deduped_13_1 + QUO_INT( deduped_1_2, deduped_12_1 ) + 1); + end ) ), deduped_16_1 ), deduped_16_1, deduped_16_1, deduped_17_1 ) * (KroneckerMat( ConvertMatrixToRow( deduped_11_1 ), deduped_7_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_14_1 ], function ( i_2 ) + local deduped_1_2; + deduped_1_2 := (i_2 - 1); + return (REM_INT( deduped_1_2, deduped_18_1 ) * deduped_18_1 + QUO_INT( deduped_1_2, deduped_18_1 ) + 1); + end ) ), deduped_14_1 ), deduped_14_1, deduped_14_1, deduped_17_1 ), deduped_7_1 ) * KroneckerMat( deduped_11_1, HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_8_1 ], function ( i_2 ) local deduped_1_2; deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_15_1 ) * deduped_20_1 + QUO_INT( deduped_1_2, deduped_15_1 ) + 1); - end ) ), deduped_9_1 ), deduped_9_1, deduped_9_1, deduped_18_1 ) * (KroneckerMat( deduped_8_1, deduped_16_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_15_1 ], function ( i_2 ) - local deduped_1_2; - deduped_1_2 := (i_2 - 1); - return (REM_INT( deduped_1_2, deduped_21_1 ) * deduped_20_1 + QUO_INT( deduped_1_2, deduped_21_1 ) + 1); - end ) ), deduped_15_1 ), deduped_15_1, deduped_15_1, deduped_18_1 ), deduped_16_1 ) * KroneckerMat( HomalgIdentityMatrix( deduped_21_1, deduped_18_1 ), ConvertMatrixToColumn( deduped_16_1 ) ))) ) ); + return (REM_INT( deduped_1_2, deduped_9_1 ) * deduped_18_1 + QUO_INT( deduped_1_2, deduped_9_1 ) + 1); + end ) ), deduped_8_1 ), deduped_8_1, deduped_8_1, deduped_17_1 ) ) * KroneckerMat( TransposedMatrix( deduped_11_1 ), (KroneckerMat( deduped_10_1, KroneckerMat( HomalgIdentityMatrix( deduped_13_1, deduped_17_1 ), deduped_11_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_13_1 ], function ( i_2 ) + local deduped_1_2; + deduped_1_2 := (i_2 - 1); + return (REM_INT( deduped_1_2, deduped_19_1 ) * deduped_18_1 + QUO_INT( deduped_1_2, deduped_19_1 ) + 1); + end ) ), deduped_13_1 ), deduped_13_1, deduped_13_1, deduped_17_1 ), deduped_11_1 ) * KroneckerMat( deduped_15_1, ConvertMatrixToColumn( deduped_11_1 ) ) ) * (KroneckerMat( deduped_10_1, deduped_15_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_12_1 ], function ( i_2 ) + local deduped_1_2; + deduped_1_2 := (i_2 - 1); + return (REM_INT( deduped_1_2, deduped_20_1 ) * deduped_19_1 + QUO_INT( deduped_1_2, deduped_20_1 ) + 1); + end ) ), deduped_12_1 ), deduped_12_1, deduped_12_1, deduped_17_1 ), deduped_15_1 ) * KroneckerMat( HomalgIdentityMatrix( deduped_20_1, deduped_17_1 ), ConvertMatrixToColumn( deduped_15_1 ) ))) )) ); end ######## - , 13351 : IsPrecompiledDerivation := true ); + , 13151 : IsPrecompiledDerivation := true ); ## AddMonomorphismIntoSomeInjectiveObject( cat, diff --git a/MonoidalCategories/PackageInfo.g b/MonoidalCategories/PackageInfo.g index 3fd973dce2..ec00fcdcdc 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.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", diff --git a/MonoidalCategories/gap/BraidedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/BraidedMonoidalCategoriesDerivedMethods.gi index a65805d5b3..bd4328903b 100644 --- a/MonoidalCategories/gap/BraidedMonoidalCategoriesDerivedMethods.gi +++ b/MonoidalCategories/gap/BraidedMonoidalCategoriesDerivedMethods.gi @@ -8,11 +8,11 @@ AddDerivationToCAP( BraidingInverseWithGivenTensorProducts, "BraidingInverseWithGivenTensorProducts as the inverse of the braiding", [ [ InverseForMorphisms, 1 ], - [ Braiding, 1 ] ], + [ BraidingWithGivenTensorProducts, 1 ] ], function( cat, object_2_tensored_object_1, object_1, object_2, object_1_tensored_object_2 ) - ##TODO: Use BraidingWithGiven - return InverseForMorphisms( cat, Braiding( cat, object_1, object_2 ) ); + + return InverseForMorphisms( cat, BraidingWithGivenTensorProducts( cat, object_1_tensored_object_2, object_1, object_2, object_2_tensored_object_1 ) ); end : CategoryFilter := IsBraidedMonoidalCategory ); @@ -20,10 +20,11 @@ end : CategoryFilter := IsBraidedMonoidalCategory ); AddDerivationToCAP( BraidingWithGivenTensorProducts, "BraidingWithGivenTensorProducts as the inverse of BraidingInverse", [ [ InverseForMorphisms, 1 ], - [ BraidingInverse, 1 ] ], + [ BraidingInverseWithGivenTensorProducts, 1 ] ], function( cat, object_1_tensored_object_2, object_1, object_2, object_2_tensored_object_1 ) - ##TODO: Use BraidingInverseWithGiven - return InverseForMorphisms( cat, BraidingInverse( cat, object_1, object_2 ) ); + + return InverseForMorphisms( cat, BraidingInverseWithGivenTensorProducts( cat, object_2_tensored_object_1, object_1, object_2, object_1_tensored_object_2 ) ); end : CategoryFilter := IsBraidedMonoidalCategory ); + diff --git a/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi index 34e1bebdf7..833ea1d7cd 100644 --- a/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi +++ b/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi @@ -288,7 +288,7 @@ end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); ## AddDerivationToCAP( EvaluationForDualWithGivenTensorProduct, "EvaluationForDualWithGivenTensorProduct using the tensor hom adjunction and IsomorphismFromDualObjectToInternalHomIntoTensorUnit", - [ [ InternalHomToTensorProductAdjunctionMap, 1 ], + [ [ InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct, 1 ], [ IsomorphismFromDualObjectToInternalHomIntoTensorUnit, 1 ] ], function( cat, s, a, r ) @@ -297,8 +297,11 @@ AddDerivationToCAP( EvaluationForDualWithGivenTensorProduct, # # Adjoint( a^v → Hom(a,1) ) = ( a^v ⊗ a → 1 ) - return InternalHomToTensorProductAdjunctionMap( cat, a, r, - IsomorphismFromDualObjectToInternalHomIntoTensorUnit( cat, a ) ); + return InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct( cat, + a, + r, + IsomorphismFromDualObjectToInternalHomIntoTensorUnit( cat, a ), + s ); end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); @@ -528,14 +531,16 @@ end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); AddDerivationToCAP( IsomorphismFromObjectToInternalHomWithGivenInternalHom, "IsomorphismFromObjectToInternalHomWithGivenInternalHom using the coevaluation morphism", [ [ TensorUnit, 1 ], + [ TensorProductOnObjects, 1 ], + [ InternalHomOnObjects, 1 ], [ PreCompose, 1 ], - [ CoevaluationMorphism, 1 ], - [ InternalHomOnMorphisms, 1 ], + [ CoevaluationMorphismWithGivenRange, 1 ], + [ InternalHomOnMorphismsWithGivenInternalHoms, 1 ], [ IdentityMorphism, 1 ], - [ RightUnitor, 1 ] ], + [ RightUnitorWithGivenTensorProduct, 1 ] ], function( cat, a, internal_hom ) - local unit; + local unit, a_x_1, hom_1_ax1; # a # | @@ -548,12 +553,16 @@ AddDerivationToCAP( IsomorphismFromObjectToInternalHomWithGivenInternalHom, # Hom(1, a) unit := TensorUnit( cat ); + a_x_1 := TensorProductOnObjects( cat, a, unit ); + hom_1_ax1:= InternalHomOnObjects( cat, unit, a_x_1 ); return PreCompose( cat, - CoevaluationMorphism( cat, a, unit ), - InternalHomOnMorphisms( cat, - IdentityMorphism( cat, unit ), - RightUnitor( cat, a ) ) ); + CoevaluationMorphismWithGivenRange( cat, a, unit, hom_1_ax1 ), + InternalHomOnMorphismsWithGivenInternalHoms( cat, + hom_1_ax1, + IdentityMorphism( cat, unit ), + RightUnitorWithGivenTensorProduct( cat, a, a_x_1 ), + internal_hom ) ); end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); @@ -561,7 +570,7 @@ end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); AddDerivationToCAP( IsomorphismFromObjectToInternalHomWithGivenInternalHom, "IsomorphismFromObjectToInternalHomWithGivenInternalHom as the adjoint of the right unitor", [ [ TensorUnit, 1 ], - [ TensorProductToInternalHomAdjunctionMap, 1 ], + [ TensorProductToInternalHomAdjunctionMapWithGivenInternalHom, 1 ], [ RightUnitor, 1 ] ], function( cat, a, internal_hom ) @@ -570,10 +579,11 @@ AddDerivationToCAP( IsomorphismFromObjectToInternalHomWithGivenInternalHom, # # Adjoint( ρ_a ) = ( a → Hom(1,a) ) - return TensorProductToInternalHomAdjunctionMap( cat, + return TensorProductToInternalHomAdjunctionMapWithGivenInternalHom( cat, a, TensorUnit( cat ), - RightUnitor( cat, a ) ); + RightUnitor( cat, a ), + internal_hom ); end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); @@ -595,10 +605,13 @@ AddDerivationToCAP( IsomorphismFromInternalHomToObjectWithGivenInternalHom, "IsomorphismFromInternalHomToObjectWithGivenInternalHom using the evaluation morphism", [ [ TensorUnit, 1 ], [ PreCompose, 1 ], - [ RightUnitorInverse, 1 ], - [ EvaluationMorphism, 1 ] ], + [ TensorProductOnObjects, 1 ], + [ InternalHomOnObjects, 1 ], + [ RightUnitorInverseWithGivenTensorProduct, 1 ], + [ EvaluationMorphismWithGivenSource, 1 ] ], function( cat, a, internal_hom ) + local unit, hom_1a, hom_1a_x_1; # Hom(1,a) # | @@ -610,9 +623,13 @@ AddDerivationToCAP( IsomorphismFromInternalHomToObjectWithGivenInternalHom, # v # a + unit := TensorUnit( cat ); + hom_1a := InternalHomOnObjects( cat, unit, a ); + hom_1a_x_1 := TensorProductOnObjects( cat, hom_1a, unit ); + return PreCompose( cat, - RightUnitorInverse( cat, internal_hom ), - EvaluationMorphism( cat, TensorUnit( cat ), a ) ); + RightUnitorInverseWithGivenTensorProduct( cat, internal_hom, hom_1a_x_1 ), + EvaluationMorphismWithGivenSource( cat, unit, a, hom_1a_x_1 ) ); end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); @@ -679,7 +696,7 @@ end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); ## AddDerivationToCAP( EvaluationMorphismWithGivenSource, "EvaluationMorphismWithGivenSource using the tensor hom adjunction on the identity", - [ [ InternalHomToTensorProductAdjunctionMap, 1 ], + [ [ InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct, 1 ], [ IdentityMorphism, 1 ], [ InternalHomOnObjects, 1 ] ], @@ -687,16 +704,18 @@ AddDerivationToCAP( EvaluationMorphismWithGivenSource, # Adjoint( id_Hom(a,b): Hom(a,b) → Hom(a,b) ) = ( Hom(a,b) ⊗ a → b ) - return InternalHomToTensorProductAdjunctionMap( cat, - a, b, - IdentityMorphism( cat, InternalHomOnObjects( cat, a, b ) ) ); + return InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct( cat, + a, + b, + IdentityMorphism( cat, InternalHomOnObjects( cat, a, b ) ), + tensor_object ); end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); ## AddDerivationToCAP( CoevaluationMorphismWithGivenRange, "CoevaluationMorphismWithGivenRange using the tensor hom adjunction on the identity", - [ [ TensorProductToInternalHomAdjunctionMap, 1 ], + [ [ TensorProductToInternalHomAdjunctionMapWithGivenInternalHom, 1 ], [ IdentityMorphism, 1 ], [ TensorProductOnObjects, 1 ] ], @@ -704,9 +723,11 @@ AddDerivationToCAP( CoevaluationMorphismWithGivenRange, # Adjoint( id_(a ⊗ b): a ⊗ b → a ⊗ b ) = ( a → Hom(b, a ⊗ b) ) - return TensorProductToInternalHomAdjunctionMap( cat, - a, b, - IdentityMorphism( cat, TensorProductOnObjects( cat, a, b ) ) ); + return TensorProductToInternalHomAdjunctionMapWithGivenInternalHom( cat, + a, + b, + IdentityMorphism( cat, TensorProductOnObjects( cat, a, b ) ), + internal_hom ); end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); @@ -849,13 +870,14 @@ end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); ## AddDerivationToCAP( MonoidalPostComposeMorphismWithGivenObjects, "MonoidalPostComposeMorphismWithGivenObjects using MonoidalPreComposeMorphism and braiding", - [ [ Braiding, 1 ], + [ [ BraidingWithGivenTensorProducts, 1 ], [ InternalHomOnObjects, 2 ], [ PreCompose, 1 ], - [ MonoidalPreComposeMorphism, 1 ] ], + [ TensorProductOnObjects, 1], + [ MonoidalPreComposeMorphismWithGivenObjects, 1 ] ], function( cat, source, a, b, c, range ) - local braiding; + local hom_ab, hom_bc, hom_ab_x_hom_bc, braiding; # Hom(b,c) ⊗ Hom(a,b) # | @@ -867,22 +889,27 @@ AddDerivationToCAP( MonoidalPostComposeMorphismWithGivenObjects, # v # Hom(a,c) - braiding := Braiding( cat, InternalHomOnObjects( cat, b, c ), InternalHomOnObjects( cat, a, b ) ); + hom_ab := InternalHomOnObjects( cat, a, b ); + hom_bc := InternalHomOnObjects( cat, b, c ); + hom_ab_x_hom_bc := TensorProductOnObjects( cat, hom_ab, hom_bc ); + + braiding := BraidingWithGivenTensorProducts( cat, source, hom_bc, hom_ab, hom_ab_x_hom_bc ); - return PreCompose( cat, braiding, MonoidalPreComposeMorphism( cat, a, b, c ) ); + return PreCompose( cat, braiding, MonoidalPreComposeMorphismWithGivenObjects( cat, hom_ab_x_hom_bc, a, b, c, range ) ); end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); ## AddDerivationToCAP( MonoidalPreComposeMorphismWithGivenObjects, "MonoidalPreComposeMorphismWithGivenObjects using MonoidalPostComposeMorphism and braiding", - [ [ Braiding, 1 ], + [ [ BraidingWithGivenTensorProducts, 1 ], [ InternalHomOnObjects, 2 ], [ PreCompose, 1 ], - [ MonoidalPostComposeMorphism, 1 ] ], + [ TensorProductOnObjects, 1], + [ MonoidalPostComposeMorphismWithGivenObjects, 1 ] ], function( cat, source, a, b, c, range ) - local braiding; + local hom_ab, hom_bc, hom_bc_x_hom_ab, braiding; # Hom(a,b) ⊗ Hom(b,c) # | @@ -894,9 +921,13 @@ AddDerivationToCAP( MonoidalPreComposeMorphismWithGivenObjects, # v # Hom(a,c) - braiding := Braiding( cat, InternalHomOnObjects( cat, a, b ), InternalHomOnObjects( cat, b, c ) ); + hom_ab := InternalHomOnObjects( cat, a, b ); + hom_bc := InternalHomOnObjects( cat, b, c ); + hom_bc_x_hom_ab := TensorProductOnObjects( cat, hom_bc, hom_ab ); + + braiding := BraidingWithGivenTensorProducts( cat, source, hom_ab, hom_bc, hom_bc_x_hom_ab ); - return PreCompose( cat, braiding, MonoidalPostComposeMorphism( cat, a, b, c ) ); + return PreCompose( cat, braiding, MonoidalPostComposeMorphismWithGivenObjects( cat, hom_bc_x_hom_ab, a, b, c, range ) ); end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); diff --git a/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi index 2dc4016d68..d9753b33f4 100644 --- a/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi +++ b/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi @@ -293,7 +293,7 @@ end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory ); ## AddDerivationToCAP( CoclosedEvaluationForCoDualWithGivenTensorProduct, "CoclosedEvaluationForCoDualWithGivenTensorProduct using the cohom tensor adjunction and IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject", - [ [ InternalCoHomToTensorProductAdjunctionMap, 1 ], + [ [ InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct, 1 ], [ IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject, 1 ] ], function( cat, s, a, r ) @@ -302,10 +302,11 @@ AddDerivationToCAP( CoclosedEvaluationForCoDualWithGivenTensorProduct, # Adjoint( Cohom(1,a) → a_v ) = ( 1 → a_v ⊗ a ) - return InternalCoHomToTensorProductAdjunctionMap( cat, + return InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct( cat, s, a, - IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject( cat, a ) ); + IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject( cat, a ), + r ); end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory ); @@ -539,13 +540,15 @@ AddDerivationToCAP( IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom, "IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom using the coclosed coevaluation morphism", [ [ TensorUnit, 1 ], [ PreCompose, 1 ], - [ InternalCoHomOnMorphisms, 1 ], - [ RightUnitorInverse, 1 ], + [ TensorProductOnObjects, 1 ], + [ InternalCoHomOnObjects, 1 ], + [ InternalCoHomOnMorphismsWithGivenInternalCoHoms, 1 ], + [ RightUnitorInverseWithGivenTensorProduct, 1 ], [ IdentityMorphism, 1 ], - [ CoclosedCoevaluationMorphism, 1 ] ], + [ CoclosedCoevaluationMorphismWithGivenSource, 1 ] ], function( cat, a, internal_cohom ) - local unit; + local unit, a_x_1, cohom_a1_1; # Cohom(a, 1) # | @@ -558,13 +561,16 @@ AddDerivationToCAP( IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom, # a unit := TensorUnit( cat ); + a_x_1 := TensorProductOnObjects( cat, a, unit ); + cohom_a1_1 := InternalCoHomOnObjects( cat, a_x_1, unit ); return PreCompose( cat, - InternalCoHomOnMorphisms( cat, - RightUnitorInverse( cat, a ), - IdentityMorphism( cat, unit ) ), - - CoclosedCoevaluationMorphism( cat, a, unit ) ); + InternalCoHomOnMorphismsWithGivenInternalCoHoms( cat, + internal_cohom, + RightUnitorInverseWithGivenTensorProduct( cat, a, a_x_1 ), + IdentityMorphism( cat, unit ), + cohom_a1_1 ), + CoclosedCoevaluationMorphismWithGivenSource( cat, a, unit, cohom_a1_1 ) ); end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory ); @@ -572,7 +578,7 @@ end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory ); AddDerivationToCAP( IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom, "IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom as the adjoint of the right inverse unitor", [ [ TensorUnit, 1 ], - [ TensorProductToInternalCoHomAdjunctionMap, 1 ], + [ TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom, 1 ], [ RightUnitorInverse, 1 ] ], function( cat, a, internal_cohom ) @@ -581,10 +587,11 @@ AddDerivationToCAP( IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom, # # Adjoint( (ρ_a)^-1 ) = ( Cohom(a,1) → a ) - return TensorProductToInternalCoHomAdjunctionMap( cat, + return TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom( cat, a, TensorUnit( cat ), - RightUnitorInverse( cat, a ) ); + RightUnitorInverse( cat, a ), + internal_cohom ); end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory ); @@ -606,11 +613,12 @@ AddDerivationToCAP( IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom, "IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom using the coclosed evaluation morphism", [ [ TensorUnit, 1 ], [ PreCompose, 1 ], - [ CoclosedEvaluationMorphism, 1 ], - [ RightUnitor, 1 ] ], + [ InternalCoHomOnObjects, 1 ], + [ CoclosedEvaluationMorphismWithGivenRange, 1 ], + [ RightUnitorWithGivenTensorProduct, 1 ] ], function( cat, a, internal_cohom ) - + local unit, cohom_a1_x_1; # a # | # | coclev_(a,1) @@ -621,9 +629,12 @@ AddDerivationToCAP( IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom, # v # Cohom(a,1) + unit := TensorUnit( cat ); + cohom_a1_x_1 := InternalCoHomOnObjects( cat, internal_cohom, unit ); + return PreCompose( cat, - CoclosedEvaluationMorphism( cat, a, TensorUnit( cat ) ), - RightUnitor( cat, internal_cohom ) ); + CoclosedEvaluationMorphismWithGivenRange( cat, a, unit, cohom_a1_x_1 ), + RightUnitorWithGivenTensorProduct( cat, internal_cohom, cohom_a1_x_1 ) ); end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory ); @@ -690,7 +701,7 @@ end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory ); ## AddDerivationToCAP( CoclosedEvaluationMorphismWithGivenRange, "CoclosedEvaluationMorphismWithGivenRange using the cohom tensor adjunction on the identity", - [ [ InternalCoHomToTensorProductAdjunctionMap, 1 ], + [ [ InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct, 1 ], [ IdentityMorphism, 1 ], [ InternalCoHomOnObjects, 1 ] ], @@ -698,16 +709,17 @@ AddDerivationToCAP( CoclosedEvaluationMorphismWithGivenRange, # Adjoint( id_Cohom(a,b): Cohom(a,b) → Cohom(a,b) ) = ( a → Cohom(a,b) ⊗ b ) - return InternalCoHomToTensorProductAdjunctionMap( cat, - a, b, - IdentityMorphism( cat, InternalCoHomOnObjects( cat, a, b ) ) - ); + return InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct( cat, + a, + b, + IdentityMorphism( cat, InternalCoHomOnObjects( cat, a, b ) ), + tensor_object ); end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory ); AddDerivationToCAP( CoclosedCoevaluationMorphismWithGivenSource, "CoclosedCoevaluationMorphismWithGivenSource using the cohom tensor adjunction on the identity", - [ [ TensorProductToInternalCoHomAdjunctionMap, 1 ], + [ [ TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom, 1 ], [ IdentityMorphism, 1 ], [ TensorProductOnObjects, 1 ] ], @@ -715,10 +727,11 @@ AddDerivationToCAP( CoclosedCoevaluationMorphismWithGivenSource, # Adjoint( id_(a ⊗ b): a ⊗ b → a ⊗ b ) = ( Cohom(a ⊗ b, b) → a ) - return TensorProductToInternalCoHomAdjunctionMap( cat, - a, b, - IdentityMorphism( cat, TensorProductOnObjects( cat, a, b ) ) - ); + return TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom( cat, + a, + b, + IdentityMorphism( cat, TensorProductOnObjects( cat, a, b ) ), + internal_cohom ); end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory ); @@ -861,13 +874,14 @@ end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory ); ## AddDerivationToCAP( MonoidalPostCoComposeMorphismWithGivenObjects, "MonoidalPostCoComposeMorphismWithGivenObjects using MonoidalPreCoComposeMorphism and braiding", - [ [ Braiding, 1 ], + [ [ BraidingWithGivenTensorProducts, 1 ], [ InternalCoHomOnObjects, 2 ], [ PreCompose, 1 ], - [ MonoidalPreCoComposeMorphism, 1 ] ], + [ TensorProductOnObjects, 1 ], + [ MonoidalPreCoComposeMorphismWithGivenObjects, 1 ] ], function( cat, source, a, b, c, range ) - local braiding; + local cohom_ab, cohom_bc, cohom_bc_x_cohom_ab, braiding; # Cohom(a,c) # | @@ -879,22 +893,27 @@ AddDerivationToCAP( MonoidalPostCoComposeMorphismWithGivenObjects, # v # Cohom(a,b) ⊗ Cohom(b,c) - braiding := Braiding( cat, InternalCoHomOnObjects( cat, b, c ), InternalCoHomOnObjects( cat, a, b ) ); + cohom_ab := InternalCoHomOnObjects( cat, a, b ); + cohom_bc := InternalCoHomOnObjects( cat, b, c ); + cohom_bc_x_cohom_ab := TensorProductOnObjects( cat, cohom_bc, cohom_ab ); - return PreCompose( cat, MonoidalPreCoComposeMorphism( cat, a, b, c ), braiding ); + braiding := BraidingWithGivenTensorProducts( cat, cohom_bc_x_cohom_ab, cohom_bc, cohom_ab, range ); + + return PreCompose( cat, MonoidalPreCoComposeMorphismWithGivenObjects( cat, source, a, b, c, cohom_bc_x_cohom_ab ), braiding ); end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory ); ## AddDerivationToCAP( MonoidalPreCoComposeMorphismWithGivenObjects, "MonoidalPreCoComposeMorphismWithGivenObjects using MonoidalPostCoComposeMorphism and braiding", - [ [ Braiding, 1 ], + [ [ BraidingWithGivenTensorProducts, 1 ], [ InternalCoHomOnObjects, 2 ], [ PreCompose, 1 ], - [ MonoidalPostCoComposeMorphism, 1 ] ], + [ TensorProductOnObjects, 1 ], + [ MonoidalPostCoComposeMorphismWithGivenObjects, 1 ] ], function( cat, source, a, b, c, range ) - local braiding; + local cohom_ab, cohom_bc, cohom_ab_x_cohom_bc, braiding; # Cohom(a,c) # | @@ -905,10 +924,14 @@ AddDerivationToCAP( MonoidalPreCoComposeMorphismWithGivenObjects, # | B_( Cohom(a,b), Cohom(b,c) ) # v # Cohom(b,c) ⊗ Cohom(a,b) - - braiding := Braiding( cat, InternalCoHomOnObjects( cat, a, b ), InternalCoHomOnObjects( cat, b, c ) ); - return PreCompose( cat, MonoidalPostCoComposeMorphism( cat, a, b, c ), braiding ); + cohom_ab := InternalCoHomOnObjects( cat, a, b ); + cohom_bc := InternalCoHomOnObjects( cat, b, c ); + cohom_ab_x_cohom_bc := TensorProductOnObjects( cat, cohom_ab, cohom_bc ); + + braiding := BraidingWithGivenTensorProducts( cat, cohom_ab_x_cohom_bc, cohom_ab, cohom_bc, range ); + + return PreCompose( cat, MonoidalPostCoComposeMorphismWithGivenObjects( cat, source, a, b, c, cohom_ab_x_cohom_bc ), braiding ); end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );