Merge pull request #243 from mohamed-barakat/CartesianRightCoevaluation

compile CartesianRightCoevaluationMorphismWithGivenRange

PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "FinSetsForCAP",
 Subtitle := "The elementary topos of (skeletal) finite sets",
-Version := "2024.02-01",
+Version := "2024.02-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",

examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g

@@ -28,6 +28,7 @@ list_of_operations :=
           "CartesianBraidingInverseWithGivenDirectProducts",
           "CartesianLambdaIntroduction",
           "CartesianRightEvaluationMorphismWithGivenSource",
+          "CartesianRightCoevaluationMorphismWithGivenRange",
           "CoastrictionToImage",
           "CoimageProjection",
           "IsHomSetInhabited",

gap/CompilerLogic.gi

@@ -490,3 +490,19 @@ CapJitAddLogicTemplate(
         dst_template := "entry in list",
     )
 );
+
+CapJitAddLogicTemplate(
+    rec(
+        variable_names := [ "length", "a", "b" ],
+        src_template := "[ 0 .. length - 1 ][1 + a + b]",
+        dst_template := "a + b",
+    )
+);
+
+CapJitAddLogicTemplate(
+    rec(
+        variable_names := [ "a", "q", "i" ],
+        src_template := "Sum( List( [ 0 .. a - 1 ], k -> (k + a * i) * q^k ) )",
+        dst_template := "q * GeometricSumDiff1( q, a ) + a * i * GeometricSum( q, a )",
+    )
+);

gap/SkeletalFinSets.gi

@@ -799,16 +799,17 @@ AddExponentialOnObjects( SkeletalFinSets,
 
 end );
 
-## A special case of ExponentialToDirectProductRightAdjunctionMap for A = TerminalObject
+## A special case of ExponentialToDirectProductRightAdjunctionMap for A = 𝟙 = TerminalObject
 ## InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism
+## (g: 𝟙 → Bᴸ) ↦ (f: L = L × 𝟙 → B)
 AddCartesianLambdaElimination( SkeletalFinSets,
-  function ( cat, L, B, intro )
+  function ( cat, L, B, g )
     local l, b, v;
 
     l := Length( L );
     b := Length( B );
 
-    v := AsList( intro )[1];
+    v := AsList( g )[1];
 
     return MorphismConstructor( cat,
                    L,
@@ -818,7 +819,7 @@ AddCartesianLambdaElimination( SkeletalFinSets,
 end );
 
 ## base-change from b^l to b:
-## (g: A →Bᴸ) ↦ (f: L × A → B)
+## (g: A → Bᴸ) ↦ (f: L × A → B)
 AddExponentialToDirectProductRightAdjunctionMapWithGivenDirectProduct( SkeletalFinSets,
   function ( cat, L, B, g, LxA )
     local l, b, g_map, la;
@@ -842,7 +843,7 @@ AddExponentialToDirectProductRightAdjunctionMapWithGivenDirectProduct( SkeletalF
 end );
 
 ## base-change from b to b^l:
-## (f: L × A → B) ↦ (g: A →Bᴸ)
+## (f: L × A → B) ↦ (g: A → Bᴸ)
 AddDirectProductToExponentialRightAdjunctionMapWithGivenExponential( SkeletalFinSets,
   function ( cat, L, A, f, expLB )
     local B, l, b, f_map;

gap/precompiled_categories/SkeletalCategoryOfFiniteSetsWithMorphismsGivenByListsPrecompiled.gi

@@ -149,6 +149,25 @@ end
 
     , 100 );
 
+    ##
+    AddCartesianRightCoevaluationMorphismWithGivenRange( cat,
+
+########
+function ( cat_1, a_1, b_1, r_1 )
+    local hoisted_2_1, hoisted_3_1, deduped_4_1, deduped_5_1, deduped_6_1;
+    deduped_6_1 := Length( a_1 );
+    deduped_5_1 := Length( b_1 );
+    deduped_4_1 := deduped_6_1 * deduped_5_1;
+    hoisted_3_1 := deduped_4_1 * GeometricSumDiff1( deduped_4_1, deduped_6_1 );
+    hoisted_2_1 := GeometricSum( deduped_4_1, deduped_6_1 );
+    return CreateCapCategoryMorphismWithAttributes( cat_1, b_1, r_1, AsList, List( [ 0 .. deduped_5_1 - 1 ], function ( i_2 )
+              return hoisted_3_1 + deduped_6_1 * i_2 * hoisted_2_1;
+          end ) );
+end
+########
+
+    , 301 : IsPrecompiledDerivation := true );
+
     ##
     AddCartesianRightEvaluationMorphismWithGivenSource( cat,