Skip to content

Commit 9698af4

Browse files
author
Tom Kuhmichel
committed
WithGiven* for monoidal Isomorphisms
1 parent a12bd07 commit 9698af4

File tree

8 files changed

+183
-139
lines changed

8 files changed

+183
-139
lines changed

‎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.11-02",
13+
Version := "2023.11-03",
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/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi‎

Lines changed: 29 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -534,14 +534,16 @@ end : CategoryFilter := IsCartesianClosedCategory );
534534
AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
535535
"IsomorphismFromObjectToExponentialWithGivenExponential using the coevaluation morphism",
536536
[ [ TerminalObject, 1 ],
537+
[ DirectProduct, 1 ],
538+
[ ExponentialOnObjects, 1 ],
537539
[ PreCompose, 1 ],
538-
[ CartesianCoevaluationMorphism, 1 ],
539-
[ ExponentialOnMorphisms, 1 ],
540+
[ CartesianCoevaluationMorphismWithGivenRange, 1 ],
541+
[ ExponentialOnMorphismsWithGivenExponentials, 1 ],
540542
[ IdentityMorphism, 1 ],
541-
[ CartesianRightUnitor, 1 ] ],
543+
[ CartesianRightUnitorWithGivenDirectProduct, 1 ] ],
542544

543545
function( cat, a, internal_hom )
544-
local unit;
546+
local unit, a_x_1, exp_1_ax1;
545547

546548
# a
547549
# |
@@ -554,20 +556,24 @@ AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
554556
# Exp(1, a)
555557

556558
unit := TerminalObject( cat );
559+
a_x_1 := BinaryDirectProduct( cat, a, unit );
560+
exp_1_ax1:= ExponentialOnObjects( cat, unit, a_x_1 );
557561

558562
return PreCompose( cat,
559-
CartesianCoevaluationMorphism( cat, a, unit ),
560-
ExponentialOnMorphisms( cat,
561-
IdentityMorphism( cat, unit ),
562-
CartesianRightUnitor( cat, a ) ) );
563+
CartesianCoevaluationMorphismWithGivenRange( cat, a, unit, exp_1_ax1 ),
564+
ExponentialOnMorphismsWithGivenExponentials( cat,
565+
exp_1_ax1,
566+
IdentityMorphism( cat, unit ),
567+
CartesianRightUnitorWithGivenDirectProduct( cat, a, a_x_1 ),
568+
internal_hom ) );
563569

564570
end : CategoryFilter := IsCartesianClosedCategory );
565571

566572
##
567573
AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
568574
"IsomorphismFromObjectToExponentialWithGivenExponential as the adjoint of the right unitor",
569575
[ [ TerminalObject, 1 ],
570-
[ DirectProductToExponentialAdjunctionMap, 1 ],
576+
[ DirectProductToExponentialAdjunctionMapWithGivenExponential, 1 ],
571577
[ CartesianRightUnitor, 1 ] ],
572578

573579
function( cat, a, internal_hom )
@@ -576,10 +582,11 @@ AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
576582
#
577583
# Adjoint( ρ_a ) = ( a → Exp(1,a) )
578584

579-
return DirectProductToExponentialAdjunctionMap( cat,
585+
return DirectProductToExponentialAdjunctionMapWithGivenExponential( cat,
580586
a,
581587
TerminalObject( cat ),
582-
CartesianRightUnitor( cat, a ) );
588+
CartesianRightUnitor( cat, a ),
589+
internal_hom );
583590

584591
end : CategoryFilter := IsCartesianClosedCategory );
585592

@@ -601,10 +608,13 @@ AddDerivationToCAP( IsomorphismFromExponentialToObjectWithGivenExponential,
601608
"IsomorphismFromExponentialToObjectWithGivenExponential using the evaluation morphism",
602609
[ [ TerminalObject, 1 ],
603610
[ PreCompose, 1 ],
604-
[ CartesianRightUnitorInverse, 1 ],
605-
[ CartesianEvaluationMorphism, 1 ] ],
611+
[ DirectProduct, 1 ],
612+
[ ExponentialOnObjects, 1 ],
613+
[ CartesianRightUnitorInverseWithGivenDirectProduct, 1 ],
614+
[ CartesianEvaluationMorphismWithGivenSource, 1 ] ],
606615

607616
function( cat, a, internal_hom )
617+
local unit, exp_1a, exp_1a_x_1;
608618

609619
# Exp(1,a)
610620
# |
@@ -616,9 +626,13 @@ AddDerivationToCAP( IsomorphismFromExponentialToObjectWithGivenExponential,
616626
# v
617627
# a
618628

629+
unit := TerminalObject( cat );
630+
exp_1a := ExponentialOnObjects( cat, unit, a );
631+
exp_1a_x_1 := BinaryDirectProduct( cat, exp_1a, unit );
632+
619633
return PreCompose( cat,
620-
CartesianRightUnitorInverse( cat, internal_hom ),
621-
CartesianEvaluationMorphism( cat, TerminalObject( cat ), a ) );
634+
CartesianRightUnitorInverseWithGivenDirectProduct( cat, internal_hom, exp_1a_x_1 ),
635+
CartesianEvaluationMorphismWithGivenSource( cat, unit, a, exp_1a_x_1 ) );
622636

623637
end : CategoryFilter := IsCartesianClosedCategory );
624638

