Merge pull request #225 from mohamed-barakat/CoimageProjection

AddAstrictionToCoimage

Author: zickgraf

PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "FinSetsForCAP",
 Subtitle := "The elementary topos of (skeletal) finite sets",
-Version := "2023.10-02",
+Version := "2023.10-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",
@@ -100,7 +100,7 @@ Dependencies := rec(
   NeededOtherPackages := [
                    [ "CAP", ">= 2023.09-11" ],
                    [ "CartesianCategories", ">= 2023.08-13" ],
-                   [ "Toposes", ">= 2023.10-01" ],
+                   [ "Toposes", ">= 2023.10-13" ],
                    ],
   SuggestedOtherPackages := [ ],
   ExternalConditions := [ ],

doc/Doc.autodoc

@@ -106,6 +106,9 @@
 @InsertChunk SkeletalImageEmbedding
 @InsertChunk SkeletalCoastrictionToImage
 
+@Subsection Skeletal Coimage
+@InsertChunk SkeletalCoimageObject
+
 @Subsection Skeletal Preimage
 @InsertChunk SkeletalPreimage
 

examples/CoimageObject.g

@@ -22,10 +22,11 @@ IsEpimorphism( phi );
 #! false
 IsSplitEpimorphism( phi );
 #! false
-iota := AstrictionToCoimage( phi );
-#! <A morphism in FinSets>
 pi := CoimageProjection( phi );
 #! <An epimorphism in FinSets>
+iota := AstrictionToCoimage( phi );
+#! <A morphism in FinSets>
 PreCompose( pi, iota ) = phi;
 #! true
+
 #! @EndExample

examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g

@@ -8,7 +8,7 @@
 
 LoadPackage( "FinSetsForCAP", false );
 #! true
-LoadPackage( "CompilerForCAP", false );
+LoadPackage( "CompilerForCAP", ">= 2023.10-03", false );
 #! true
 
 ReadPackage( "FinSetsForCAP", "gap/CompilerLogic.gi" );
@@ -24,6 +24,8 @@ primitive_operations :=
           category_constructor( : no_precompiled_code := true ) );;
 list_of_operations :=
   SortedList( Concatenation( primitive_operations, [
+          "CoastrictionToImage",
+          "CoimageProjection",
           "IsHomSetInhabited",
           "TruthMorphismOfImplies",
           #"HasPushoutComplement",

examples/SkeletalCoimageObject.g

@@ -0,0 +1,32 @@
+#! @Chunk SkeletalCoimageObject
+
+#! @Example
+LoadPackage( "FinSetsForCAP", false );
+#! true
+m := FinSet( 3 );
+#! |3|
+n := FinSet( 3 );
+#! |3|
+phi := MapOfFinSets( m, [ 1, 0, 1 ], n );
+#! |3| → |3|
+I := CoimageObject( phi );
+#! |2|
+IsMonomorphism( phi );
+#! false
+IsSplitMonomorphism( phi );
+#! false
+IsEpimorphism( phi );
+#! false
+IsSplitEpimorphism( phi );
+#! false
+pi := CoimageProjection( phi );
+#! |3| → |2|
+iota := AstrictionToCoimage( phi );
+#! |2| → |3|
+PreCompose( pi, iota ) = phi;
+#! true
+Display( iota );
+#! { 0, 1 } ⱶ[ 1, 0 ]→ { 0, 1, 2 }
+Display( ImageEmbedding( phi ) );
+#! { 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1, 2 }
+#! @EndExample

gap/SkeletalFinSets.gi

@@ -356,14 +356,6 @@ AddPreCompose( SkeletalFinSets,
 
 end );
 
-##
-AddImageObject( SkeletalFinSets,
-  function ( cat, phi )
-    
-    return ObjectConstructor( cat, BigInt( Length( Set( AsList( phi ) ) ) ) );
-    
-end );
-
 ## the function SKELETAL_FIN_SETS_IsEpimorphism
 ## has linear runtime complexity
 AddIsEpimorphism( SkeletalFinSets,
@@ -484,36 +476,32 @@ AddColift( SkeletalFinSets,
 end );
 
 ##
-AddImageEmbeddingWithGivenImageObject( SkeletalFinSets,
-  function ( cat, phi, image )
+AddImageEmbedding( SkeletalFinSets,
+  function ( cat, phi )
+    local map;
+    
+    map := Set( AsList( phi ) );
+    
+    return MorphismConstructor( cat, ObjectConstructor( cat, BigInt( Length( map ) ) ), map, Range( phi ) );
 
-    return MorphismConstructor( cat, image, Set( AsList( phi ) ), Range( phi ) );
-
 end );
 
 ##
-AddCoastrictionToImageWithGivenImageObject( SkeletalFinSets,
-  function ( cat, phi, image_object )
-    local G, images, s, L, l, pi;
-    
-    G := AsList( phi );
-    
-    images := Set( G );
-    
-    s := Source( phi );
-    
-    L := List( s, i -> -1 + BigInt( SafePosition( images, G[1 + i] ) ) );
+AddAstrictionToCoimage( SkeletalFinSets,
+  function ( cat, phi )
+    local L, map;
 
-    pi := MorphismConstructor( cat, s, L, image_object );
+    L := AsList( phi );
 
-    #% CAP_JIT_DROP_NEXT_STATEMENT
-    Assert( 3, IsEpimorphism( cat, pi ) );
+    ## unlike ImageObject which is a subobject of the range,
+    ## the CoimageObject is a factor object of the source,
+    ## and we want to retain the sorting of the source:
+    map := DuplicateFreeList( L );
 
-    return pi;
+    return MorphismConstructor( cat, ObjectConstructor( cat, BigInt( Length( map ) ) ), map, Range( phi ) );
 
 end );
 
-
 ## Limits
 
 ##

gap/precompiled_categories/SkeletalCategoryOfFiniteSetsWithMorphismsGivenByListsPrecompiled.gi

@@ -5,6 +5,19 @@
 #
 BindGlobal( "ADD_FUNCTIONS_FOR_SkeletalCategoryOfFiniteSetsWithMorphismsGivenByListsPrecompiled", function ( cat )
 
+    ##
+    AddAstrictionToCoimage( cat,
+        
+########
+function ( cat_1, alpha_1 )
+    local deduped_1_1;
+    deduped_1_1 := DuplicateFreeList( AsList( alpha_1 ) );
+    return CreateCapCategoryMorphismWithAttributes( cat_1, CreateCapCategoryObjectWithAttributes( cat_1, Length, BigInt( Length( deduped_1_1 ) ) ), Range( alpha_1 ), AsList, deduped_1_1 );
+end
+########
+        
+    , 100 );
+    
     ##
     AddCartesianBraidingInverseWithGivenDirectProducts( cat,
 
@@ -157,21 +170,21 @@ end
     , 100 );
 
     ##
-    AddCoastrictionToImageWithGivenImageObject( cat,
+    AddCoastrictionToImage( cat,
 
 ########
-function ( cat_1, alpha_1, I_1 )
-    local hoisted_2_1, deduped_3_1, deduped_4_1;
-    deduped_4_1 := AsList( alpha_1 );
-    deduped_3_1 := Source( alpha_1 );
-    hoisted_2_1 := SSortedList( deduped_4_1 );
-    return CreateCapCategoryMorphismWithAttributes( cat_1, deduped_3_1, I_1, AsList, List( [ 0 .. Length( deduped_3_1 ) - 1 ], function ( i_2 )
-              return -1 + BigInt( SafePosition( hoisted_2_1, deduped_4_1[(1 + i_2)] ) );
+function ( cat_1, alpha_1 )
+    local deduped_3_1, deduped_4_1, deduped_5_1;
+    deduped_5_1 := AsList( alpha_1 );
+    deduped_4_1 := Source( alpha_1 );
+    deduped_3_1 := SSortedList( deduped_5_1 );
+    return CreateCapCategoryMorphismWithAttributes( cat_1, deduped_4_1, CreateCapCategoryObjectWithAttributes( cat_1, Length, BigInt( Length( deduped_3_1 ) ) ), AsList, List( [ 0 .. Length( deduped_4_1 ) - 1 ], function ( x_2 )
+              return -1 + BigInt( SafePosition( deduped_3_1, deduped_5_1[(1 + x_2)] ) );
           end ) );
 end
 ########
 
-    , 100 );
+    , 202 : IsPrecompiledDerivation := true );
 
     ##
     AddCoequalizer( cat,
@@ -184,6 +197,23 @@ end
 
     , 100 );
 
+    ##
+    AddCoimageProjection( cat,
+        
+########
+function ( cat_1, alpha_1 )
+    local deduped_3_1, deduped_4_1, deduped_5_1;
+    deduped_5_1 := AsList( alpha_1 );
+    deduped_4_1 := Source( alpha_1 );
+    deduped_3_1 := DuplicateFreeList( deduped_5_1 );
+    return CreateCapCategoryMorphismWithAttributes( cat_1, deduped_4_1, CreateCapCategoryObjectWithAttributes( cat_1, Length, BigInt( Length( deduped_3_1 ) ) ), AsList, List( [ 0 .. Length( deduped_4_1 ) - 1 ], function ( x_2 )
+              return -1 + BigInt( SafePosition( deduped_3_1, deduped_5_1[(1 + x_2)] ) );
+          end ) );
+end
+########
+        
+    , 202 : IsPrecompiledDerivation := true );
+    
     ##
     AddColift( cat,
 
@@ -345,22 +375,13 @@ end
     , 100 );
 
     ##
-    AddImageEmbeddingWithGivenImageObject( cat,
+    AddImageEmbedding( cat,
 
 ########
-function ( cat_1, alpha_1, I_1 )
-    return CreateCapCategoryMorphismWithAttributes( cat_1, I_1, Range( alpha_1 ), AsList, SSortedList( AsList( alpha_1 ) ) );
-end
-########
-        
-    , 100 );
-    
-    ##
-    AddImageObject( cat,
-        
-########
-function ( cat_1, arg2_1 )
-    return CreateCapCategoryObjectWithAttributes( cat_1, Length, BigInt( Length( SSortedList( AsList( arg2_1 ) ) ) ) );
+function ( cat_1, alpha_1 )
+    local deduped_1_1;
+    deduped_1_1 := SSortedList( AsList( alpha_1 ) );
+    return CreateCapCategoryMorphismWithAttributes( cat_1, CreateCapCategoryObjectWithAttributes( cat_1, Length, BigInt( Length( deduped_1_1 ) ) ), Range( alpha_1 ), AsList, deduped_1_1 );
 end
 ########
 
@@ -816,7 +837,7 @@ function ( cat_1, l_1, m_1 )
 end
 ########
 
-    , 19767 : IsPrecompiledDerivation := true );
+    , 19464 : IsPrecompiledDerivation := true );
 
     ##
     AddSomeInjectiveObject( cat,