AddIsColiftable + AddColift for FinSets

Author: mohamed-barakat

PackageInfo.g

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

doc/Doc.autodoc

@@ -52,6 +52,9 @@
 @Subsection Lift
 @InsertChunk Lift
 
+@Subsection Colift
+@InsertChunk Colift
+
 @Subsection Topos properties
 @InsertChunk Topos
 

examples/Colift.g

@@ -0,0 +1,30 @@
+#! @Chunk Colift
+
+LoadPackage( "FinSetsForCAP" );
+
+#! @Example
+m := FinSet( [ 1 .. 5 ] );
+#! <An object in FinSets>
+n := FinSet( [ 1 .. 4 ] );
+#! <An object in FinSets>
+f := MapOfFinSets(
+             m,
+             [ [ 1, 2 ], [ 2, 2 ], [ 3, 1 ], [ 4, 1 ], [ 5, 3 ] ],
+             n );
+#! <A morphism in FinSets>
+g := MapOfFinSets(
+             m,
+             [ [ 1, 5 ], [ 2, 5 ], [ 3, 4 ], [ 4, 4 ], [ 5, 5 ] ],
+             m );
+#! <A morphism in FinSets>
+IsColiftable( f, g );
+#! true
+chi := Colift( f, g );
+#! <A morphism in FinSets>
+Display( chi );
+#! [ [ 1 .. 4 ], [ [ 1, 4 ], [ 2, 5 ], [ 3, 5 ], [ 4, 1 ] ], [ 1 .. 5 ] ]
+PreCompose( f, Colift( f, g ) ) = g;
+#! true
+IsColiftable( g, f );
+#! false
+#! @EndExample

gap/FinSetsForCAP.gd

@@ -217,6 +217,13 @@ DeclareOperation( "ProjectionOfFinSets",
 DeclareOperation( "Preimage",
         [ IsFiniteSetMap, IsFiniteSet ] );
 
+#! @Description
+#!  Compute an element of the preimage of the element <A>y</A> under the morphism <A>f</A>.
+#! @Arguments f, y
+#! @Returns a GAP object
+DeclareOperation( "ElementOfPreimage",
+        [ IsFiniteSetMap, IsObject ] );
+
 #! @Description
 #!  Compute the image of <A>S_</A> under the morphism <A>f</A>.
 #! @Arguments f, S_

gap/FinSetsForCAP.gi

@@ -352,6 +352,17 @@ InstallMethod( Preimage,
 
 end );
 
+##
+InstallMethod( ElementOfPreimage,
+        "for a CAP map of finite sets and a GAP object",
+        [ IsFiniteSetMap, IsObject ],
+        
+  function ( f, y )
+    
+    return First( Source( f ), x -> IsEqualForElementsOfFinSets( f(x), y ) );
+    
+end );
+
 ##
 InstallMethod( ImageObject,
         "for a CAP map of finite sets and a CAP finite set",
@@ -768,6 +779,42 @@ AddLift( category_of_finite_sets,
 
 end );
 
+## beta \circ alpha^{-1} is again an ordinary function,
+## i.e., fibers of alpha are mapped under beta to the same element
+AddIsColiftable( category_of_finite_sets,
+  function ( category_of_finite_sets, alpha, beta )
+    
+    return ForAll( AsList( ImageObject( alpha ) ),
+                   i -> Length( DuplicateFreeList( List( Preimage( alpha, FinSetNC( category_of_finite_sets, [ i ] ) ), beta ) ) ) = 1 );
+    
+end );
+
+##
+AddColift( category_of_finite_sets,
+  function ( category_of_finite_sets, alpha, beta )
+    local S, T, im_alpha, elm_T, chi;
+    
+    S := Range( alpha );
+    T := Range( beta );
+    
+    im_alpha := AsList( ImageObject( alpha ) );
+    
+    if not IsInitial( T ) then ## this is, e.g., implied by not IsInitial( S ), since we assume a colift exists
+        elm_T := AsList( T )[1];
+    fi;
+    
+    chi :=
+      function ( y )
+        if not y in im_alpha then
+            return [ y, elm_T ];
+        fi;
+        return [ y, beta( ElementOfPreimage( alpha, y ) ) ];
+    end;
+    
+    return MapOfFinSets( S, List( AsList( S ), chi ), T );
+    
+end );
+
 ##
 AddImageEmbedding( category_of_finite_sets,
   function ( category_of_finite_sets, phi )