Merge pull request #245 from mohamed-barakat/AdjunctMorphism

comply with CartesianCategories v2024.02-02

Author: mohamed-barakat

PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "FinSetsForCAP",
 Subtitle := "The elementary topos of (skeletal) finite sets",
-Version := "2024.02-02",
+Version := "2024.02-03",
 
 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",
@@ -99,8 +99,8 @@ Dependencies := rec(
   GAP := ">= 4.12.1",
   NeededOtherPackages := [
                    [ "CAP", ">= 2023.12-05" ],
-                   [ "CartesianCategories", ">= 2024.01-17" ],
-                   [ "Toposes", ">= 2024.01-02" ],
+                   [ "CartesianCategories", ">= 2024.02-02" ],
+                   [ "Toposes", ">= 2024.02-02" ],
                    ],
   SuggestedOtherPackages := [ ],
   ExternalConditions := [ ],

examples/SkeletalCartesianLambdaIntroduction.g

@@ -46,11 +46,11 @@ Display( Li );
 #!  { 0 } ⱶ[ 4 ]→ { 0,..., 7 }, { 0 } ⱶ[ 5 ]→ { 0,..., 7 },\
 #!  { 0 } ⱶ[ 6 ]→ { 0,..., 7 }, { 0 } ⱶ[ 7 ]→ { 0,..., 7 } ]
 List( L, phi ->
-      DirectProductToExponentialLeftAdjunctionMap( T, S, phi ) ) = Li;
+      DirectProductToExponentialLeftAdjunctMorphism( T, S, phi ) ) = Li;
 #! true
 List( Li, psi -> CartesianLambdaElimination( S, R, psi ) ) = L;
 #! true
 List( Li, psi ->
-      ExponentialToDirectProductLeftAdjunctionMap( S, R, psi ) ) = L;
+      ExponentialToDirectProductLeftAdjunctMorphism( S, R, psi ) ) = L;
 #! true
 #! @EndExample

examples/SkeletalTopos.g

@@ -32,16 +32,16 @@ CartesianBraidingInverse( M, N );;
 ExponentialOnObjects( M, N );;
 ExponentialOnMorphisms( f, g );;
 CartesianRightEvaluationMorphism( M, N );;
