Add derivations for isomorphisms

- Equalizer of direct product <-> Fiber product
- Coequalizer of coproduct <-> Pushout
- Kernel of joint differences <-> Equalizer
- Cokernel of joint differences <-> Coequalizer

Author: Tom Kuhmichel

CAP/gap/DerivedMethods.gi

@@ -1929,6 +1929,86 @@ AddDerivationToCAP( IsomorphismFromCoimageToCokernelOfKernel,
 
 end : Description := "IsomorphismFromCoimageToCokernelOfKernel as the inverse of IsomorphismFromCokernelOfKernelToCoimage" );
 
+##
+AddDerivationToCAP( IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct,
+          
+  function( cat, A, diagram )
+    local joint_pairwise_differences, equalizer_embedding;
+    
+    joint_pairwise_differences := JointPairwiseDifferencesOfMorphismsIntoDirectProduct( cat, A, diagram );
+    
+    equalizer_embedding := EmbeddingOfEqualizer( cat, A, diagram );
+    
+    return KernelLift( cat, joint_pairwise_differences, Source( equalizer_embedding ), equalizer_embedding );
+    
+end : Description := "IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct using the universal property of the kernel" );
+
+##
+AddDerivationToCAP( IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer,
+          
+  function( cat, A, diagram )
+    local kernel_embedding;
+    
+    kernel_embedding := KernelEmbedding( cat, JointPairwiseDifferencesOfMorphismsIntoDirectProduct( cat, A, diagram ) );
+    
+    return UniversalMorphismIntoEqualizer( cat, A, diagram, Source( kernel_embedding ), kernel_embedding );
+    
+end : Description := "IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer using the universal property of the equalizer" );
+
+##
+AddDerivationToCAP( IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct,
+          
+  function( cat, A, diagram )
+    local cokernel_proj;
+    
+    cokernel_proj := CokernelProjection( cat, JointPairwiseDifferencesOfMorphismsFromCoproduct( cat, A, diagram ) );
+    
+    return UniversalMorphismFromCoequalizer( cat, A, diagram, Range( cokernel_proj ), cokernel_proj );
+    
+end : Description := "IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct using the universal property of the coequalizer" );
+
+##
+AddDerivationToCAP( IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer,
+          
+  function( cat, A, diagram )
+    local joint_pairwise_differences, coequalizer_projection;
+    
+    joint_pairwise_differences := JointPairwiseDifferencesOfMorphismsFromCoproduct( cat, A, diagram );
+    
+    coequalizer_projection := ProjectionOntoCoequalizer( cat, A, diagram );
+    
+    return CokernelColift( cat, joint_pairwise_differences, Range( coequalizer_projection ), coequalizer_projection );
+    
+end : Description := "IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer using the universal property of the cokernel" );
+
+##
+AddDerivationToCAP( IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram,
+                    [ [ DirectProduct, 1 ],
+                      [ PreCompose, 2 ],
+                      [ ProjectionInFactorOfDirectProductWithGivenDirectProduct, 2 ],
+                      [ ProjectionInFactorOfFiberProduct, 2 ],
+                      [ UniversalMorphismIntoDirectProductWithGivenDirectProduct, 1 ],
+                      [ FiberProduct, 1 ],
+                      [ UniversalMorphismIntoEqualizer, 1 ] ],
+                      
+  function( cat, diagram )
+    local sources_of_diagram, direct_product, direct_product_diagram, test_source, fiber_product_embedding;
+    
+    sources_of_diagram := List( diagram, Source );
+    
+    direct_product := DirectProduct( cat, sources_of_diagram );
+    
+    direct_product_diagram := List( [ 1.. Length( sources_of_diagram ) ],
+                                    i -> PreCompose( cat, ProjectionInFactorOfDirectProductWithGivenDirectProduct( cat, sources_of_diagram, i, direct_product ), diagram[ i ] ) );
+    
+    test_source := List( [ 1 .. Length( diagram ) ], i -> ProjectionInFactorOfFiberProduct( cat, diagram, i ) );
+    
+    fiber_product_embedding := UniversalMorphismIntoDirectProductWithGivenDirectProduct( cat, sources_of_diagram, FiberProduct( cat, diagram ), test_source, direct_product );
+    
+    return UniversalMorphismIntoEqualizer( cat, direct_product, direct_product_diagram, Source( fiber_product_embedding ), fiber_product_embedding );
+    
+end : Description := "IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram using the universal property of the equalizer" );
+
 ##
 AddDerivationToCAP( IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram,
                     [ [ IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct, 1 ],
@@ -1940,6 +2020,32 @@ AddDerivationToCAP( IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram
 
 end : Description := "IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram as the inverse of IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct" );
 
+##
+AddDerivationToCAP( IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct,
+                    [ [ PreCompose, 4 ],
+                      [ ProjectionInFactorOfDirectProductWithGivenDirectProduct, 2 ],
+                      [ DirectProduct, 1 ],
+                      [ EmbeddingOfEqualizer, 1 ],
+                      [ UniversalMorphismIntoFiberProduct, 1 ] ],
+                      
+  function( cat, diagram )
+    local sources_of_diagram, direct_product_diagram, direct_product, equalizer_embedding, equalizer_of_direct_product_diagram;
+    
+    sources_of_diagram := List( diagram, Source );
+    
+    direct_product := DirectProduct( cat, sources_of_diagram );
+    
+    direct_product_diagram := List( [ 1.. Length( sources_of_diagram ) ],
+                                    i -> PreCompose( cat, ProjectionInFactorOfDirectProductWithGivenDirectProduct( cat, sources_of_diagram, i, direct_product ), diagram[ i ] ) );
+    
+    equalizer_embedding := EmbeddingOfEqualizer( cat, direct_product, direct_product_diagram );
+    
+    equalizer_of_direct_product_diagram := List( [ 1 .. Length( direct_product_diagram ) ], i -> PreCompose( cat, equalizer_embedding, direct_product_diagram[ i ] ) );
+    
+    return UniversalMorphismIntoFiberProduct( cat, diagram, Source( equalizer_embedding ), equalizer_of_direct_product_diagram );
+    
+end : Description := "IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct using the universal property of the fiber product" );
+
 ##
 AddDerivationToCAP( IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct,
                     [ [ IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram, 1 ],
@@ -1951,6 +2057,32 @@ AddDerivationToCAP( IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct
 
 end : Description := "IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct as the inverse of IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram" );
 
+##
+AddDerivationToCAP( IsomorphismFromPushoutToCoequalizerOfCoproductDiagram,
+                    [ [ Coproduct, 1 ],
+                      [ PreCompose, 4 ],
+                      [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ],
+                      [ ProjectionOntoCoequalizer, 1 ],
+                      [ UniversalMorphismFromPushout, 1 ] ],
+                      
+  function( cat, diagram )
+    local ranges_of_diagram, coproduct, coproduct_diagram, coequalizer_projection, coequalizer_of_coproduct_diagram;
+    
+    ranges_of_diagram := List( diagram, Range );
+    
+    coproduct := Coproduct( cat, ranges_of_diagram );
+    
+    coproduct_diagram := List( [ 1.. Length( ranges_of_diagram ) ],
+                                    i -> PreCompose( cat, diagram[ i ], InjectionOfCofactorOfCoproductWithGivenCoproduct( cat, ranges_of_diagram, i, coproduct ) ) );
+    
+    coequalizer_projection := ProjectionOntoCoequalizer( cat, coproduct, coproduct_diagram );
+    
+    coequalizer_of_coproduct_diagram := List( [ 1 .. Length( coproduct_diagram ) ], i -> PreCompose( cat, coproduct_diagram[ i ], coequalizer_projection ) );
+    
+    return UniversalMorphismFromPushout( cat, diagram, Range( coequalizer_projection ), coequalizer_of_coproduct_diagram );
+    
+end : Description := "IsomorphismFromPushoutToCoequalizerOfCoproductDiagram using the universal property of the pushout" );
+
 ##
 AddDerivationToCAP( IsomorphismFromPushoutToCoequalizerOfCoproductDiagram,
                     [ [ IsomorphismFromCoequalizerOfCoproductDiagramToPushout , 1 ],
@@ -1962,6 +2094,34 @@ AddDerivationToCAP( IsomorphismFromPushoutToCoequalizerOfCoproductDiagram,
 
 end : Description := "IsomorphismFromPushoutToCoequalizerOfCoproductDiagram as the inverse of IsomorphismFromCoequalizerOfCoproductDiagramToPushout" );
 
+##
+AddDerivationToCAP( IsomorphismFromCoequalizerOfCoproductDiagramToPushout,
+                    [ [ Coproduct, 1 ],
+                      [ PreCompose, 2 ],
+                      [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ],
+                      [ InjectionOfCofactorOfPushout, 2 ],
+                      [ UniversalMorphismFromCoproductWithGivenCoproduct, 1 ],
+                      [ Pushout, 1 ],
+                      [ UniversalMorphismFromCoequalizer, 1 ] ],
+                      
+  function( cat, diagram )
+    local ranges_of_diagram, coproduct, coproduct_diagram, test_source, pushout_injection;
+    
+    ranges_of_diagram := List( diagram, Range );
+    
+    coproduct := Coproduct( cat, ranges_of_diagram );
+    
+    coproduct_diagram := List( [ 1.. Length( ranges_of_diagram ) ],
+                                 i -> PreCompose( cat, diagram[ i ], InjectionOfCofactorOfCoproductWithGivenCoproduct( cat, ranges_of_diagram, i, coproduct ) ) );
+    
+    test_source := List( [ 1 .. Length( diagram ) ], i -> InjectionOfCofactorOfPushout( cat, diagram, i ) );
+    
+    pushout_injection := UniversalMorphismFromCoproductWithGivenCoproduct( cat, ranges_of_diagram, Pushout( cat, diagram ), test_source, coproduct );
+    
+    return UniversalMorphismFromCoequalizer( cat, coproduct, coproduct_diagram, Source( pushout_injection ), pushout_injection );
+    
+end : Description := "IsomorphismFromCoequalizerOfCoproductDiagramToPushout using the universal property of the coequalizer" );
+
 ##
 AddDerivationToCAP( IsomorphismFromCoequalizerOfCoproductDiagramToPushout,
                     [ [ IsomorphismFromPushoutToCoequalizerOfCoproductDiagram, 1 ],