Skip to content

Commit 91f0ae5

Browse files
mohamed-barakatmohamed-barakat
authored
Merge pull request #1492 from TKuh/adjunction_with_given
Add derivation for `*AdjunctionMapWithGivenTensorProduct`
2 parents add7ebd + cf75f32 commit 91f0ae5

12 files changed

+174
-6
lines changed

‎CAP/examples/TerminalCategoryWithMultipleObjects.g‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ T := TerminalCategoryWithMultipleObjects( );
1010
Display( T );
1111
#! A CAP category with name TerminalCategoryWithMultipleObjects( ):
1212
#!
13-
#! 65 primitive operations were used to derive 309 operations for this category \
13+
#! 65 primitive operations were used to derive 311 operations for this category \
1414
#! which algorithmically
1515
#! * IsCategoryWithDecidableColifts
1616
#! * IsCategoryWithDecidableLifts

‎CAP/examples/TerminalCategoryWithSingleObject.g‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ T := TerminalCategoryWithSingleObject( );
1010
Display( T );
1111
#! A CAP category with name TerminalCategoryWithSingleObject( ):
1212
#!
13-
#! 63 primitive operations were used to derive 309 operations for this category \
13+
#! 63 primitive operations were used to derive 311 operations for this category \
1414
#! which algorithmically
1515
#! * IsCategoryWithDecidableColifts
1616
#! * IsCategoryWithDecidableLifts

‎CartesianCategories/PackageInfo.g‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
1010

1111
PackageName := "CartesianCategories",
1212
Subtitle := "Cartesian and cocartesian categories and various subdoctrines",
13-
Version := "2023.08-14",
13+
Version := "2023.10-01",
1414
Date := ~.Version{[ 1 .. 10 ]},
1515
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)( ),
1616
License := "GPL-2.0-or-later",

‎CartesianCategories/examples/InfoStringOfInstalledOperationsOfCategory.g‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ distributive := DummyCategory( rec(
1515
properties := [ "IsBicartesianClosedCategory", "IsSkeletalCategory" ] ) );;
1616

1717
InfoOfInstalledOperationsOfCategory( distributive );
18-
#! 19 primitive operations were used to derive 112 operations for this category \
18+
#! 19 primitive operations were used to derive 113 operations for this category \
1919
#! which algorithmically
2020
#! * IsBicartesianClosedCategory
2121
#! and not yet algorithmically

‎CartesianCategories/gap/AUTOGENERATED_FROM.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
The files of this package which include the line `THIS FILE WAS AUTOMATICALLY GENERATED` in their header have been autogenerated
22

3-
* from MonoidalCategories v2023.08-11
3+
* from MonoidalCategories v2023.10-01

‎CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,37 @@ AddDerivationToCAP( ExponentialToDirectProductAdjunctionMap,
9494

9595
end : CategoryFilter := IsCartesianClosedCategory );
9696