-ExponentialToDirectProductRightAdjunctionMap( M, N,
+ExponentialToDirectProductRightAdjunctMorphism( M, N,
     UniversalMorphismFromInitialObject( ExponentialOnObjects( M, N ) )
 );;
 CartesianLeftEvaluationMorphism( M, N );;
 CartesianLeftCoevaluationMorphism( N, M );;
 CartesianLeftCoevaluationMorphism( T, T );;
-DirectProductToExponentialLeftAdjunctionMap( M, N,
+DirectProductToExponentialLeftAdjunctMorphism( M, N,
     UniversalMorphismIntoTerminalObject( DirectProduct( M, N ) )
 );;
-ExponentialToDirectProductLeftAdjunctionMap( M, N,
+ExponentialToDirectProductLeftAdjunctMorphism( M, N,
     UniversalMorphismFromInitialObject( ExponentialOnObjects( M, N ) )
 );;
 

examples/Topos.g

@@ -33,18 +33,18 @@ ExponentialOnObjects( FinSet( [ 1 ] ), exp );;
 ExponentialOnMorphisms( f, g );;
 CartesianRightEvaluationMorphism( M, N );;
 CartesianRightCoevaluationMorphism( N, M );;
-DirectProductToExponentialRightAdjunctionMap( M, N,
+DirectProductToExponentialRightAdjunctMorphism( M, N,
     UniversalMorphismIntoTerminalObject( DirectProduct( M, N ) )
 );;
-ExponentialToDirectProductRightAdjunctionMap( M, N,
+ExponentialToDirectProductRightAdjunctMorphism( M, N,
     UniversalMorphismFromInitialObject( ExponentialOnObjects( M, N ) )
 );;
 CartesianLeftEvaluationMorphism( M, N );;
 CartesianLeftCoevaluationMorphism( N, M );;
-DirectProductToExponentialLeftAdjunctionMap( M, N,
+DirectProductToExponentialLeftAdjunctMorphism( M, N,
     UniversalMorphismIntoTerminalObject( DirectProduct( M, N ) )
 );;
-ExponentialToDirectProductLeftAdjunctionMap( M, N,
+ExponentialToDirectProductLeftAdjunctMorphism( M, N,
     UniversalMorphismFromInitialObject( ExponentialOnObjects( M, N ) )
 );;
 

gap/FinSets.gi

@@ -970,7 +970,7 @@ AddCartesianLeftCoevaluationMorphismWithGivenRange( category_of_finite_sets,
 end );
 
 ##
-AddDirectProductToExponentialLeftAdjunctionMap( category_of_finite_sets,
+AddDirectProductToExponentialLeftAdjunctMorphism( category_of_finite_sets,
   function ( category_of_finite_sets, M, N, f )
     local L;
 
@@ -981,7 +981,7 @@ AddDirectProductToExponentialLeftAdjunctionMap( category_of_finite_sets,
 end );
 
 ##
-AddExponentialToDirectProductLeftAdjunctionMap( category_of_finite_sets,
+AddExponentialToDirectProductLeftAdjunctMorphism( category_of_finite_sets,
   function ( category_of_finite_sets, N, L, g )
     local M, MN;
 
@@ -1013,7 +1013,7 @@ AddCartesianRightCoevaluationMorphismWithGivenRange( category_of_finite_sets,
 end );
 
 ##
-AddDirectProductToExponentialRightAdjunctionMap( category_of_finite_sets,
+AddDirectProductToExponentialRightAdjunctMorphism( category_of_finite_sets,
   function ( category_of_finite_sets, M, N, f )
     local L;
 
@@ -1024,7 +1024,7 @@ AddDirectProductToExponentialRightAdjunctionMap( category_of_finite_sets,
 end );
 
 ##
-AddExponentialToDirectProductRightAdjunctionMap( category_of_finite_sets,
+AddExponentialToDirectProductRightAdjunctMorphism( category_of_finite_sets,
   function ( category_of_finite_sets, M, L, g )
     local N, MN;
 

gap/SkeletalFinSets.gi

@@ -799,7 +799,7 @@ AddExponentialOnObjects( SkeletalFinSets,
 
 end );
 
-## A special case of ExponentialToDirectProductRightAdjunctionMap for A = 𝟙 = TerminalObject
+## A special case of ExponentialToDirectProductRightAdjunctMorphism for A = 𝟙 = TerminalObject
 ## InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism
 ## (g: 𝟙 → Bᴸ) ↦ (f: L = L × 𝟙 → B)
 AddCartesianLambdaElimination( SkeletalFinSets,
@@ -820,7 +820,7 @@ end );
 
 ## base-change from b^l to b:
 ## (g: A → Bᴸ) ↦ (f: L × A → B)
-AddExponentialToDirectProductRightAdjunctionMapWithGivenDirectProduct( SkeletalFinSets,
+AddExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct( SkeletalFinSets,
   function ( cat, L, B, g, LxA )
     local l, b, g_map, la;
 
@@ -844,7 +844,7 @@ end );
 
 ## base-change from b to b^l:
 ## (f: L × A → B) ↦ (g: A → Bᴸ)
-AddDirectProductToExponentialRightAdjunctionMapWithGivenExponential( SkeletalFinSets,
+AddDirectProductToExponentialRightAdjunctMorphismWithGivenExponential( SkeletalFinSets,
   function ( cat, L, A, f, expLB )
     local B, l, b, f_map;
 
@@ -909,7 +909,7 @@ end, 1 + Sum( [ [ "ExponentialOnObjects", 1 ],
                 [ "ExactCoverWithGlobalElements", 1 ],
                 [ "PreComposeList", 2 ],
                 [ "CartesianLambdaElimination", 2 ],
-                [ "DirectProductToExponentialRightAdjunctionMapWithGivenExponential", 2 ] ],
+                [ "DirectProductToExponentialRightAdjunctMorphismWithGivenExponential", 2 ] ],
         e -> e[2] * CurrentOperationWeight( SkeletalFinSets!.derivations_weight_list, e[1] ) ) );
 
 ## Bᴸ × L → B

gap/precompiled_categories/SkeletalCategoryOfFiniteSetsWithMorphismsGivenByListsPrecompiled.gi

@@ -320,7 +320,7 @@ end
     , 100 );
 
     ##
-    AddDirectProductToExponentialRightAdjunctionMapWithGivenExponential( cat,
+    AddDirectProductToExponentialRightAdjunctMorphismWithGivenExponential( cat,
 
 ########
 function ( cat_1, a_1, b_1, f_1, i_1 )
@@ -446,7 +446,7 @@ end
     , 100 );
 
     ##
-    AddExponentialToDirectProductRightAdjunctionMapWithGivenDirectProduct( cat,
+    AddExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct( cat,
 
 ########
 function ( cat_1, a_1, c_1, g_1, s_1 )