Merge pull request #1209 from TKuh/KernelOfPairwiseDifferences

Introduce isomorphisms for the equalizer

Author: zickgraf

CAP/PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "CAP",
 Subtitle := "Categories, Algorithms, Programming",
-Version := "2022.12-13",
+Version := "2022.12-14",
 Date := Concatenation( "01/", ~.Version{[ 6, 7 ]}, "/", ~.Version{[ 1 .. 4 ]} ),
 License := "GPL-2.0-or-later",
 

CAP/examples/TerminalCategoryWithMultipleObjects.g

@@ -10,7 +10,7 @@ T := TerminalCategoryWithMultipleObjects( );
 Display( T );
 #! A CAP category with name TerminalCategoryWithMultipleObjects( ):
 #! 
-#! 63 primitive operations were used to derive 282 operations for this category
+#! 63 primitive operations were used to derive 286 operations for this category
 #! which algorithmically
 #! * IsCategoryWithDecidableColifts
 #! * IsCategoryWithDecidableLifts

CAP/examples/TerminalCategoryWithSingleObject.g

@@ -10,7 +10,7 @@ T := TerminalCategoryWithSingleObject( );
 Display( T );
 #! A CAP category with name TerminalCategoryWithSingleObject( ):
 #! 
-#! 63 primitive operations were used to derive 282 operations for this category
+#! 63 primitive operations were used to derive 286 operations for this category
 #! which algorithmically
 #! * IsCategoryWithDecidableColifts
 #! * IsCategoryWithDecidableLifts

CAP/gap/AddFunctions.autogen.gd

@@ -2422,6 +2422,25 @@ DeclareOperation( "AddIsomorphismFromCoequalizerOfCoproductDiagramToPushout",
 DeclareOperation( "AddIsomorphismFromCoequalizerOfCoproductDiagramToPushout",
                   [ IsCapCategory, IsList ] );
 
+#! @Description
+#! The arguments are a category $C$ and a function $F$.
+#! This operation adds the given function $F$
+#! to the category for the basic operation `IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct`.
+#! $F: ( A, D ) \mapsto \mathtt{IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct}(A, D)$.
+#! @Returns nothing
+#! @Arguments C, F
+DeclareOperation( "AddIsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct",
+                  [ IsCapCategory, IsFunction ] );
+
+DeclareOperation( "AddIsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct",
+                  [ IsCapCategory, IsFunction, IsInt ] );
+
+DeclareOperation( "AddIsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct",
+                  [ IsCapCategory, IsList, IsInt ] );
+
+DeclareOperation( "AddIsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct",
+                  [ IsCapCategory, IsList ] );
+
 #! @Description
 #! The arguments are a category $C$ and a function $F$.
 #! This operation adds the given function $F$
@@ -2460,6 +2479,25 @@ DeclareOperation( "AddIsomorphismFromCokernelOfDiagonalDifferenceToPushout",
 DeclareOperation( "AddIsomorphismFromCokernelOfDiagonalDifferenceToPushout",
                   [ IsCapCategory, IsList ] );
 
+#! @Description
+#! The arguments are a category $C$ and a function $F$.
+#! This operation adds the given function $F$
+#! to the category for the basic operation `IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer`.
+#! $F: ( A, D ) \mapsto \mathtt{IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer}(A, D)$.
+#! @Returns nothing
+#! @Arguments C, F
+DeclareOperation( "AddIsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer",
+                  [ IsCapCategory, IsFunction ] );
+
+DeclareOperation( "AddIsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer",
+                  [ IsCapCategory, IsFunction, IsInt ] );
+
+DeclareOperation( "AddIsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer",
+                  [ IsCapCategory, IsList, IsInt ] );
+
+DeclareOperation( "AddIsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer",
+                  [ IsCapCategory, IsList ] );
+
 #! @Description
 #! The arguments are a category $C$ and a function $F$.
 #! This operation adds the given function $F$
@@ -2574,6 +2612,25 @@ DeclareOperation( "AddIsomorphismFromEqualizerOfDirectProductDiagramToFiberProdu
 DeclareOperation( "AddIsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct",
                   [ IsCapCategory, IsList ] );
 
+#! @Description
+#! The arguments are a category $C$ and a function $F$.
+#! This operation adds the given function $F$
+#! to the category for the basic operation `IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct`.
+#! $F: ( A, D ) \mapsto \mathtt{IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct}(A, D)$.
+#! @Returns nothing
+#! @Arguments C, F
+DeclareOperation( "AddIsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct",
+                  [ IsCapCategory, IsFunction ] );
+
+DeclareOperation( "AddIsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct",
+                  [ IsCapCategory, IsFunction, IsInt ] );
+
+DeclareOperation( "AddIsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct",
+                  [ IsCapCategory, IsList, IsInt ] );
+
+DeclareOperation( "AddIsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct",
+                  [ IsCapCategory, IsList ] );
+
 #! @Description
 #! The arguments are a category $C$ and a function $F$.
 #! This operation adds the given function $F$
@@ -2726,6 +2783,25 @@ DeclareOperation( "AddIsomorphismFromKernelOfDiagonalDifferenceToFiberProduct",
 DeclareOperation( "AddIsomorphismFromKernelOfDiagonalDifferenceToFiberProduct",
                   [ IsCapCategory, IsList ] );
 
+#! @Description
+#! The arguments are a category $C$ and a function $F$.
+#! This operation adds the given function $F$
+#! to the category for the basic operation `IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer`.
+#! $F: ( A, D ) \mapsto \mathtt{IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer}(A, D)$.
+#! @Returns nothing
+#! @Arguments C, F
+DeclareOperation( "AddIsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer",
+                  [ IsCapCategory, IsFunction ] );
+
+DeclareOperation( "AddIsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer",
+                  [ IsCapCategory, IsFunction, IsInt ] );
+
+DeclareOperation( "AddIsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer",
+                  [ IsCapCategory, IsList, IsInt ] );
+
+DeclareOperation( "AddIsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer",
+                  [ IsCapCategory, IsList ] );
+
 #! @Description
 #! The arguments are a category $C$ and a function $F$.
 #! This operation adds the given function $F$

CAP/gap/DerivedMethods.gi

@@ -3588,6 +3588,80 @@ AddDerivationToCAP( MereExistenceOfSolutionOfLinearSystemInAbCategory,
   Description := "MereExistenceOfSolutionOfLinearSystemInAbCategory using the homomorphism structure"
 );
 
+## Final methods for Equalizer
+
+##
+AddFinalDerivationBundle( # IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct
+                    [ [ JointPairwiseDifferencesOfMorphismsIntoDirectProduct, 1 ], 
+                      [ KernelObject, 1 ],
+                      [ IdentityMorphism, 1 ] ],
+                    [ Equalizer,
+                      EmbeddingOfEqualizer,
+                      EmbeddingOfEqualizerWithGivenEqualizer,
+                      UniversalMorphismIntoEqualizer,
+                      UniversalMorphismIntoEqualizerWithGivenEqualizer,
+                      IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct,
+                      IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer ],
+[
+  IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct,
+  function( cat, A, diagram )
+    local kernel_of_pairwise_differences;
+    
+    kernel_of_pairwise_differences := KernelObject( cat, JointPairwiseDifferencesOfMorphismsIntoDirectProduct( cat, A, diagram ) );
+    
+    return IdentityMorphism( cat, kernel_of_pairwise_differences );
+    
+  end
+],
+[
+  IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer,
+  function( cat, A, diagram )
+    local kernel_of_pairwise_differences;
+    
+    kernel_of_pairwise_differences := KernelObject( cat, JointPairwiseDifferencesOfMorphismsIntoDirectProduct( cat, A, diagram ) );
+    
+    return IdentityMorphism( cat, kernel_of_pairwise_differences );
+    
+  end
+] : Description := "IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct as the identity of the kernel of the pairwise differences" );
+
+## Final methods for Coequalizer
+
+##
+AddFinalDerivationBundle( # IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct
+                    [ [ JointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ], 
+                      [ CokernelObject, 1 ],
+                      [ IdentityMorphism, 1 ] ],
+                    [ Coequalizer,
+                      ProjectionOntoCoequalizer,
+                      ProjectionOntoCoequalizerWithGivenCoequalizer,
+                      UniversalMorphismFromCoequalizer,
+                      UniversalMorphismFromCoequalizerWithGivenCoequalizer,
+                      IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct,
+                      IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer ],
+[
+  IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct,
+  function( cat, A, diagram )
+    local cokernel_of_pairwise_differences;
+    
+    cokernel_of_pairwise_differences := CokernelObject( cat, JointPairwiseDifferencesOfMorphismsFromCoproduct( cat, A, diagram ) );
+    
+    return IdentityMorphism( cat, cokernel_of_pairwise_differences );
+    
+  end
+],
+[
+  IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer,
+  function( cat, A, diagram )
+    local cokernel_of_pairwise_differences;
+    
+    cokernel_of_pairwise_differences := CokernelObject( cat, JointPairwiseDifferencesOfMorphismsFromCoproduct( cat, A, diagram ) );
+    
+    return IdentityMorphism( cat, cokernel_of_pairwise_differences );
+    
+  end
+] : Description := "IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct as the identity of the kernel of the pairwise differences" );
+
 ## Final methods for FiberProduct
 
 ##

CAP/gap/MethodRecord.gi

@@ -1619,6 +1619,20 @@ UniversalMorphismIntoEqualizerWithGivenEqualizer := rec(
   compatible_with_congruence_of_morphisms := false,
 ),
 
+IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct := rec(
+  filter_list := [ "category", "object", "list_of_morphisms" ],
+  io_type := [ [ "A", "D" ], [ "E", "Delta" ] ],
+  return_type := "morphism",
+  dual_operation := "IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer",
+),
+
+IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer := rec(
+  filter_list := [ "category", "object", "list_of_morphisms" ],
+  io_type := [ [ "A", "D" ], [ "Delta", "E" ] ],
+  return_type := "morphism",
+  dual_operation := "IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct",
+),
+
 FiberProduct := rec(
   filter_list := [ "category", "list_of_morphisms" ],
   dual_operation := "Pushout",
@@ -2049,6 +2063,20 @@ UniversalMorphismFromCoequalizerWithGivenCoequalizer := rec(
   compatible_with_congruence_of_morphisms := false,
 ),
 
+IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct := rec(
+  filter_list := [ "category", "object", "list_of_morphisms" ],
+  io_type := [ [ "A", "D" ], [ "C", "Delta" ] ],
+  return_type := "morphism",
+  dual_operation := "IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer",
+),
+
+IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer := rec(
+  filter_list := [ "category", "object", "list_of_morphisms" ],
+  io_type := [ [ "A", "D" ], [ "Delta", "C" ] ],
+  return_type := "morphism",
+  dual_operation := "IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct",
+),
+
 Pushout := rec(
   filter_list := [ "category", "list_of_morphisms" ],
   dual_operation := "FiberProduct",

CAP/gap/UniversalObjects.gd

@@ -1434,6 +1434,26 @@ DeclareOperation( "EqualizerFunctorialWithGivenEqualizers",
 DeclareOperation( "JointPairwiseDifferencesOfMorphismsIntoDirectProduct",
                   [ IsCapCategoryObject, IsList ] );
 
+#! @Description
+#! The arguments are an object A and a list of morphisms $D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}$.
+#! The output is a morphism
+#! $\mathrm{Equalizer}(D) \rightarrow \Delta$,
+#! where $\Delta$ denotes the kernel object equalizing the morphisms $\beta_i$.
+#! @Returns a morphism in $\mathrm{Hom}(\mathrm{Equalizer}(D), \Delta)$
+#! @Arguments A, D
+DeclareOperation( "IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct",
+                  [ IsCapCategoryObject, IsList ] );
+
+#! @Description
+#! The arguments are an object A and a list of morphisms $D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}$.
+#! The output is a morphism
+#! $\Delta \rightarrow \mathrm{Equalizer}(D)$,
+#! where $\Delta$ denotes the kernel object equalizing the morphisms $\beta_i$.
+#! @Returns a morphism in $\mathrm{Hom}(\Delta, \mathrm{Equalizer}(D))$
+#! @Arguments A, D
+DeclareOperation( "IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer",
+                  [ IsCapCategoryObject, IsList ] );
+
 #! @Chapter Universal Objects
 
 ####################################
@@ -1623,6 +1643,26 @@ DeclareOperation( "CoequalizerFunctorialWithGivenCoequalizers",
 DeclareOperation( "JointPairwiseDifferencesOfMorphismsFromCoproduct",
                   [ IsCapCategoryObject, IsList ] );
 
+#! @Description
+#! The arguments are an object A and a list of morphisms $D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}$.
+#! The output is a morphism
+#! $\mathrm{Coequalizer}(D) \rightarrow \Delta$,
+#! where $\Delta$ denotes the cokernel object coequalizing the morphisms $\beta_i$.
+#! @Returns a morphism in $\mathrm{Hom}(\mathrm{Coequalizer}(D), \Delta)$
+#! @Arguments A, D
+DeclareOperation( "IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct",
+                  [ IsCapCategoryObject, IsList ] );
+
+#! @Description
+#! The arguments are an object A and a list of morphisms $D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}$.
+#! The output is a morphism
+#! $\Delta \rightarrow \mathrm{Coequalizer}(D)$,
+#! where $\Delta$ denotes the cokernel object coequalizing the morphisms $\beta_i$.
+#! @Returns a morphism in $\mathrm{Hom}(\Delta, \mathrm{Coequalizer}(D))$
+#! @Arguments A, D
+DeclareOperation( "IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer",
+                  [ IsCapCategoryObject, IsList ] );
+
 #! @Chapter Universal Objects
 
 ####################################

FreydCategoriesForCAP/gap/CategoryOfRows.autogen.gd

@@ -368,15 +368,19 @@
 #! * <Ref BookName="CAP" Func="IsBijectiveObject" Label="for Is" />
 #! * <Ref BookName="CAP" Func="IsInjective" Label="for Is" />
 #! * <Ref BookName="CAP" Func="IsProjective" Label="for Is" />
+#! * <Ref BookName="CAP" Func="IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct" Label="for Is" />
 #! * <Ref BookName="CAP" Func="IsomorphismFromCoimageToCokernelOfKernel" Label="for Is" />
 #! * <Ref BookName="CAP" Func="IsomorphismFromCokernelOfDiagonalDifferenceToPushout" Label="for Is" />
+#! * <Ref BookName="CAP" Func="IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer" Label="for Is" />
 #! * <Ref BookName="CAP" Func="IsomorphismFromCokernelOfKernelToCoimage" Label="for Is" />
+#! * <Ref BookName="CAP" Func="IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct" Label="for Is" />
 #! * <Ref BookName="CAP" Func="IsomorphismFromFiberProductToKernelOfDiagonalDifference" Label="for Is" />
 #! * <Ref BookName="CAP" Func="IsomorphismFromHomologyObjectToItsConstructionAsAnImageObject" Label="for Is" />
 #! * <Ref BookName="CAP" Func="IsomorphismFromImageObjectToKernelOfCokernel" Label="for Is" />
 #! * <Ref BookName="CAP" Func="IsomorphismFromItsConstructionAsAnImageObjectToHomologyObject" Label="for Is" />
 #! * <Ref BookName="CAP" Func="IsomorphismFromKernelOfCokernelToImageObject" Label="for Is" />
 #! * <Ref BookName="CAP" Func="IsomorphismFromKernelOfDiagonalDifferenceToFiberProduct" Label="for Is" />
+#! * <Ref BookName="CAP" Func="IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer" Label="for Is" />
 #! * <Ref BookName="CAP" Func="IsomorphismFromPushoutToCokernelOfDiagonalDifference" Label="for Is" />
 #! * <Ref BookName="CAP" Func="KernelEmbedding" Label="for Is" />
 #! * <Ref BookName="CAP" Func="KernelEmbeddingWithGivenKernelObject" Label="for Is" />

GradedModulePresentationsForCAP/examples/CohP1.g

@@ -18,7 +18,7 @@ Display( Sgrmod );
 #! A CAP category with name
 #! The category of graded left f.p. modules over Q[x,y] (with weights [ 1, 1 ]):
 #! 
-#! 40 primitive operations were used to derive 207 operations for this category
+#! 40 primitive operations were used to derive 211 operations for this category
 #! which algorithmically
 #! * IsMonoidalCategory
 #! * IsAbelianCategoryWithEnoughProjectives
@@ -80,7 +80,7 @@ Display( CohP1 );
 #! The Serre quotient category of The category of graded left f.p. modules
 #! over Q[x,y] (with weights [ 1, 1 ]) by test function with name: is_artinian:
 #! 
-#! 21 primitive operations were used to derive 164 operations for this category
+#! 21 primitive operations were used to derive 168 operations for this category
 #! which algorithmically
 #! * IsAbelianCategory
 Sh := CanonicalProjection( CohP1 );