‎CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi‎

Lines changed: 27 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -543,13 +543,15 @@ AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,
543543
"IsomorphismFromCoexponentialToObjectWithGivenCoexponential using the cocartesian coevaluation morphism",
544544
[ [ InitialObject, 1 ],
545545
[ PreCompose, 1 ],
546-
[ CoexponentialOnMorphisms, 1 ],
547-
[ CocartesianRightUnitorInverse, 1 ],
546+
[ Coproduct, 1 ],
547+
[ CoexponentialOnObjects, 1 ],
548+
[ CoexponentialOnMorphismsWithGivenCoexponentials, 1 ],
549+
[ CocartesianRightUnitorInverseWithGivenCoproduct, 1 ],
548550
[ IdentityMorphism, 1 ],
549-
[ CocartesianCoevaluationMorphism, 1 ] ],
551+
[ CocartesianCoevaluationMorphismWithGivenSource, 1 ] ],
550552

551553
function( cat, a, internal_cohom )
552-
local unit;
554+
local unit, a_x_1, coexp_a1_1;
553555

554556
# Coexp(a, 1)
555557
# |
@@ -562,21 +564,24 @@ AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,
562564
# a
563565

564566
unit := InitialObject( cat );
567+
a_x_1 := BinaryCoproduct( cat, a, unit );
568+
coexp_a1_1 := CoexponentialOnObjects( cat, a_x_1, unit );
565569

566570
return PreCompose( cat,
567-
CoexponentialOnMorphisms( cat,
568-
CocartesianRightUnitorInverse( cat, a ),
569-
IdentityMorphism( cat, unit ) ),
570-
571-
CocartesianCoevaluationMorphism( cat, a, unit ) );
571+
CoexponentialOnMorphismsWithGivenCoexponentials( cat,
572+
internal_cohom,
573+
CocartesianRightUnitorInverseWithGivenCoproduct( cat, a, a_x_1 ),
574+
IdentityMorphism( cat, unit ),
575+
coexp_a1_1 ),
576+
CocartesianCoevaluationMorphismWithGivenSource( cat, a, unit, coexp_a1_1 ) );
572577

573578
end : CategoryFilter := IsCocartesianCoclosedCategory );
574579

575580
##
576581
AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,
577582
"IsomorphismFromCoexponentialToObjectWithGivenCoexponential as the adjoint of the right inverse unitor",
578583
[ [ InitialObject, 1 ],
579-
[ CoproductToCoexponentialAdjunctionMap, 1 ],
584+
[ CoproductToCoexponentialAdjunctionMapWithGivenCoexponential, 1 ],
580585
[ CocartesianRightUnitorInverse, 1 ] ],
581586

582587
function( cat, a, internal_cohom )
@@ -585,10 +590,11 @@ AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,
585590
#
586591
# Adjoint( (ρ_a)^-1 ) = ( Coexp(a,1) → a )
587592

588-
return CoproductToCoexponentialAdjunctionMap( cat,
593+
return CoproductToCoexponentialAdjunctionMapWithGivenCoexponential( cat,
589594
a,
590595
InitialObject( cat ),
591-
CocartesianRightUnitorInverse( cat, a ) );
596+
CocartesianRightUnitorInverse( cat, a ),
597+
internal_cohom );
592598

593599
end : CategoryFilter := IsCocartesianCoclosedCategory );
594600

@@ -610,11 +616,12 @@ AddDerivationToCAP( IsomorphismFromObjectToCoexponentialWithGivenCoexponential,
610616
"IsomorphismFromObjectToCoexponentialWithGivenCoexponential using the cocartesian evaluation morphism",
611617
[ [ InitialObject, 1 ],
612618
[ PreCompose, 1 ],
613-
[ CocartesianEvaluationMorphism, 1 ],
614-
[ CocartesianRightUnitor, 1 ] ],
619+
[ CoexponentialOnObjects, 1 ],
620+
[ CocartesianEvaluationMorphismWithGivenRange, 1 ],
621+
[ CocartesianRightUnitorWithGivenCoproduct, 1 ] ],
615622

616623
function( cat, a, internal_cohom )
617-
624+
local unit, coexp_a1_x_1;
618625
# a
619626
# |
620627
# | cocaev_(a,1)
@@ -625,9 +632,12 @@ AddDerivationToCAP( IsomorphismFromObjectToCoexponentialWithGivenCoexponential,
625632
# v
626633
# Coexp(a,1)
627634

635+
unit := InitialObject( cat );
636+
coexp_a1_x_1 := CoexponentialOnObjects( cat, internal_cohom, unit );
637+
628638
return PreCompose( cat,
629-
CocartesianEvaluationMorphism( cat, a, InitialObject( cat ) ),
630-
CocartesianRightUnitor( cat, internal_cohom ) );
639+
CocartesianEvaluationMorphismWithGivenRange( cat, a, unit, coexp_a1_x_1 ),
640+
CocartesianRightUnitorWithGivenCoproduct( cat, internal_cohom, coexp_a1_x_1 ) );
631641

632642
end : CategoryFilter := IsCocartesianCoclosedCategory );
633643

‎LinearAlgebraForCAP/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 := "LinearAlgebraForCAP",
1212
Subtitle := "Category of Matrices over a Field for CAP",
13-
Version := "2023.11-01",
13+
Version := "2023.11-02",
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)