installed derivations for Abelian categories

* IsomorphismFromKernelOfCokernelToImageObject * IsomorphismFromCoimageToCokernelOfKernel
homalg-project · Dec 21, 2022 · 8c109da · 8c109da
1 parent 95ca8cb
commit 8c109da
Show file tree

Hide file tree

Showing 4 changed files with 54 additions and 16 deletions.
diff --git a/CAP/PackageInfo.g b/CAP/PackageInfo.g
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "CAP",
 Subtitle := "Categories, Algorithms, Programming",
-Version := "2022.12-15",
+Version := "2022.12-16",
 Date := Concatenation( "01/", ~.Version{[ 6, 7 ]}, "/", ~.Version{[ 1 .. 4 ]} ),
 License := "GPL-2.0-or-later",
 

diff --git a/CAP/gap/DerivedMethods.gi b/CAP/gap/DerivedMethods.gi
@@ -1820,6 +1820,26 @@ AddDerivationToCAP( IsomorphismFromKernelOfCokernelToImageObject,
 
 end : Description := "IsomorphismFromKernelOfCokernelToImageObject as the inverse of IsomorphismFromImageObjectToKernelOfCokernel" );
 
+##
+AddDerivationToCAP( IsomorphismFromKernelOfCokernelToImageObject,
+                    [ [ ImageEmbedding, 1 ],
+                      [ CokernelProjection, 1 ],
+                      [ KernelEmbedding, 1 ],
+                      [ LiftAlongMonomorphism, 1 ] ],
+
+  function( cat, mor )
+    local image_embedding, ker_of_coker_embedding;
+
+    image_embedding := ImageEmbedding( cat, mor );
+
+    ker_of_coker_embedding := KernelEmbedding( cat, CokernelProjection( cat, mor ) );
+
+    return LiftAlongMonomorphism( cat, image_embedding, ker_of_coker_embedding );
+
+  end : CategoryFilter := IsAbelianCategory, ##FIXME: PreAbelian?
+      Description := "IsomorphismFromKernelOfCokernelToImageObject as the unique lift of the kernel of the cokernel along the image embedding"
+);
+
 ##
 AddDerivationToCAP( IsomorphismFromImageObjectToKernelOfCokernel,
 
@@ -1875,6 +1895,26 @@ AddDerivationToCAP( IsomorphismFromCoimageToCokernelOfKernel,
 
 end : Description := "IsomorphismFromCoimageToCokernelOfKernel as the inverse of IsomorphismFromCokernelOfKernelToCoimage" );
 
+##
+AddDerivationToCAP( IsomorphismFromCoimageToCokernelOfKernel,
+                    [ [ CoimageProjection, 1 ],
+                      [ KernelEmbedding, 1 ],
+                      [ CokernelProjection, 1 ],
+                      [ ColiftAlongEpimorphism, 1 ] ],
+
+  function( cat, mor )
+    local coimage_projection, coker_of_ker_projection;
+
+    coimage_projection := CoimageProjection( cat, mor );
+
+    coker_of_ker_projection := CokernelProjection( cat, KernelEmbedding( cat, mor ) );
+
+    return ColiftAlongEpimorphism( cat, coimage_projection, coker_of_ker_projection );
+
+  end : CategoryFilter := IsAbelianCategory, ##FIXME: PreAbelian?
+      Description := "IsomorphismFromCoimageToCokernelOfKernel as the unique colift of the cokernel of the kernel along the coimage projection"
+);
+
 ##
 AddDerivationToCAP( IsomorphismFromFiberProductToKernelOfDiagonalDifference,
 

diff --git a/LinearAlgebraForCAP/PackageInfo.g b/LinearAlgebraForCAP/PackageInfo.g
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "LinearAlgebraForCAP",
 Subtitle := "Category of Matrices over a Field for CAP",
-Version := "2022.12-04",
+Version := "2022.12-05",
 Date := Concatenation( "01/", ~.Version{[ 6, 7 ]}, "/", ~.Version{[ 1 .. 4 ]} ),
 License := "GPL-2.0-or-later",
 
@@ -89,7 +89,7 @@ Dependencies := rec(
   NeededOtherPackages := [ [ "ToolsForHomalg", ">=2015.09.18" ],
                            [ "MatricesForHomalg", ">= 2021.12-01" ],
                            [ "GaussForHomalg", ">= 2021.04-02" ],
-                           [ "CAP", ">= 2022.12-07" ],
+                           [ "CAP", ">= 2022.12-16" ],
                            [ "MonoidalCategories", ">= 2022.06-01" ],
                            ],
   SuggestedOtherPackages := [

diff --git a/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi b/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi
@@ -2165,16 +2165,15 @@ end
 
 ########
 function ( cat_1, C_1, alpha_1, I_1 )
-    local morphism_attr_1_1, deduped_2_1, deduped_3_1, deduped_4_1;
-    deduped_4_1 := UnderlyingRing( cat_1 );
+    local morphism_attr_1_1, deduped_2_1, deduped_3_1;
     deduped_3_1 := UnderlyingMatrix( alpha_1 );
     deduped_2_1 := SyzygiesOfRows( SyzygiesOfColumns( deduped_3_1 ) );
-    morphism_attr_1_1 := RightDivide( HomalgIdentityMatrix( RowRankOfMatrix( deduped_3_1 ), deduped_4_1 ), RightDivide( LeftDivide( BasisOfColumns( deduped_3_1 ), deduped_3_1 ), deduped_2_1 ) * RightDivide( HomalgIdentityMatrix( NumberRows( deduped_2_1 ), deduped_4_1 ), RightDivide( BasisOfRows( deduped_3_1 ), deduped_2_1 ) ) );
+    morphism_attr_1_1 := RightDivide( HomalgIdentityMatrix( RowRankOfMatrix( deduped_3_1 ), UnderlyingRing( cat_1 ) ), RightDivide( LeftDivide( BasisOfColumns( deduped_3_1 ), deduped_3_1 ), deduped_2_1 ) * RightDivide( deduped_2_1, BasisOfRows( deduped_3_1 ) ) );
     return CreateCapCategoryMorphismWithAttributes( cat_1, CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberRows( morphism_attr_1_1 ) ), C_1, UnderlyingMatrix, morphism_attr_1_1 );
 end
 ########
 
-    , 1817 : IsPrecompiledDerivation := true );
+    , 1512 : IsPrecompiledDerivation := true );
 
     ##
     AddIsAutomorphism( cat,
@@ -2603,12 +2602,12 @@ end
 function ( cat_1, alpha_1 )
     local morphism_attr_1_1, deduped_2_1;
     deduped_2_1 := UnderlyingMatrix( alpha_1 );
-    morphism_attr_1_1 := RightDivide( HomalgIdentityMatrix( ColumnRankOfMatrix( deduped_2_1 ), UnderlyingRing( cat_1 ) ), LeftDivide( SyzygiesOfColumns( SyzygiesOfRows( deduped_2_1 ) ), BasisOfColumns( deduped_2_1 ) ) );
+    morphism_attr_1_1 := LeftDivide( BasisOfColumns( deduped_2_1 ), SyzygiesOfColumns( SyzygiesOfRows( deduped_2_1 ) ) );
     return CreateCapCategoryMorphismWithAttributes( cat_1, CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberRows( morphism_attr_1_1 ) ), CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberColumns( morphism_attr_1_1 ) ), UnderlyingMatrix, morphism_attr_1_1 );
 end
 ########
 
