From 578e66ffe9224887d7d0acfaf910f7b9e37b7299 Mon Sep 17 00:00:00 2001 From: Tom Kuhmichel Date: Fri, 6 Oct 2023 13:54:55 +0200 Subject: [PATCH] WithGiven* for monoidal Isomorphisms --- .../CartesianClosedCategoriesMethodRecord.gi | 6 - ...CartesianClosedCategoriesDerivedMethods.gi | 29 ++-- ...rtesianCoclosedCategoriesDerivedMethods.gi | 32 ++-- .../MatrixCategoryPrecompiled.gi | 140 +++++++++--------- ...cClosedMonoidalCategoriesDerivedMethods.gi | 29 ++-- ...oclosedMonoidalCategoriesDerivedMethods.gi | 32 ++-- 6 files changed, 136 insertions(+), 132 deletions(-) diff --git a/CartesianCategories/gap/CartesianClosedCategoriesMethodRecord.gi b/CartesianCategories/gap/CartesianClosedCategoriesMethodRecord.gi index e04757d13a..4baff84bd3 100644 --- a/CartesianCategories/gap/CartesianClosedCategoriesMethodRecord.gi +++ b/CartesianCategories/gap/CartesianClosedCategoriesMethodRecord.gi @@ -29,7 +29,6 @@ ExponentialOnMorphisms := rec( return_type := "morphism", dual_operation := "CoexponentialOnMorphisms", dual_arguments_reversed := true, - compatible_with_congruence_of_morphisms := true, # Test in CartesianClosedCategoriesTest ), @@ -43,7 +42,6 @@ ExponentialOnMorphismsWithGivenExponentials := rec( return_type := "morphism", dual_operation := "CoexponentialOnMorphismsWithGivenCoexponentials", dual_arguments_reversed := true, - compatible_with_congruence_of_morphisms := true, ), CartesianEvaluationMorphism := rec( @@ -109,7 +107,6 @@ DirectProductToExponentialAdjunctionMap := rec( return_type := "morphism", dual_operation := "CoproductToCoexponentialAdjunctionMap", dual_arguments_reversed := false, - compatible_with_congruence_of_morphisms := true, # Test in CartesianClosedCategoriesTest ), @@ -134,7 +131,6 @@ ExponentialToDirectProductAdjunctionMap := rec( dual_operation := "CoexponentialToCoproductAdjunctionMap", dual_preprocessor_func := { cat, a, b, g } -> NTuple( 4, Opposite( cat ), Opposite( b ), Opposite( a ), Opposite( g ) ), dual_arguments_reversed := false, - compatible_with_congruence_of_morphisms := true, # Test in CartesianClosedCategoriesTest ), @@ -221,7 +217,6 @@ CartesianDualOnMorphisms := rec( with_given_object_position := "both", return_type := "morphism", dual_operation := "CocartesianDualOnMorphisms", - compatible_with_congruence_of_morphisms := true, # Test in CartesianClosedCategoriesTest ), @@ -235,7 +230,6 @@ CartesianDualOnMorphismsWithGivenCartesianDuals := rec( return_type := "morphism", dual_operation := "CocartesianDualOnMorphismsWithGivenCocartesianDuals", dual_arguments_reversed := true, - compatible_with_congruence_of_morphisms := true, ), CartesianEvaluationForCartesianDual := rec( diff --git a/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi b/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi index e425c0aae7..c249cbd193 100644 --- a/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi +++ b/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi @@ -534,7 +534,7 @@ end : CategoryFilter := IsCartesianClosedCategory ); AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential, "IsomorphismFromObjectToExponentialWithGivenExponential using the coevaluation morphism", [ [ TerminalObject, 1 ], - [ PreCompose, 1 ], + [ PreComposeList, 1 ], [ CartesianCoevaluationMorphism, 1 ], [ ExponentialOnMorphisms, 1 ], [ IdentityMorphism, 1 ], @@ -555,11 +555,11 @@ AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential, unit := TerminalObject( cat ); - return PreCompose( cat, - CartesianCoevaluationMorphism( cat, a, unit ), - ExponentialOnMorphisms( cat, - IdentityMorphism( cat, unit ), - CartesianRightUnitor( cat, a ) ) ); + return PreComposeList( cat, + a, + [ CartesianCoevaluationMorphism( cat, a, unit ), + ExponentialOnMorphisms( cat, IdentityMorphism( cat, unit ), CartesianRightUnitor( cat, a ) ) ], + internal_hom ); end : CategoryFilter := IsCartesianClosedCategory ); @@ -567,7 +567,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 ) @@ -576,10 +576,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 ); @@ -600,7 +601,7 @@ end : CategoryFilter := IsCartesianClosedCategory ); AddDerivationToCAP( IsomorphismFromExponentialToObjectWithGivenExponential, "IsomorphismFromExponentialToObjectWithGivenExponential using the evaluation morphism", [ [ TerminalObject, 1 ], - [ PreCompose, 1 ], + [ PreComposeList, 1 ], [ CartesianRightUnitorInverse, 1 ], [ CartesianEvaluationMorphism, 1 ] ], @@ -616,9 +617,11 @@ AddDerivationToCAP( IsomorphismFromExponentialToObjectWithGivenExponential, # v # a - return PreCompose( cat, - CartesianRightUnitorInverse( cat, internal_hom ), - CartesianEvaluationMorphism( cat, TerminalObject( cat ), a ) ); + return PreComposeList( cat, + internal_hom, + [ CartesianRightUnitorInverse( cat, internal_hom ), + CartesianEvaluationMorphism( cat, TerminalObject( cat ), a ) ], + a ); end : CategoryFilter := IsCartesianClosedCategory ); diff --git a/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi b/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi index 28d7a35983..9b1b567604 100644 --- a/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi +++ b/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi @@ -542,7 +542,7 @@ end : CategoryFilter := IsCocartesianCoclosedCategory ); AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential, "IsomorphismFromCoexponentialToObjectWithGivenCoexponential using the cocartesian coevaluation morphism", [ [ InitialObject, 1 ], - [ PreCompose, 1 ], + [ PreComposeList, 1 ], [ CoexponentialOnMorphisms, 1 ], [ CocartesianRightUnitorInverse, 1 ], [ IdentityMorphism, 1 ], @@ -563,12 +563,13 @@ AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential, unit := InitialObject( cat ); - return PreCompose( cat, - CoexponentialOnMorphisms( cat, - CocartesianRightUnitorInverse( cat, a ), - IdentityMorphism( cat, unit ) ), - - CocartesianCoevaluationMorphism( cat, a, unit ) ); + return PreComposeList( cat, + internal_cohom, + [ CoexponentialOnMorphisms( cat, + CocartesianRightUnitorInverse( cat, a ), + IdentityMorphism( cat, unit ) ), + CocartesianCoevaluationMorphism( cat, a, unit ) ], + a ); end : CategoryFilter := IsCocartesianCoclosedCategory ); @@ -576,7 +577,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 ) @@ -585,10 +586,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,7 +611,7 @@ end : CategoryFilter := IsCocartesianCoclosedCategory ); AddDerivationToCAP( IsomorphismFromObjectToCoexponentialWithGivenCoexponential, "IsomorphismFromObjectToCoexponentialWithGivenCoexponential using the cocartesian evaluation morphism", [ [ InitialObject, 1 ], - [ PreCompose, 1 ], + [ PreComposeList, 1 ], [ CocartesianEvaluationMorphism, 1 ], [ CocartesianRightUnitor, 1 ] ], @@ -625,9 +627,11 @@ AddDerivationToCAP( IsomorphismFromObjectToCoexponentialWithGivenCoexponential, # v # Coexp(a,1) - return PreCompose( cat, - CocartesianEvaluationMorphism( cat, a, InitialObject( cat ) ), - CocartesianRightUnitor( cat, internal_cohom ) ); + return PreComposeList( cat, + a, + [ CocartesianEvaluationMorphism( cat, a, InitialObject( cat ) ), + CocartesianRightUnitor( cat, internal_cohom ) ], + internal_cohom ); end : CategoryFilter := IsCocartesianCoclosedCategory ); diff --git a/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi b/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi index 84c0c9c914..eaaa2f68b9 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 ######## - , 5827 : IsPrecompiledDerivation := true ); + , 5223 : 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 ######## - , 5826 : IsPrecompiledDerivation := true ); + , 5222 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromInternalCoHomToTensorProductWithCoDualObject( cat, @@ -2952,7 +2950,7 @@ function ( cat_1, a_1 ) end ######## - , 3315 : IsPrecompiledDerivation := true ); + , 3616 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromInternalHomToObjectWithGivenInternalHom( cat, @@ -2972,7 +2970,7 @@ function ( cat_1, a_1, s_1 ) end ######## - , 3314 : IsPrecompiledDerivation := true ); + , 3615 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromInternalHomToTensorProductWithDualObject( cat, @@ -3050,7 +3048,7 @@ function ( cat_1, a_1 ) end ######## - , 3315 : IsPrecompiledDerivation := true ); + , 3616 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom( cat, @@ -3070,61 +3068,59 @@ function ( cat_1, a_1, r_1 ) end ######## - , 3314 : IsPrecompiledDerivation := true ); + , 3615 : 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 ######## - , 5827 : IsPrecompiledDerivation := true ); + , 5223 : 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 ######## - , 5826 : IsPrecompiledDerivation := true ); + , 5222 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromPushoutToCoequalizerOfCoproductDiagram( cat, diff --git a/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi index 5c348eaa16..2bb0e22503 100644 --- a/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi +++ b/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi @@ -531,7 +531,7 @@ end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); AddDerivationToCAP( IsomorphismFromObjectToInternalHomWithGivenInternalHom, "IsomorphismFromObjectToInternalHomWithGivenInternalHom using the coevaluation morphism", [ [ TensorUnit, 1 ], - [ PreCompose, 1 ], + [ PreComposeList, 1 ], [ CoevaluationMorphism, 1 ], [ InternalHomOnMorphisms, 1 ], [ IdentityMorphism, 1 ], @@ -552,11 +552,11 @@ AddDerivationToCAP( IsomorphismFromObjectToInternalHomWithGivenInternalHom, unit := TensorUnit( cat ); - return PreCompose( cat, - CoevaluationMorphism( cat, a, unit ), - InternalHomOnMorphisms( cat, - IdentityMorphism( cat, unit ), - RightUnitor( cat, a ) ) ); + return PreComposeList( cat, + a, + [ CoevaluationMorphism( cat, a, unit ), + InternalHomOnMorphisms( cat, IdentityMorphism( cat, unit ), RightUnitor( cat, a ) ) ], + internal_hom ); end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); @@ -564,7 +564,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 ) @@ -573,10 +573,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 ); @@ -597,7 +598,7 @@ end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); AddDerivationToCAP( IsomorphismFromInternalHomToObjectWithGivenInternalHom, "IsomorphismFromInternalHomToObjectWithGivenInternalHom using the evaluation morphism", [ [ TensorUnit, 1 ], - [ PreCompose, 1 ], + [ PreComposeList, 1 ], [ RightUnitorInverse, 1 ], [ EvaluationMorphism, 1 ] ], @@ -613,9 +614,11 @@ AddDerivationToCAP( IsomorphismFromInternalHomToObjectWithGivenInternalHom, # v # a - return PreCompose( cat, - RightUnitorInverse( cat, internal_hom ), - EvaluationMorphism( cat, TensorUnit( cat ), a ) ); + return PreComposeList( cat, + internal_hom, + [ RightUnitorInverse( cat, internal_hom ), + EvaluationMorphism( cat, TensorUnit( cat ), a ) ], + a ); end : CategoryFilter := IsSymmetricClosedMonoidalCategory ); diff --git a/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi index e667aee386..bff425fc82 100644 --- a/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi +++ b/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi @@ -539,7 +539,7 @@ end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory ); AddDerivationToCAP( IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom, "IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom using the coclosed coevaluation morphism", [ [ TensorUnit, 1 ], - [ PreCompose, 1 ], + [ PreComposeList, 1 ], [ InternalCoHomOnMorphisms, 1 ], [ RightUnitorInverse, 1 ], [ IdentityMorphism, 1 ], @@ -560,12 +560,13 @@ AddDerivationToCAP( IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom, unit := TensorUnit( cat ); - return PreCompose( cat, - InternalCoHomOnMorphisms( cat, - RightUnitorInverse( cat, a ), - IdentityMorphism( cat, unit ) ), - - CoclosedCoevaluationMorphism( cat, a, unit ) ); + return PreComposeList( cat, + internal_cohom, + [ InternalCoHomOnMorphisms( cat, + RightUnitorInverse( cat, a ), + IdentityMorphism( cat, unit ) ), + CoclosedCoevaluationMorphism( cat, a, unit ) ], + a ); end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory ); @@ -573,7 +574,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 ) @@ -582,10 +583,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,7 +608,7 @@ end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory ); AddDerivationToCAP( IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom, "IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom using the coclosed evaluation morphism", [ [ TensorUnit, 1 ], - [ PreCompose, 1 ], + [ PreComposeList, 1 ], [ CoclosedEvaluationMorphism, 1 ], [ RightUnitor, 1 ] ], @@ -622,9 +624,11 @@ AddDerivationToCAP( IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom, # v # Cohom(a,1) - return PreCompose( cat, - CoclosedEvaluationMorphism( cat, a, TensorUnit( cat ) ), - RightUnitor( cat, internal_cohom ) ); + return PreComposeList( cat, + a, + [ CoclosedEvaluationMorphism( cat, a, TensorUnit( cat ) ), + RightUnitor( cat, internal_cohom ) ], + internal_cohom ); end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );