derived ImageEmbedding as the colift along the coastriction to image

Author: mohamed-barakat

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",
 

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 ],
+                        [ LiftAlongMonomorphism, 1 ],
+                    ],
+                    
+  function ( cat_1, alpha_1 )
+    return LiftAlongMonomorphism( cat_1, AstrictionToCoimage( cat_1, alpha_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 ],
+                        [ LiftAlongMonomorphism, 1 ],
+                    ],
+                    
+  function ( cat_1, alpha_1, C_1 )
+    return LiftAlongMonomorphism( cat_1, AstrictionToCoimageWithGivenCoimageObject( cat_1, alpha_1, C_1 ), alpha_1 );
+end : CategoryFilter := IsCapCategory,
+      Weight := 1,
+      is_autogenerated_by_CompilerForCAP := true );
+
 ##
 AddDerivationToCAP( CokernelColift,
                     "dualizing the derivation of KernelLift by KernelLift using LiftAlongMonomorphism and KernelEmbedding",

CAP/gap/DerivedMethods.gi

@@ -435,6 +435,36 @@ AddDerivationToCAP( UniversalMorphismIntoEqualizer,
 
   end );
 
+##
+AddDerivationToCAP( ImageEmbedding,
+                    "ImageEmbedding as the colift along the coastriction to image",
+                    [ [ CoastrictionToImage, 1 ],
+                      [ ColiftAlongEpimorphism, 1 ] ],
+                    
+  function( cat, mor )
+    local coastriction_to_image;
+    
+    coastriction_to_image := CoastrictionToImage( cat, mor );
+    
+    return ColiftAlongEpimorphism( cat, coastriction_to_image, mor );
+    
+  end );
+
+##
+AddDerivationToCAP( ImageEmbeddingWithGivenImageObject,
+                    "ImageEmbeddingWithGivenImageObject as the colift along the coastriction to image",
+                    [ [ CoastrictionToImageWithGivenImageObject, 1 ],
+                      [ ColiftAlongEpimorphism, 1 ] ],
+                    
+  function( cat, mor, image_object )
+    local coastriction_to_image;
+    
+    coastriction_to_image := CoastrictionToImageWithGivenImageObject( cat, mor, image_object );
+    
+    return ColiftAlongEpimorphism( cat, coastriction_to_image, mor );
+    
+  end );
+
 ##
 AddDerivationToCAP( ImageEmbedding,
                     "ImageEmbedding as the kernel embedding of the cokernel projection",