derived ImageEmbedding as the colift along the coastriction to image

for IsAbelianCategory

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 := IsAbelianCategory,
+ 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 := IsAbelianCategory,
+ 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 : CategoryFilter := IsAbelianCategory ); ##FIXME: PreAbelian?
+
+##
+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 : CategoryFilter := IsAbelianCategory ); ##FIXME: PreAbelian?
+
 ##
 AddDerivationToCAP( ImageEmbedding,
  "ImageEmbedding as the kernel embedding of the cokernel projection",