From 7f818cc421073b8e34d193a02dee37e16faf75b3 Mon Sep 17 00:00:00 2001
From: Mohamed Barakat <mohamed.barakat@rwth-aachen.de>
Date: Sat, 27 Nov 2021 17:45:55 +0100
Subject: [PATCH] AddIsColiftable + AddColift for FinSets

---
 PackageInfo.g        |  2 +-
 doc/Doc.autodoc      |  3 +++
 examples/Colift.g    | 30 ++++++++++++++++++++++++++++
 gap/FinSetsForCAP.gd |  7 +++++++
 gap/FinSetsForCAP.gi | 47 ++++++++++++++++++++++++++++++++++++++++++++
 5 files changed, 88 insertions(+), 1 deletion(-)
 create mode 100644 examples/Colift.g

diff --git a/PackageInfo.g b/PackageInfo.g
index 0714f02e..e0dd776c 100644
--- a/PackageInfo.g
+++ b/PackageInfo.g
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "FinSetsForCAP",
 Subtitle := "The elementary topos of (skeletal) finite sets",
-Version := "2021.11-16",
+Version := "2021.11-17",
 
 Date := Concatenation( "01/", ~.Version{[ 6, 7 ]}, "/", ~.Version{[ 1 .. 4 ]} ),
 License := "GPL-2.0-or-later",
diff --git a/doc/Doc.autodoc b/doc/Doc.autodoc
index d2c8a7f2..81841fe7 100644
--- a/doc/Doc.autodoc
+++ b/doc/Doc.autodoc
@@ -52,6 +52,9 @@
 @Subsection Lift
 @InsertChunk Lift
 
+@Subsection Colift
+@InsertChunk Colift
+
 @Subsection Topos properties
 @InsertChunk Topos
 
diff --git a/examples/Colift.g b/examples/Colift.g
new file mode 100644
index 00000000..b02edd5b
--- /dev/null
+++ b/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
diff --git a/gap/FinSetsForCAP.gd b/gap/FinSetsForCAP.gd
index a81e8e77..207392d5 100644
--- a/gap/FinSetsForCAP.gd
+++ b/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_
diff --git a/gap/FinSetsForCAP.gi b/gap/FinSetsForCAP.gi
index 47aca091..74e92710 100644
--- a/gap/FinSetsForCAP.gi
+++ b/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",
@@ -770,6 +781,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 )