97+
##
98+
AddDerivationToCAP( ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct,
99+
"ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct using DirectProductOnMorphisms and CartesianEvaluationMorphism",
100+
[ [ PreCompose, 1 ],
101+
[ DirectProductOnMorphismsWithGivenDirectProducts, 1 ],
102+
[ IdentityMorphism, 1 ],
103+
[ CartesianEvaluationMorphism, 1 ] ],
104+
105+
function( cat, b, c, g, t )
106+
local ev_bc;
107+
108+
# g: a → Exp(b,c)
109+
#
110+
# a × b
111+
# |
112+
# | g × id_b
113+
# v
114+
# Exp(b,c) × b
115+
# |
116+
# | ev_bc
117+
# v
118+
# c
119+
120+
ev_bc := CartesianEvaluationMorphism( cat, b, c );
121+
122+
return PreCompose( cat,
123+
DirectProductOnMorphismsWithGivenDirectProducts( cat, t, g, IdentityMorphism( cat, b ), Source( ev_bc ) ),
124+
ev_bc );
125+
126+
end : CategoryFilter := IsCartesianClosedCategory );
127+
97128
##
98129
AddDerivationToCAP( UniversalPropertyOfCartesianDual,
99130
"UniversalPropertyOfCartesianDual using the direct product-exponential adjunction",

‎CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,37 @@ AddDerivationToCAP( CoexponentialToCoproductAdjunctionMap,
9494

9595
end : CategoryFilter := IsCocartesianCoclosedCategory );
9696

97+
##
98+
AddDerivationToCAP( CoexponentialToCoproductAdjunctionMapWithGivenCoproduct,
99+
"CoexponentialToCoproductAdjunctionMapWithGivenCoproduct using CoproductOnMorphisms and CocartesianEvaluationMorphism",
100+
[ [ PreCompose, 1 ],
101+
[ CocartesianEvaluationMorphism, 1 ],
102+
[ CoproductOnMorphismsWithGivenCoproducts, 1 ],
103+
[ IdentityMorphism, 1 ] ],
104+
105+
function( cat, a, b, f, t )
106+
local cocaev_bc;
107+
108+
# f: Coexp(a,b) → c
109+
#
110+
# a
111+
# |
112+
# | cocaev_ab
113+
# v
114+
# Coexp(a,b) ⊔ b
115+
# |
116+
# | f ⊔ id_b
117+
# v
118+
# c ⊔ b
119+
120+
cocaev_bc := CocartesianEvaluationMorphism( cat, a, b );
121+
122+
return PreCompose( cat,
123+
cocaev_bc,
124+
CoproductOnMorphismsWithGivenCoproducts( cat, Range( cocaev_bc ), f, IdentityMorphism( cat, b ), t ) );
125+
126+
end : CategoryFilter := IsCocartesianCoclosedCategory );
127+
97128
##
98129
AddDerivationToCAP( UniversalPropertyOfCocartesianDual,
99130
"UniversalPropertyOfCocartesianDual using the coexponential-coproduct adjunction",

‎FreydCategoriesForCAP/gap/CategoryOfRows.autogen.gd‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -251,10 +251,12 @@
251251
#! * <Ref BookName="MonoidalCategories" Func="InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects" Label="for Is" />
252252
#! * <Ref BookName="MonoidalCategories" Func="InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects" Label="for Is" />
253253
#! * <Ref BookName="MonoidalCategories" Func="InternalCoHomToTensorProductAdjunctionMap" Label="for Is" />
254+
#! * <Ref BookName="MonoidalCategories" Func="InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct" Label="for Is" />
254255
#! * <Ref BookName="MonoidalCategories" Func="InternalHomOnMorphisms" Label="for Is" />
255256
#! * <Ref BookName="MonoidalCategories" Func="InternalHomOnMorphismsWithGivenInternalHoms" Label="for Is" />
256257
#! * <Ref BookName="MonoidalCategories" Func="InternalHomOnObjects" Label="for Is" />
257258
#! * <Ref BookName="MonoidalCategories" Func="InternalHomToTensorProductAdjunctionMap" Label="for Is" />
259+
#! * <Ref BookName="MonoidalCategories" Func="InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct" Label="for Is" />
258260
#! * <Ref BookName="CAP" Func="IsIsomorphicForObjects" Label="for Is" />
259261
#! * <Ref BookName="MonoidalCategories" Func="IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit" Label="for Is" />
260262
#! * <Ref BookName="MonoidalCategories" Func="IsomorphismFromDualObjectToInternalHomIntoTensorUnit" Label="for Is" />

‎LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1997,6 +1997,27 @@ end
19971997

19981998
, 3513 : IsPrecompiledDerivation := true );
19991999

2000+
##
2001+
AddInternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct( cat,
2002+
2003+
########
2004+
function ( cat_1, a_1, b_1, f_1, t_1 )
2005+
local deduped_3_1, deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1;
2006+
deduped_7_1 := Dimension( b_1 );
2007+
deduped_6_1 := UnderlyingRing( cat_1 );
2008+
deduped_5_1 := Dimension( a_1 );
2009+
deduped_4_1 := deduped_5_1 * deduped_7_1;
2010+
deduped_3_1 := HomalgIdentityMatrix( deduped_7_1, deduped_6_1 );
2011+
return CreateCapCategoryMorphismWithAttributes( cat_1, a_1, t_1, UnderlyingMatrix, KroneckerMat( HomalgIdentityMatrix( deduped_5_1, deduped_6_1 ), ConvertMatrixToRow( deduped_3_1 ) ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_4_1 ], function ( i_2 )
2012+
local deduped_1_2;
2013+
deduped_1_2 := (i_2 - 1);
2014+
return (REM_INT( deduped_1_2, deduped_7_1 ) * deduped_5_1 + QUO_INT( deduped_1_2, deduped_7_1 ) + 1);
2015+
end ) ), deduped_4_1 ), deduped_4_1, deduped_4_1, deduped_6_1 ), deduped_3_1 ) * KroneckerMat( HomalgIdentityMatrix( (deduped_7_1 * deduped_5_1), deduped_6_1 ), deduped_3_1 ) * KroneckerMat( UnderlyingMatrix( f_1 ), deduped_3_1 ) );
2016+
end
2017+
########
2018+
2019+
, 3312 : IsPrecompiledDerivation := true );
2020+
20002021
##
20012022
AddInternalHomOnMorphisms( cat,
20022023

@@ -2054,6 +2075,27 @@ end
20542075

20552076
, 3513 : IsPrecompiledDerivation := true );
20562077

