Merge pull request #73 from mohamed-barakat/devel

AddCartesianCoevaluationMorphismWithGivenRange( SkeletalFinSets, ... )

Author: zickgraf

PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "FinSetsForCAP",
 Subtitle := "The elementary topos of (skeletal) finite sets",
-Version := "2021.12-07",
+Version := "2021.12-09",
 
 Date := Concatenation( "01/", ~.Version{[ 6, 7 ]}, "/", ~.Version{[ 1 .. 4 ]} ),
 License := "GPL-2.0-or-later",

doc/Doc.autodoc

@@ -46,7 +46,7 @@
 @Subsection Pushout
 @InsertChunk Pushout
 
-@Subsection Cartesian lambda introduction
+@Subsection Cartesian Lambda Introduction
 @InsertChunk CartesianLambdaIntroduction
 
 @Subsection Lift
@@ -112,6 +112,9 @@
 @Subsection Skeletal Pushout
 @InsertChunk SkeletalPushout
 
+@Subsection Skeletal Cartesian Lambda Introduction
+@InsertChunk SkeletalCartesianLambdaIntroduction
+
 @Subsection Skeletal Lift
 @InsertChunk SkeletalLift
 

examples/CartesianLambdaIntroduction.g

@@ -23,4 +23,8 @@ Length( Range( lf ) );
 #! 8
 lf( T[1] ) = f;
 #! true
+elf := CartesianLambdaElimination( S, R, lf );
+#! <A morphism in FinSets>
+elf = f;
+#! true
 #! @EndExample

examples/SkeletalCartesianLambdaIntroduction.g

@@ -0,0 +1,30 @@
+#! @Chunk SkeletalCartesianLambdaIntroduction
+
+LoadPackage( "FinSetsForCAP" );
+
+#! @Example
+S := FinSet( 3 );
+#! <An object in SkeletalFinSets>
+R := FinSet( 2 );
+#! <An object in SkeletalFinSets>
+f := MapOfFinSets( S, [ 2, 2, 1 ], R );
+#! <A morphism in SkeletalFinSets>
+IsWellDefined( f );
+#! true
+T := TerminalObject( SkeletalFinSets );
+#! <An object in SkeletalFinSets>
+IsTerminal( T );
+#! true
+lf := CartesianLambdaIntroduction( f );
+#! <A split monomorphism in SkeletalFinSets>
+Source( lf ) = T;
+#! true
+Display( Range( lf ) );
+#! 8
+Display( lf );
+#! [ 1, [ 7 ], 8 ]
+elf := CartesianLambdaElimination( S, R, lf );
+#! <A morphism in SkeletalFinSets>
+elf = f;
+#! true
+#! @EndExample

examples/SkeletalTopos.g

@@ -31,5 +31,20 @@ CartesianBraidingInverse( M, N );;
 ExponentialOnObjects( M, N );;
 ExponentialOnMorphisms( f, g );;
 CartesianEvaluationMorphism( M, N );;
+CartesianCoevaluationMorphism( M, N );;
+DirectProductToExponentialAdjunctionMap( M, N,
+    UniversalMorphismIntoTerminalObject( DirectProduct( M, N ) )
+);;
+ExponentialToDirectProductAdjunctionMap( M, N,
+    UniversalMorphismFromInitialObject( ExponentialOnObjects( M, N ) )
+);;
+
+M := FinSet( 2 );;
+N := FinSet( 2 );;
+P := FinSet( 1 );;
+Q := FinSet( 2 );;
+CartesianPreComposeMorphism( M, N, P );;
+CartesianPostComposeMorphism( M, N, P );;
+DirectProductExponentialCompatibilityMorphism( [ M, N, P, Q ] );;
 
 #! @EndExample

examples/Topos.g

@@ -45,6 +45,6 @@ P := FinSet( [ "*" ] );;
 Q := FinSet( [ "§", "&" ] );;
 CartesianPreComposeMorphism( M, N, P );;
 CartesianPostComposeMorphism( M, N, P );;
-DirectProductExponentialCompatibilityMorphism( [ M, N, P, Q  ] );;
+DirectProductExponentialCompatibilityMorphism( [ M, N, P, Q ] );;
 
 #! @EndExample

gap/FinSetsForCAP.gi

