Skip to content

Commit

Permalink
WithGiven* for monoidal Isomorphisms
Browse files Browse the repository at this point in the history
  • Loading branch information
Tom Kuhmichel committed Nov 29, 2023
1 parent d962219 commit da8624c
Show file tree
Hide file tree
Showing 8 changed files with 183 additions and 139 deletions.
2 changes: 1 addition & 1 deletion CartesianCategories/PackageInfo.g
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
44 changes: 29 additions & 15 deletions CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
# |
Expand All @@ -554,20 +556,24 @@ 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 );

##
AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
"IsomorphismFromObjectToExponentialWithGivenExponential as the adjoint of the right unitor",
[ [ TerminalObject, 1 ],
[ DirectProductToExponentialAdjunctionMap, 1 ],
[ DirectProductToExponentialAdjunctionMapWithGivenExponential, 1 ],
[ CartesianRightUnitor, 1 ] ],

function( cat, a, internal_hom )
Expand All @@ -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 );

Expand All @@ -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)
# |
Expand All @@ -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 );

Expand Down
44 changes: 27 additions & 17 deletions CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
# |
Expand All @@ -562,21 +564,24 @@ 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 );

##
AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,
"IsomorphismFromCoexponentialToObjectWithGivenCoexponential as the adjoint of the right inverse unitor",
[ [ InitialObject, 1 ],
[ CoproductToCoexponentialAdjunctionMap, 1 ],
[ CoproductToCoexponentialAdjunctionMapWithGivenCoexponential, 1 ],
[ CocartesianRightUnitorInverse, 1 ] ],

function( cat, a, internal_cohom )
Expand All @@ -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 );

Expand All @@ -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)
Expand All @@ -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 );

Expand Down
2 changes: 1 addition & 1 deletion LinearAlgebraForCAP/PackageInfo.g
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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",

Expand Down
Loading

0 comments on commit da8624c

Please sign in to comment.