From 46d99cc9328202c5dc169e5df3bafc7ef0c2b30b 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 --- ...CartesianClosedCategoriesDerivedMethods.gi | 44 ++++-- ...rtesianCoclosedCategoriesDerivedMethods.gi | 44 +++--- .../MatrixCategoryPrecompiled.gi | 140 +++++++++--------- ...cClosedMonoidalCategoriesDerivedMethods.gi | 44 ++++-- ...oclosedMonoidalCategoriesDerivedMethods.gi | 44 +++--- 5 files changed, 180 insertions(+), 136 deletions(-) diff --git a/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi b/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi index a19ce52e3c..3b0ca74006 100644 --- a/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi +++ b/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi @@ -534,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 # | @@ -554,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 ); @@ -567,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 ) @@ -576,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 ); @@ -601,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) # | @@ -616,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 ); diff --git a/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi b/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi index 58b10f2ad4..9d0c17727d 100644 --- a/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi +++ b/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi @@ -543,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) # | @@ -562,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 ); @@ -576,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 ) @@ -585,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 ); @@ -610,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) @@ -625,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 ); diff --git a/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi b/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi index af1cf57791..06e27140d0 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, diff --git a/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi index f0fa9b8b6b..50a88a841b 100644 --- a/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi +++ b/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi @@ -531,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 # | @@ -551,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 ); @@ -564,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 ) @@ -573,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 ); @@ -598,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) # | @@ -613,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 ); diff --git a/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi index ce6a3369aa..d9753b33f4 100644 --- a/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi +++ b/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi @@ -540,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) # | @@ -559,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 ); @@ -573,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 ) @@ -582,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 ); @@ -607,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) @@ -622,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 );