AddDerivationToCAP( MorphismFromCoimageToImageWithGivenObjects, ... )

homalg-project · Oct 4, 2023 · c60dc43 · c60dc43
1 parent 1ec4f9f
commit c60dc43
Showing 1 changed file with 15 additions and 0 deletions.
diff --git a/CAP/gap/DerivedMethods.gi b/CAP/gap/DerivedMethods.gi
@@ -2907,6 +2907,21 @@ AddFinalDerivationBundle( "IsomorphismFromImageObjectToKernelOfCokernel as the i
   end,
 ] : CategoryFilter := IsAbelianCategory );
 
+##
+AddDerivationToCAP( MorphismFromCoimageToImageWithGivenObjects,
+                    "MorphismFromCoimageToImageWithGivenObjects using that the image embedding lifts the coimage astriction",
+                    [ [ ImageEmbeddingWithGivenImageObject, 1 ],
+                      [ AstrictionToCoimageWithGivenCoimageObject, 1 ],
+                      [ LiftAlongMonomorphism, 1 ] ],
+
+  function( cat, coimage, morphism, image )
+
+    return LiftAlongMonomorphism( cat,
+                   ImageEmbeddingWithGivenImageObject( cat, morphism, image ),
+                   AstrictionToCoimageWithGivenCoimageObject( cat, morphism, coimage ) );
+
+end );
+
 ##
 AddDerivationToCAP( MorphismFromCoimageToImageWithGivenObjects,
                     "MorphismFromCoimageToImageWithGivenObjects using that images are given by kernels of cokernels",