2078+
##
2079+
AddInternalHomToTensorProductAdjunctionMapWithGivenTensorProduct( cat,
2080+
2081+
########
2082+
function ( cat_1, b_1, c_1, g_1, t_1 )
2083+
local deduped_3_1, deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1;
2084+
deduped_7_1 := Dimension( c_1 );
2085+
deduped_6_1 := UnderlyingRing( cat_1 );
2086+
deduped_5_1 := Dimension( b_1 );
2087+
deduped_4_1 := deduped_5_1 * deduped_7_1;
2088+
deduped_3_1 := HomalgIdentityMatrix( deduped_5_1, deduped_6_1 );
2089+
return CreateCapCategoryMorphismWithAttributes( cat_1, t_1, c_1, UnderlyingMatrix, KroneckerMat( UnderlyingMatrix( g_1 ), deduped_3_1 ) * (KroneckerMat( HomalgIdentityMatrix( deduped_4_1, deduped_6_1 ), deduped_3_1 ) * KroneckerMat( HomalgMatrix( PermutationMat( PermList( List( [ 1 .. deduped_4_1 ], function ( i_2 )
2090+
local deduped_1_2;
2091+
deduped_1_2 := (i_2 - 1);
2092+
return (REM_INT( deduped_1_2, deduped_7_1 ) * deduped_5_1 + QUO_INT( deduped_1_2, deduped_7_1 ) + 1);
2093+
end ) ), deduped_4_1 ), deduped_4_1, deduped_4_1, deduped_6_1 ), deduped_3_1 ) * KroneckerMat( HomalgIdentityMatrix( deduped_7_1, deduped_6_1 ), ConvertMatrixToColumn( deduped_3_1 ) )) );
2094+
end
2095+
########
2096+
2097+
, 3312 : IsPrecompiledDerivation := true );
2098+
20572099
##
20582100
AddInterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( cat,
20592101

‎MonoidalCategories/PackageInfo.g‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
1010

1111
PackageName := "MonoidalCategories",
1212
Subtitle := "Monoidal and monoidal (co)closed categories",
13-
Version := "2023.08-11",
13+
Version := "2023.10-01",
1414
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)( ),
1515
License := "GPL-2.0-or-later",
1616

0 commit comments

Comments
 (0)