@@ -1018,7 +1018,7 @@ AddCartesianLambdaIntroduction( category_of_finite_sets,
   function ( category_of_finite_sets, map )
     local I;
 
-    I := TerminalObject( CapCategory( map ) );
+    I := TerminalObject( category_of_finite_sets );
 
     return MapOfFinSetsNC(
                    I,

gap/SkeletalFinSetsForCAP.gi

@@ -804,13 +804,13 @@ end );
 ##
 AddCartesianBraidingInverseWithGivenDirectProducts( SkeletalFinSets,
   function ( cat, MN, M, N, NM )
-    local n, mn;
+    local m, n;
 
-    n := Length( N );
+    m := Length( M );
 
-    mn := Length( MN );
+    n := Length( N );
 
-    return MapOfFinSets( cat, MN, List( [ 0 .. mn - 1 ] , i -> 1 + ( i mod mn ) + QuoInt( i, n ) ), NM );
+    return MapOfFinSets( cat, MN, List( [ 0 .. Length( MN ) - 1 ] , i -> 1 + ( i mod n ) * m + QuoInt( i, n ) ), NM );
 
 end );
 
@@ -858,6 +858,18 @@ AddCartesianEvaluationMorphismWithGivenSource( SkeletalFinSets,
 
 end );
 
+##
+AddCartesianCoevaluationMorphismWithGivenRange( SkeletalFinSets,
+  function ( cat, M, N, HN_MxN )
+    local m, n;
+    
+    m := Length( M );
+    n := Length( N );
+    
+    return MapOfFinSets( cat, M, List( [ 0 .. m - 1 ], i -> 1 + Sum( [ 0 .. n - 1 ], j -> ( i * n + j ) * (m*n)^(n - j - 1) ) ), HN_MxN );
+    
+end );
+
 ##
 AddSubobjectClassifier( SkeletalFinSets,
   function ( cat )

gap/precompiled_categories/CategoryOfSkeletalFinSetsPrecompiled.gi

@@ -10,13 +10,36 @@ BindGlobal( "ADD_FUNCTIONS_FOR_CategoryOfSkeletalFinSetsPrecompiled", function (
 
 ########
 function ( cat_1, s_1, a_1, b_1, r_1 )
-    local hoisted_1_1, hoisted_2_1, deduped_3_1;
-    deduped_3_1 := Length( s_1 );
-    hoisted_2_1 := Length( b_1 );
-    hoisted_1_1 := deduped_3_1;
+    local hoisted_1_1, hoisted_2_1;
+    hoisted_2_1 := Length( a_1 );
+    hoisted_1_1 := Length( b_1 );
+    return ObjectifyMorphismWithSourceAndRangeForCAPWithAttributes( rec(
+           ), cat_1, s_1, r_1, AsList, List( [ 0 .. Length( s_1 ) - 1 ], function ( i_2 )
+              return 1 + i_2 mod hoisted_1_1 * hoisted_2_1 + QUO_INT( i_2, hoisted_1_1 );
+          end ) );
+end
+########
+        
+    , 100 );
+    
+    ##
+    AddCartesianCoevaluationMorphismWithGivenRange( cat,
+        
+########
+function ( cat_1, a_1, b_1, r_1 )
+    local hoisted_1_1, hoisted_2_1, hoisted_3_1, deduped_4_1, deduped_5_1;
+    deduped_5_1 := Length( b_1 );
+    deduped_4_1 := Length( a_1 );
+    hoisted_3_1 := [ 0 .. deduped_5_1 - 1 ];
+    hoisted_2_1 := deduped_4_1 * deduped_5_1;
+    hoisted_1_1 := deduped_5_1;
     return ObjectifyMorphismWithSourceAndRangeForCAPWithAttributes( rec(
-           ), cat_1, s_1, r_1, AsList, List( [ 0 .. deduped_3_1 - 1 ], function ( i_2 )
-              return 1 + i_2 mod hoisted_1_1 + QUO_INT( i_2, hoisted_2_1 );
+           ), cat_1, a_1, r_1, AsList, List( [ 0 .. deduped_4_1 - 1 ], function ( i_2 )
+              local hoisted_1_2;
+              hoisted_1_2 := i_2 * hoisted_1_1;
+              return 1 + Sum( hoisted_3_1, function ( j_3 )
+                        return (hoisted_1_2 + j_3) * hoisted_2_1 ^ (hoisted_1_1 - j_3 - 1);
+                    end );
           end ) );
 end
 ########