-    , 808 : IsPrecompiledDerivation := true );
+    , 503 : IsPrecompiledDerivation := true );
 
     ##
     AddIsomorphismFromCokernelOfDiagonalDifferenceToPushout( cat,
@@ -2984,15 +2983,14 @@ end
 
 ########
 function ( cat_1, alpha_1 )
-    local morphism_attr_1_1, deduped_2_1, deduped_3_1;
-    deduped_3_1 := UnderlyingMatrix( alpha_1 );
-    deduped_2_1 := SyzygiesOfRows( SyzygiesOfColumns( deduped_3_1 ) );
-    morphism_attr_1_1 := RightDivide( HomalgIdentityMatrix( NumberRows( deduped_2_1 ), UnderlyingRing( cat_1 ) ), RightDivide( BasisOfRows( deduped_3_1 ), deduped_2_1 ) );
+    local morphism_attr_1_1, deduped_2_1;
+    deduped_2_1 := UnderlyingMatrix( alpha_1 );
+    morphism_attr_1_1 := RightDivide( SyzygiesOfRows( SyzygiesOfColumns( deduped_2_1 ) ), BasisOfRows( deduped_2_1 ) );
     return CreateCapCategoryMorphismWithAttributes( cat_1, CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberRows( morphism_attr_1_1 ) ), CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberColumns( morphism_attr_1_1 ) ), UnderlyingMatrix, morphism_attr_1_1 );
 end
 ########
 
-    , 808 : IsPrecompiledDerivation := true );
+    , 503 : IsPrecompiledDerivation := true );
 
     ##
     AddIsomorphismFromKernelOfDiagonalDifferenceToFiberProduct( cat,
@@ -4142,12 +4140,12 @@ function ( cat_1, C_1, alpha_1, I_1 )
     local morphism_attr_1_1, deduped_2_1, deduped_3_1;
     deduped_3_1 := UnderlyingMatrix( alpha_1 );
     deduped_2_1 := SyzygiesOfRows( SyzygiesOfColumns( deduped_3_1 ) );
-    morphism_attr_1_1 := RightDivide( LeftDivide( BasisOfColumns( deduped_3_1 ), deduped_3_1 ), deduped_2_1 ) * RightDivide( HomalgIdentityMatrix( NumberRows( deduped_2_1 ), UnderlyingRing( cat_1 ) ), RightDivide( BasisOfRows( deduped_3_1 ), deduped_2_1 ) );
+    morphism_attr_1_1 := RightDivide( LeftDivide( BasisOfColumns( deduped_3_1 ), deduped_3_1 ), deduped_2_1 ) * RightDivide( deduped_2_1, BasisOfRows( deduped_3_1 ) );
     return CreateCapCategoryMorphismWithAttributes( cat_1, C_1, CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberColumns( morphism_attr_1_1 ) ), UnderlyingMatrix, morphism_attr_1_1 );
 end
 ########
 
-    , 1614 : IsPrecompiledDerivation := true );
+    , 1309 : IsPrecompiledDerivation := true );
 
     ##
     AddMorphismFromFiberProductToSink( cat,