From 3c7d7be8797c9ea2a2d00c1db5e782257b9158a0 Mon Sep 17 00:00:00 2001
From: Mohamed Barakat <mohamed.barakat@rwth-aachen.de>
Date: Tue, 17 Oct 2023 18:44:00 +0200
Subject: [PATCH] derived ImageEmbedding as the colift along the coastriction
 to image

---
 CAP/PackageInfo.g                 |  2 +-
 CAP/gap/DerivedMethods.autogen.gi | 28 ++++++++++++++++++++++++++++
 CAP/gap/DerivedMethods.gi         | 30 ++++++++++++++++++++++++++++++
 3 files changed, 59 insertions(+), 1 deletion(-)

diff --git a/CAP/PackageInfo.g b/CAP/PackageInfo.g
index c5883207ff..3a0dedd938 100644
--- a/CAP/PackageInfo.g
+++ b/CAP/PackageInfo.g
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "CAP",
 Subtitle := "Categories, Algorithms, Programming",
-Version := "2023.10-07",
+Version := "2023.10-08",
 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",
 
diff --git a/CAP/gap/DerivedMethods.autogen.gi b/CAP/gap/DerivedMethods.autogen.gi
index 1a110c04da..9d75c4479a 100644
--- a/CAP/gap/DerivedMethods.autogen.gi
+++ b/CAP/gap/DerivedMethods.autogen.gi
@@ -135,6 +135,20 @@ end : CategoryFilter := IsCapCategory,
       Weight := 1,
       is_autogenerated_by_CompilerForCAP := true );
 
+##
+AddDerivationToCAP( CoimageProjection,
+                    "dualizing the derivation of ImageEmbedding by ImageEmbedding as the colift along the coastriction to image",
+                    [
+                        [ AstrictionToCoimage, 1 ],
+                        [ Lift, 1 ],
+                    ],
+                    
+  function ( cat_1, alpha_1 )
+    return Lift( cat_1, alpha_1, AstrictionToCoimage( cat_1, alpha_1 ) );
+end : CategoryFilter := IsCapCategory,
+      Weight := 1,
+      is_autogenerated_by_CompilerForCAP := true );
+
 ##
 AddDerivationToCAP( CoimageProjection,
                     "dualizing the derivation of ImageEmbedding by ImageEmbedding as the kernel embedding of the cokernel projection",
@@ -151,6 +165,20 @@ end : CategoryFilter := IsAbelianCategory,
       Weight := 1,
       is_autogenerated_by_CompilerForCAP := true );
 
+##
+AddDerivationToCAP( CoimageProjectionWithGivenCoimageObject,
+                    "dualizing the derivation of ImageEmbeddingWithGivenImageObject by ImageEmbeddingWithGivenImageObject as the colift along the coastriction to image",
+                    [
+                        [ AstrictionToCoimageWithGivenCoimageObject, 1 ],
+                        [ Lift, 1 ],
+                    ],
+                    
+  function ( cat_1, alpha_1, C_1 )
+    return Lift( cat_1, alpha_1, AstrictionToCoimageWithGivenCoimageObject( cat_1, alpha_1, C_1 ) );
+end : CategoryFilter := IsCapCategory,
+      Weight := 1,
+      is_autogenerated_by_CompilerForCAP := true );
+
 ##
 AddDerivationToCAP( CokernelColift,
                     "dualizing the derivation of KernelLift by KernelLift using LiftAlongMonomorphism and KernelEmbedding",
diff --git a/CAP/gap/DerivedMethods.gi b/CAP/gap/DerivedMethods.gi
index fa494e8db4..9ee955d4ed 100644
--- a/CAP/gap/DerivedMethods.gi
+++ b/CAP/gap/DerivedMethods.gi
@@ -435,6 +435,36 @@ AddDerivationToCAP( UniversalMorphismIntoEqualizer,
     
   end );
 
+##
+AddDerivationToCAP( ImageEmbedding,
+                    "ImageEmbedding as the colift along the coastriction to image",
+                    [ [ CoastrictionToImage, 1 ],
+                      [ Colift, 1 ] ],
+                    
+  function( cat, mor )
+    local coastriction_to_image;
+    
+    coastriction_to_image := CoastrictionToImage( cat, mor );
+    
+    return Colift( cat, coastriction_to_image, mor );
+    
+  end );
+
+##
+AddDerivationToCAP( ImageEmbeddingWithGivenImageObject,
+                    "ImageEmbeddingWithGivenImageObject as the colift along the coastriction to image",
+                    [ [ CoastrictionToImageWithGivenImageObject, 1 ],
+                      [ Colift, 1 ] ],
+                    
+  function( cat, mor, image_object )
+    local coastriction_to_image;
+    
+    coastriction_to_image := CoastrictionToImageWithGivenImageObject( cat, mor, image_object );
+    
+    return Colift( cat, coastriction_to_image, mor );
+    
+  end );
+
 ##
 AddDerivationToCAP( ImageEmbedding,
                     "ImageEmbedding as the kernel embedding of the cokernel projection",