From c8f27fbafad476d463b0e3c47deb2b3e58c380d1 Mon Sep 17 00:00:00 2001 From: Fabian Zickgraf Date: Fri, 30 Sep 2022 15:19:18 +0200 Subject: [PATCH] Generate dual derivations automatically --- CAP/PackageInfo.g | 2 +- CAP/gap/CAP.gi | 11 +- CAP/gap/Derivations.gi | 15 +- CAP/gap/DerivedMethods.autogen.gi | 1596 +++++++++++++++++ CAP/gap/DerivedMethods.gi | 1291 +------------ CAP/gap/Finalize.gi | 10 +- CAP/gap/InstallAdds.gi | 2 + CAP/gap/LimitConvenience.gi | 190 +- CAP/gap/LimitConvenienceOutput.gi | 93 - CAP/read.g | 2 + CompilerForCAP/PackageInfo.g | 2 +- CompilerForCAP/gap/LogicTemplates.gi | 28 + CompilerForCAP/gap/PrecompileCategory.gi | 6 +- CompilerForCAP/tst/Logic.tst | 16 +- .../tst/generate_opposite_derivations.tst | 497 +++++ FreydCategoriesForCAP/PackageInfo.g | 2 +- ...veClosureOfRingAsCategory_CompilerLogic.gi | 18 - LinearAlgebraForCAP/PackageInfo.g | 2 +- LinearAlgebraForCAP/gap/CompilerLogic.gi | 9 - .../MatrixCategoryPrecompiled.gi | 74 +- 20 files changed, 2288 insertions(+), 1578 deletions(-) create mode 100644 CAP/gap/DerivedMethods.autogen.gi create mode 100644 CompilerForCAP/tst/generate_opposite_derivations.tst diff --git a/CAP/PackageInfo.g b/CAP/PackageInfo.g index 0b1da8399d..8f8f1d02b5 100644 --- a/CAP/PackageInfo.g +++ b/CAP/PackageInfo.g @@ -10,7 +10,7 @@ SetPackageInfo( rec( PackageName := "CAP", Subtitle := "Categories, Algorithms, Programming", -Version := "2023.09-09", +Version := "2023.09-10", 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", diff --git a/CAP/gap/CAP.gi b/CAP/gap/CAP.gi index 08e0ac9552..28feba1829 100644 --- a/CAP/gap/CAP.gi +++ b/CAP/gap/CAP.gi @@ -243,7 +243,16 @@ InstallGlobalFunction( "CreateCapCategoryWithDataTypes", obj!.is_computable := CAP_INTERNAL_RETURN_OPTION_OR_DEFAULT( "is_computable", true ); - obj!.derivations_weight_list := MakeOperationWeightList( obj, CAP_INTERNAL_DERIVATION_GRAPH ); + if ValueOption( "disable_derivations" ) = true then + + # use an empty derivation graph + obj!.derivations_weight_list := MakeOperationWeightList( obj, MakeDerivationGraph( Operations( CAP_INTERNAL_DERIVATION_GRAPH ) ) ); + + else + + obj!.derivations_weight_list := MakeOperationWeightList( obj, CAP_INTERNAL_DERIVATION_GRAPH ); + + fi; obj!.caches := rec( ); diff --git a/CAP/gap/Derivations.gi b/CAP/gap/Derivations.gi index 8db91c4c91..2e0b186a09 100644 --- a/CAP/gap/Derivations.gi +++ b/CAP/gap/Derivations.gi @@ -33,7 +33,7 @@ InstallMethod( MakeDerivation, [ IsString, IsFunction, IsDenseList, IsPosInt, IsFunction, IsFunction ], function( name, target_op, used_op_names_with_multiples_and_category_getters, weight, func, category_filter ) - local wrapped_category_filter; + local wrapped_category_filter, derivation; #= comment for Julia if PositionSublist( String( category_filter ), "CanCompute" ) <> fail then @@ -70,7 +70,7 @@ function( name, target_op, used_op_names_with_multiples_and_category_getters, we fi; - return ObjectifyWithAttributes( + derivation := ObjectifyWithAttributes( rec( ), TheTypeOfDerivedMethods, DerivationName, name, DerivationWeight, weight, @@ -80,6 +80,17 @@ function( name, target_op, used_op_names_with_multiples_and_category_getters, we UsedOperationsWithMultiplesAndCategoryGetters, used_op_names_with_multiples_and_category_getters ); + derivation!.is_with_given_derivation := CAP_INTERNAL_RETURN_OPTION_OR_DEFAULT( "is_with_given_derivation", false ); + derivation!.is_autogenerated_by_CompilerForCAP := CAP_INTERNAL_RETURN_OPTION_OR_DEFAULT( "is_autogenerated_by_CompilerForCAP", false ); + + if derivation!.is_with_given_derivation and derivation!.is_autogenerated_by_CompilerForCAP then + + Error( "WithGiven derivations should not be marked as being autogenerated by CompilerForCAP" ); + + fi; + + return derivation; + end ); InstallMethod( String, diff --git a/CAP/gap/DerivedMethods.autogen.gi b/CAP/gap/DerivedMethods.autogen.gi new file mode 100644 index 0000000000..30b1ed108a --- /dev/null +++ b/CAP/gap/DerivedMethods.autogen.gi @@ -0,0 +1,1596 @@ +# SPDX-License-Identifier: GPL-2.0-or-later +# CAP: Categories, Algorithms, Programming +# +# Implementations +# +# THIS FILE IS AUTOMATICALLY GENERATED, SEE CompilerForCAP/tst/generate_opposite_derivations.tst + +## +AddDerivationToCAP( AdditionForMorphisms, + "dualizing the derivation of AdditionForMorphisms by AdditionForMorphisms(mor1, mor2) as the composition of (mor1,mor2) with the codiagonal morphism", + [ + [ UniversalMorphismFromDirectSum, 1 ], + [ IdentityMorphism, 1 ], + [ UniversalMorphismIntoDirectSum, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, alpha_1, beta_1 ) + local deduped_1_1, deduped_2_1, deduped_3_1; + deduped_3_1 := Source( alpha_1 ); + deduped_2_1 := [ deduped_3_1, deduped_3_1 ]; + deduped_1_1 := IdentityMorphism( cat_1, deduped_3_1 ); + return PostCompose( cat_1, UniversalMorphismFromDirectSum( cat_1, deduped_2_1, Range( alpha_1 ), [ alpha_1, beta_1 ] ), UniversalMorphismIntoDirectSum( cat_1, deduped_2_1, deduped_3_1, [ deduped_1_1, deduped_1_1 ] ) ); +end : CategoryFilter := IsAdditiveCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( AstrictionToCoimage, + "dualizing the derivation of CoastrictionToImage by CoastrictionToImage using that image embedding can be seen as a kernel", + [ + [ CoimageProjection, 1 ], + [ ColiftAlongEpimorphism, 1 ], + ], + + function ( cat_1, alpha_1 ) + return ColiftAlongEpimorphism( cat_1, CoimageProjection( cat_1, alpha_1 ), alpha_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( AstrictionToCoimageWithGivenCoimageObject, + "dualizing the derivation of CoastrictionToImageWithGivenImageObject by CoastrictionToImage using that image embedding can be seen as a kernel", + [ + [ CoimageProjectionWithGivenCoimageObject, 1 ], + [ ColiftAlongEpimorphism, 1 ], + ], + + function ( cat_1, alpha_1, C_1 ) + return ColiftAlongEpimorphism( cat_1, CoimageProjectionWithGivenCoimageObject( cat_1, alpha_1, C_1 ), alpha_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( CanonicalIdentificationFromImageObjectToCoimage, + "dualizing the derivation of CanonicalIdentificationFromCoimageToImageObject by CanonicalIdentificationFromCoimageToImageObject as the inverse of CanonicalIdentificationFromImageObjectToCoimage", + [ + [ InverseForMorphisms, 1 ], + [ CanonicalIdentificationFromCoimageToImageObject, 1 ], + ], + + function ( cat_1, alpha_1 ) + return InverseForMorphisms( cat_1, CanonicalIdentificationFromCoimageToImageObject( cat_1, alpha_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( CoastrictionToImage, + "dualizing the derivation of AstrictionToCoimage by AstrictionToCoimage as the image embedding", + [ + [ CoimageProjection, 1 ], + [ PostCompose, 1 ], + [ CanonicalIdentificationFromImageObjectToCoimage, 1 ], + ], + + function ( cat_1, alpha_1 ) + return PostCompose( cat_1, CanonicalIdentificationFromImageObjectToCoimage( cat_1, alpha_1 ), CoimageProjection( cat_1, alpha_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( CoastrictionToImageWithGivenImageObject, + "dualizing the derivation of AstrictionToCoimageWithGivenCoimageObject by AstrictionToCoimage as the image embedding", + [ + [ CoimageProjection, 1 ], + [ PostCompose, 1 ], + [ CanonicalIdentificationFromImageObjectToCoimage, 1 ], + ], + + function ( cat_1, alpha_1, I_1 ) + return PostCompose( cat_1, CanonicalIdentificationFromImageObjectToCoimage( cat_1, alpha_1 ), CoimageProjection( cat_1, alpha_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( Coequalizer, + "dualizing the derivation of Equalizer by Equalizer as the source of EmbeddingOfEqualizer", + [ + [ ProjectionOntoCoequalizer, 1 ], + ], + + function ( cat_1, Y_1, morphisms_1 ) + return Range( ProjectionOntoCoequalizer( cat_1, Y_1, morphisms_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( CoequalizerFunctorialWithGivenCoequalizers, + "dualizing the derivation of EqualizerFunctorialWithGivenEqualizers by EqualizerFunctorialWithGivenEqualizers using the universality of the limit", + [ + [ UniversalMorphismFromCoequalizerWithGivenCoequalizer, 1 ], + [ PostCompose, 1 ], + [ ProjectionOntoCoequalizerWithGivenCoequalizer, 1 ], + ], + + function ( cat_1, P_1, morphisms_1, mu_1, morphismsp_1, Pp_1 ) + return UniversalMorphismFromCoequalizerWithGivenCoequalizer( cat_1, Source( mu_1 ), morphisms_1, Pp_1, PostCompose( cat_1, ProjectionOntoCoequalizerWithGivenCoequalizer( cat_1, Range( mu_1 ), morphismsp_1, Pp_1 ), mu_1 ), P_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( CoimageObject, + "dualizing the derivation of ImageObject by ImageObject as the source of ImageEmbedding", + [ + [ CoimageProjection, 1 ], + ], + + function ( cat_1, arg2_1 ) + return Range( CoimageProjection( cat_1, arg2_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( CoimageObject, + "dualizing the derivation of ImageObject by ImageObject as the source of IsomorphismFromImageObjectToKernelOfCokernel", + [ + [ IsomorphismFromCokernelOfKernelToCoimage, 1 ], + ], + + function ( cat_1, arg2_1 ) + return Range( IsomorphismFromCokernelOfKernelToCoimage( cat_1, arg2_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( CoimageObject, + "dualizing the derivation of ImageObject by ImageObject as the range of IsomorphismFromKernelOfCokernelToImageObject", + [ + [ IsomorphismFromCoimageToCokernelOfKernel, 1 ], + ], + + function ( cat_1, arg2_1 ) + return Source( IsomorphismFromCoimageToCokernelOfKernel( cat_1, arg2_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( CoimageObjectFunctorialWithGivenCoimageObjects, + "dualizing the derivation of ImageObjectFunctorialWithGivenImageObjects by ImageObjectFunctorialWithGivenImageObjects using the universality", + [ + [ ColiftAlongEpimorphism, 1 ], + [ CoimageProjectionWithGivenCoimageObject, 2 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, C_1, alpha_1, mu_1, alphap_1, Cp_1 ) + return ColiftAlongEpimorphism( cat_1, CoimageProjectionWithGivenCoimageObject( cat_1, alpha_1, C_1 ), PostCompose( cat_1, CoimageProjectionWithGivenCoimageObject( cat_1, alphap_1, Cp_1 ), mu_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( CoimageProjection, + "dualizing the derivation of ImageEmbedding by ImageEmbedding as the kernel embedding of the cokernel projection", + [ + [ KernelEmbedding, 1 ], + [ CokernelProjection, 1 ], + [ IsomorphismFromCokernelOfKernelToCoimage, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, alpha_1 ) + return PostCompose( cat_1, IsomorphismFromCokernelOfKernelToCoimage( cat_1, alpha_1 ), CokernelProjection( cat_1, KernelEmbedding( cat_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", + [ + [ ColiftAlongEpimorphism, 1 ], + [ CokernelProjection, 1 ], + ], + + function ( cat_1, alpha_1, T_1, tau_1 ) + return ColiftAlongEpimorphism( cat_1, CokernelProjection( cat_1, alpha_1 ), tau_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( CokernelColiftWithGivenCokernelObject, + "dualizing the derivation of KernelLiftWithGivenKernelObject by KernelLift using LiftAlongMonomorphism and KernelEmbedding", + [ + [ ColiftAlongEpimorphism, 1 ], + [ CokernelProjectionWithGivenCokernelObject, 1 ], + ], + + function ( cat_1, alpha_1, T_1, tau_1, P_1 ) + return ColiftAlongEpimorphism( cat_1, CokernelProjectionWithGivenCokernelObject( cat_1, alpha_1, P_1 ), tau_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( CokernelObject, + "dualizing the derivation of KernelObject by KernelObject as the source of KernelEmbedding", + [ + [ CokernelProjection, 1 ], + ], + + function ( cat_1, alpha_1 ) + return Range( CokernelProjection( cat_1, alpha_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( CokernelObjectFunctorialWithGivenCokernelObjects, + "dualizing the derivation of KernelObjectFunctorialWithGivenKernelObjects by KernelObjectFunctorialWithGivenKernelObjects using the universality of the limit", + [ + [ CokernelColiftWithGivenCokernelObject, 1 ], + [ PostCompose, 1 ], + [ CokernelProjectionWithGivenCokernelObject, 1 ], + ], + + function ( cat_1, P_1, alpha_1, mu_1, alphap_1, Pp_1 ) + return CokernelColiftWithGivenCokernelObject( cat_1, alpha_1, Pp_1, PostCompose( cat_1, CokernelProjectionWithGivenCokernelObject( cat_1, alphap_1, Pp_1 ), mu_1 ), P_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( ColiftAlongEpimorphism, + "dualizing the derivation of LiftAlongMonomorphism by LiftAlongMonomorphism using Lift", + [ + [ Colift, 1 ], + ], + + function ( cat_1, epsilon_1, tau_1 ) + return Colift( cat_1, epsilon_1, tau_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( ColiftAlongEpimorphism, + "dualizing the derivation of LiftAlongMonomorphism by LiftAlongMonomorphism by inverting the kernel lift from the source to the kernel of the cokernel of a given monomorphism", + [ + [ KernelEmbedding, 1 ], + [ CokernelColift, 2 ], + [ PostCompose, 1 ], + [ InverseForMorphisms, 1 ], + ], + + function ( cat_1, epsilon_1, tau_1 ) + local deduped_1_1; + deduped_1_1 := KernelEmbedding( cat_1, epsilon_1 ); + return PostCompose( cat_1, CokernelColift( cat_1, deduped_1_1, Range( tau_1 ), tau_1 ), InverseForMorphisms( cat_1, CokernelColift( cat_1, deduped_1_1, Range( epsilon_1 ), epsilon_1 ) ) ); +end : CategoryFilter := IsAbelianCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( ComponentOfMorphismFromCoproduct, + "dualizing the derivation of ComponentOfMorphismIntoDirectProduct by ComponentOfMorphismIntoDirectProduct using ComponentOfMorphismIntoDirectSum", + [ + [ IsomorphismFromDirectSumToCoproduct, 1 ], + [ ComponentOfMorphismFromDirectSum, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, alpha_1, I_1, i_1 ) + return ComponentOfMorphismFromDirectSum( cat_1, PostCompose( cat_1, alpha_1, IsomorphismFromDirectSumToCoproduct( cat_1, I_1 ) ), I_1, i_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( ComponentOfMorphismFromCoproduct, + "dualizing the derivation of ComponentOfMorphismIntoDirectProduct by ComponentOfMorphismIntoDirectProduct by composing with the direct product projection", + [ + [ InjectionOfCofactorOfCoproduct, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, alpha_1, I_1, i_1 ) + return PostCompose( cat_1, alpha_1, InjectionOfCofactorOfCoproduct( cat_1, I_1, i_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( ComponentOfMorphismFromDirectSum, + "dualizing the derivation of ComponentOfMorphismIntoDirectSum by ComponentOfMorphismIntoDirectSum using ComponentOfMorphismIntoDirectProduct", + [ + [ IsomorphismFromCoproductToDirectSum, 1 ], + [ ComponentOfMorphismFromCoproduct, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, alpha_1, S_1, i_1 ) + return ComponentOfMorphismFromCoproduct( cat_1, PostCompose( cat_1, alpha_1, IsomorphismFromCoproductToDirectSum( cat_1, S_1 ) ), S_1, i_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( ComponentOfMorphismFromDirectSum, + "dualizing the derivation of ComponentOfMorphismIntoDirectSum by ComponentOfMorphismIntoDirectSum by composing with the direct sum projection", + [ + [ InjectionOfCofactorOfDirectSum, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, alpha_1, S_1, i_1 ) + return PostCompose( cat_1, alpha_1, InjectionOfCofactorOfDirectSum( cat_1, S_1, i_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( Coproduct, + "dualizing the derivation of DirectProduct by DirectProduct as the source of IsomorphismFromDirectProductToDirectSum", + [ + [ IsomorphismFromDirectSumToCoproduct, 1 ], + ], + + function ( cat_1, objects_1 ) + return Range( IsomorphismFromDirectSumToCoproduct( cat_1, objects_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( CoproductFunctorialWithGivenCoproducts, + "dualizing the derivation of DirectProductFunctorialWithGivenDirectProducts by DirectProductFunctorialWithGivenDirectProducts using the universality of the limit", + [ + [ UniversalMorphismFromCoproductWithGivenCoproduct, 1 ], + [ PostCompose, 2 ], + [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ], + ], + + function ( cat_1, P_1, objects_1, L_1, objectsp_1, Pp_1 ) + return UniversalMorphismFromCoproductWithGivenCoproduct( cat_1, objects_1, Pp_1, List( [ 1 .. Length( L_1 ) ], function ( i_2 ) + return PostCompose( cat_1, InjectionOfCofactorOfCoproductWithGivenCoproduct( cat_1, objectsp_1, i_2, Pp_1 ), L_1[i_2] ); + end ), P_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( DirectSumFunctorialWithGivenDirectSums, + "dualizing the derivation of DirectSumFunctorialWithGivenDirectSums by DirectSumFunctorialWithGivenDirectSums using the universality of the limit", + [ + [ UniversalMorphismFromDirectSumWithGivenDirectSum, 1 ], + [ PostCompose, 2 ], + [ InjectionOfCofactorOfDirectSumWithGivenDirectSum, 2 ], + ], + + function ( cat_1, P_1, objects_1, L_1, objectsp_1, Pp_1 ) + return UniversalMorphismFromDirectSumWithGivenDirectSum( cat_1, objects_1, Pp_1, List( [ 1 .. Length( L_1 ) ], function ( i_2 ) + return PostCompose( cat_1, InjectionOfCofactorOfDirectSumWithGivenDirectSum( cat_1, objectsp_1, i_2, Pp_1 ), L_1[i_2] ); + end ), P_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( ImageEmbedding, + "dualizing the derivation of CoimageProjection by CoimageProjection as the coastriction to image", + [ + [ CanonicalIdentificationFromCoimageToImageObject, 1 ], + [ AstrictionToCoimage, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, alpha_1 ) + return PostCompose( cat_1, AstrictionToCoimage( cat_1, alpha_1 ), CanonicalIdentificationFromCoimageToImageObject( cat_1, alpha_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( ImageObject, + "dualizing the derivation of CoimageObject by CoimageObject as the range of CanonicalIdentificationFromImageObjectToCoimage", + [ + [ CanonicalIdentificationFromCoimageToImageObject, 1 ], + ], + + function ( cat_1, arg2_1 ) + return Source( CanonicalIdentificationFromCoimageToImageObject( cat_1, arg2_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( ImageObject, + "dualizing the derivation of CoimageObject by CoimageObject as the source of CanonicalIdentificationFromCoimageToImageObject", + [ + [ CanonicalIdentificationFromImageObjectToCoimage, 1 ], + ], + + function ( cat_1, arg2_1 ) + return Range( CanonicalIdentificationFromImageObjectToCoimage( cat_1, arg2_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( InitialObject, + "dualizing the derivation of TerminalObject by TerminalObject as the source of IsomorphismFromTerminalObjectToZeroObject", + [ + [ IsomorphismFromZeroObjectToInitialObject, 1 ], + ], + + function ( cat_1 ) + return Range( IsomorphismFromZeroObjectToInitialObject( cat_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( InitialObject, + "dualizing the derivation of TerminalObject by TerminalObject as the range of IsomorphismFromZeroObjectToTerminalObject", + [ + [ IsomorphismFromInitialObjectToZeroObject, 1 ], + ], + + function ( cat_1 ) + return Source( IsomorphismFromInitialObjectToZeroObject( cat_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( InitialObjectFunctorial, + "dualizing the derivation of TerminalObjectFunctorial by TerminalObjectFunctorial by taking the identity morphism of TerminalObject", + [ + [ InitialObject, 1 ], + [ IdentityMorphism, 1 ], + ], + + function ( cat_1 ) + return IdentityMorphism( cat_1, InitialObject( cat_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( InitialObjectFunctorialWithGivenInitialObjects, + "dualizing the derivation of TerminalObjectFunctorialWithGivenTerminalObjects by TerminalObjectFunctorialWithGivenTerminalObjects using the universality of the limit", + [ + [ UniversalMorphismFromInitialObjectWithGivenInitialObject, 1 ], + ], + + function ( cat_1, P_1, Pp_1 ) + return UniversalMorphismFromInitialObjectWithGivenInitialObject( cat_1, Pp_1, P_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( InjectionOfCofactorOfCoproduct, + "dualizing the derivation of ProjectionInFactorOfDirectProduct by ProjectionInFactorOfDirectProduct using ProjectionInFactorOfDirectSum", + [ + [ IsomorphismFromDirectSumToCoproduct, 1 ], + [ InjectionOfCofactorOfDirectSum, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, objects_1, k_1 ) + return PostCompose( cat_1, IsomorphismFromDirectSumToCoproduct( cat_1, objects_1 ), InjectionOfCofactorOfDirectSum( cat_1, objects_1, k_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( InjectionOfCofactorOfDirectSum, + "dualizing the derivation of ProjectionInFactorOfDirectSum by ProjectionInFactorOfDirectSum using UniversalMorphismFromDirectSum", + [ + [ IdentityMorphism, 1 ], + [ ZeroMorphism, 2 ], + [ UniversalMorphismIntoDirectSum, 1 ], + ], + + function ( cat_1, objects_1, k_1 ) + local hoisted_1_1, deduped_3_1; + deduped_3_1 := objects_1[k_1]; + hoisted_1_1 := IdentityMorphism( cat_1, deduped_3_1 ); + return UniversalMorphismIntoDirectSum( cat_1, objects_1, deduped_3_1, List( [ 1 .. Length( objects_1 ) ], function ( i_2 ) + if i_2 = k_1 then + return hoisted_1_1; + else + return ZeroMorphism( cat_1, deduped_3_1, objects_1[i_2] ); + fi; + return; + end ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( InjectionOfCofactorOfDirectSum, + "dualizing the derivation of ProjectionInFactorOfDirectSum by ProjectionInFactorOfDirectSum using ProjectionInFactorOfDirectProduct", + [ + [ IsomorphismFromCoproductToDirectSum, 1 ], + [ InjectionOfCofactorOfCoproduct, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, objects_1, k_1 ) + return PostCompose( cat_1, IsomorphismFromCoproductToDirectSum( cat_1, objects_1 ), InjectionOfCofactorOfCoproduct( cat_1, objects_1, k_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( InjectionOfCofactorOfDirectSumWithGivenDirectSum, + "dualizing the derivation of ProjectionInFactorOfDirectSumWithGivenDirectSum by ProjectionInFactorOfDirectSum using UniversalMorphismFromDirectSum", + [ + [ IdentityMorphism, 1 ], + [ ZeroMorphism, 2 ], + [ UniversalMorphismIntoDirectSumWithGivenDirectSum, 1 ], + ], + + function ( cat_1, objects_1, k_1, P_1 ) + local hoisted_1_1, deduped_3_1; + deduped_3_1 := objects_1[k_1]; + hoisted_1_1 := IdentityMorphism( cat_1, deduped_3_1 ); + return UniversalMorphismIntoDirectSumWithGivenDirectSum( cat_1, objects_1, deduped_3_1, List( [ 1 .. Length( objects_1 ) ], function ( i_2 ) + if i_2 = k_1 then + return hoisted_1_1; + else + return ZeroMorphism( cat_1, deduped_3_1, objects_1[i_2] ); + fi; + return; + end ), P_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( InjectionOfCofactorOfPushout, + "dualizing the derivation of ProjectionInFactorOfFiberProduct by ProjectionInFactorOfFiberProduct by composing the embedding of equalizer with the direct product projection", + [ + [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ], + [ PostCompose, 3 ], + [ ProjectionOntoCoequalizer, 1 ], + [ Coproduct, 1 ], + [ ComponentOfMorphismFromCoproduct, 1 ], + [ IsomorphismFromCoequalizerOfCoproductDiagramToPushout, 1 ], + ], + + function ( cat_1, morphisms_1, k_1 ) + local deduped_3_1, deduped_4_1; + deduped_4_1 := List( morphisms_1, Range ); + deduped_3_1 := Coproduct( cat_1, deduped_4_1 ); + return PostCompose( cat_1, IsomorphismFromCoequalizerOfCoproductDiagramToPushout( cat_1, morphisms_1 ), ComponentOfMorphismFromCoproduct( cat_1, ProjectionOntoCoequalizer( cat_1, deduped_3_1, List( [ 1 .. Length( morphisms_1 ) ], function ( i_2 ) + return PostCompose( cat_1, InjectionOfCofactorOfCoproductWithGivenCoproduct( cat_1, deduped_4_1, i_2, deduped_3_1 ), morphisms_1[i_2] ); + end ) ), deduped_4_1, k_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( InjectiveColift, + "dualizing the derivation of ProjectiveLift by ProjectiveLift using Lift", + [ + [ Colift, 1 ], + ], + + function ( cat_1, alpha_1, beta_1 ) + return Colift( cat_1, alpha_1, beta_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( InjectiveEnvelopeObject, + "dualizing the derivation of ProjectiveCoverObject by ProjectiveCoverObject as the source of EpimorphismFromProjectiveCoverObject", + [ + [ MonomorphismIntoInjectiveEnvelopeObject, 1 ], + ], + + function ( cat_1, arg2_1 ) + return Range( MonomorphismIntoInjectiveEnvelopeObject( cat_1, arg2_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( InverseForMorphisms, + "dualizing the derivation of InverseForMorphisms by InverseForMorphisms using LiftAlongMonomorphism of an identity morphism", + [ + [ IdentityMorphism, 1 ], + [ ColiftAlongEpimorphism, 1 ], + ], + + function ( cat_1, alpha_1 ) + return ColiftAlongEpimorphism( cat_1, alpha_1, IdentityMorphism( cat_1, Source( alpha_1 ) ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsCodominating, + "dualizing the derivation of IsDominating by IsDominating using IsLiftableAlongMonomorphism", + [ + [ IsColiftableAlongEpimorphism, 1 ], + ], + + function ( cat_1, arg2_1, arg3_1 ) + return IsColiftableAlongEpimorphism( cat_1, arg3_1, arg2_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsCodominating, + "dualizing the derivation of IsDominating by IsDominating using IsCodominating and duality by cokernel", + [ + [ KernelEmbedding, 2 ], + [ IsDominating, 1 ], + ], + + function ( cat_1, arg2_1, arg3_1 ) + return IsDominating( cat_1, KernelEmbedding( cat_1, arg2_1 ), KernelEmbedding( cat_1, arg3_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsCodominating, + "dualizing the derivation of IsDominating by IsDominating(sub1, sub2) by deciding if sub1 composed with CokernelProjection(cat, sub2) is zero", + [ + [ KernelEmbedding, 1 ], + [ PostCompose, 1 ], + [ IsZeroForMorphisms, 1 ], + ], + + function ( cat_1, arg2_1, arg3_1 ) + return IsZeroForMorphisms( cat_1, PostCompose( cat_1, arg2_1, KernelEmbedding( cat_1, arg3_1 ) ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsColiftable, + "dualizing the derivation of IsLiftable by Two morphisms with equal targets are mutually liftable in a terminal category", + [ + ], + + function ( cat_1, arg2_1, arg3_1 ) + return true; +end : CategoryFilter := IsTerminalCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsColiftableAlongEpimorphism, + "dualizing the derivation of IsLiftableAlongMonomorphism by IsLiftableAlongMonomorphism using IsLiftable", + [ + [ IsColiftable, 1 ], + ], + + function ( cat_1, arg2_1, arg3_1 ) + return IsColiftable( cat_1, arg2_1, arg3_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsEpimorphism, + "dualizing the derivation of IsMonomorphism by IsMonomorphism by deciding if the kernel is a zero object", + [ + [ IsZeroForObjects, 1 ], + [ CokernelObject, 1 ], + ], + + function ( cat_1, arg2_1 ) + return IsZeroForObjects( cat_1, CokernelObject( cat_1, arg2_1 ) ); +end : CategoryFilter := IsAdditiveCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsEpimorphism, + "dualizing the derivation of IsMonomorphism by IsMonomorphism by deciding if the diagonal morphism is an isomorphism", + [ + [ IsIsomorphism, 1 ], + [ IdentityMorphism, 1 ], + [ UniversalMorphismFromPushout, 1 ], + ], + + function ( cat_1, arg2_1 ) + local deduped_1_1, deduped_2_1; + deduped_2_1 := Range( arg2_1 ); + deduped_1_1 := IdentityMorphism( cat_1, deduped_2_1 ); + return IsIsomorphism( cat_1, UniversalMorphismFromPushout( cat_1, [ arg2_1, arg2_1 ], deduped_2_1, [ deduped_1_1, deduped_1_1 ] ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsEqualAsFactorobjects, + "dualizing the derivation of IsEqualAsSubobjects by IsEqualAsSubobjects(sub1, sub2) if sub1 dominates sub2 and vice versa", + [ + [ IsCodominating, 2 ], + ], + + function ( cat_1, arg2_1, arg3_1 ) + return IsCodominating( cat_1, arg2_1, arg3_1 ) and IsCodominating( cat_1, arg3_1, arg2_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsIdempotent, + "dualizing the derivation of IsIdempotent by IsIdempotent by comparing the square of the morphism with itself", + [ + [ IsCongruentForMorphisms, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, arg2_1 ) + return IsCongruentForMorphisms( cat_1, PostCompose( cat_1, arg2_1, arg2_1 ), arg2_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsInitial, + "dualizing the derivation of IsTerminal by IsTerminal using IsZeroForObjects", + [ + [ IsZeroForObjects, 1 ], + ], + + function ( cat_1, arg2_1 ) + return IsZeroForObjects( cat_1, arg2_1 ); +end : CategoryFilter := IsAdditiveCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsInitial, + "dualizing the derivation of IsTerminal by IsTerminal using IsIsomorphism( cat, UniversalMorphismIntoTerminalObject )", + [ + [ IsIsomorphism, 1 ], + [ UniversalMorphismFromInitialObject, 1 ], + ], + + function ( cat_1, arg2_1 ) + return IsIsomorphism( cat_1, UniversalMorphismFromInitialObject( cat_1, arg2_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsInjective, + "dualizing the derivation of IsProjective by IsProjective by checking if the object is a retract of some projective object", + [ + [ MonomorphismIntoSomeInjectiveObject, 1 ], + [ IsSplitMonomorphism, 1 ], + ], + + function ( cat_1, arg2_1 ) + return IsSplitMonomorphism( cat_1, MonomorphismIntoSomeInjectiveObject( cat_1, arg2_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsInjective, + "dualizing the derivation of IsProjective by ", + [ + [ MonomorphismIntoInjectiveEnvelopeObject, 1 ], + [ IsIsomorphism, 1 ], + ], + + function ( cat_1, arg2_1 ) + return IsIsomorphism( cat_1, MonomorphismIntoInjectiveEnvelopeObject( cat_1, arg2_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsIsomorphism, + "dualizing the derivation of IsIsomorphism by IsIsomorphism by deciding if it is a split mono and an epi", + [ + [ IsSplitEpimorphism, 1 ], + [ IsMonomorphism, 1 ], + ], + + function ( cat_1, arg2_1 ) + return IsSplitEpimorphism( cat_1, arg2_1 ) and IsMonomorphism( cat_1, arg2_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsSplitEpimorphism, + "dualizing the derivation of IsSplitMonomorphism by IsSplitMonomorphism by using IsColiftable", + [ + [ IsLiftable, 1 ], + [ IdentityMorphism, 1 ], + ], + + function ( cat_1, arg2_1 ) + return IsLiftable( cat_1, IdentityMorphism( cat_1, Range( arg2_1 ) ), arg2_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromCoequalizerOfCoproductDiagramToPushout, + "dualizing the derivation of IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram by IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram using the universal property of the equalizer", + [ + [ Coproduct, 1 ], + [ PostCompose, 2 ], + [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ], + [ InjectionOfCofactorOfPushoutWithGivenPushout, 2 ], + [ UniversalMorphismFromCoproductWithGivenCoproduct, 1 ], + [ Pushout, 1 ], + [ UniversalMorphismFromCoequalizer, 1 ], + ], + + function ( cat_1, D_1 ) + local deduped_4_1, deduped_5_1, deduped_6_1, deduped_7_1; + deduped_7_1 := Pushout( cat_1, D_1 ); + deduped_6_1 := List( D_1, Range ); + deduped_5_1 := [ 1 .. Length( D_1 ) ]; + deduped_4_1 := Coproduct( cat_1, deduped_6_1 ); + return UniversalMorphismFromCoequalizer( cat_1, deduped_4_1, List( deduped_5_1, function ( i_2 ) + return PostCompose( cat_1, InjectionOfCofactorOfCoproductWithGivenCoproduct( cat_1, deduped_6_1, i_2, deduped_4_1 ), D_1[i_2] ); + end ), deduped_7_1, UniversalMorphismFromCoproductWithGivenCoproduct( cat_1, deduped_6_1, deduped_7_1, List( deduped_5_1, function ( i_2 ) + return InjectionOfCofactorOfPushoutWithGivenPushout( cat_1, D_1, i_2, deduped_7_1 ); + end ), deduped_4_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromCoequalizerOfCoproductDiagramToPushout, + "dualizing the derivation of IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram by IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram as the inverse of IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct", + [ + [ IsomorphismFromPushoutToCoequalizerOfCoproductDiagram, 1 ], + [ InverseForMorphisms, 1 ], + ], + + function ( cat_1, D_1 ) + return InverseForMorphisms( cat_1, IsomorphismFromPushoutToCoequalizerOfCoproductDiagram( cat_1, D_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct, + "dualizing the derivation of IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer by IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer using the universal property of the equalizer", + [ + [ JointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ], + [ CokernelObject, 1 ], + [ CokernelProjectionWithGivenCokernelObject, 1 ], + [ UniversalMorphismFromCoequalizer, 1 ], + ], + + function ( cat_1, A_1, D_1 ) + local deduped_1_1, deduped_2_1; + deduped_2_1 := JointPairwiseDifferencesOfMorphismsFromCoproduct( cat_1, A_1, D_1 ); + deduped_1_1 := CokernelObject( cat_1, deduped_2_1 ); + return UniversalMorphismFromCoequalizer( cat_1, A_1, D_1, deduped_1_1, CokernelProjectionWithGivenCokernelObject( cat_1, deduped_2_1, deduped_1_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromCoimageToCokernelOfKernel, + "dualizing the derivation of IsomorphismFromKernelOfCokernelToImageObject by IsomorphismFromKernelOfCokernelToImageObject as the inverse of IsomorphismFromImageObjectToKernelOfCokernel", + [ + [ InverseForMorphisms, 1 ], + [ IsomorphismFromCokernelOfKernelToCoimage, 1 ], + ], + + function ( cat_1, alpha_1 ) + return InverseForMorphisms( cat_1, IsomorphismFromCokernelOfKernelToCoimage( cat_1, alpha_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer, + "dualizing the derivation of IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct by IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct using the universal property of the kernel", + [ + [ JointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ], + [ Coequalizer, 1 ], + [ ProjectionOntoCoequalizerWithGivenCoequalizer, 1 ], + [ CokernelColift, 1 ], + ], + + function ( cat_1, A_1, D_1 ) + local deduped_1_1; + deduped_1_1 := Coequalizer( cat_1, A_1, D_1 ); + return CokernelColift( cat_1, JointPairwiseDifferencesOfMorphismsFromCoproduct( cat_1, A_1, D_1 ), deduped_1_1, ProjectionOntoCoequalizerWithGivenCoequalizer( cat_1, A_1, D_1, deduped_1_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromCokernelOfKernelToCoimage, + "dualizing the derivation of IsomorphismFromImageObjectToKernelOfCokernel by IsomorphismFromImageObjectToKernelOfCokernel as the inverse of IsomorphismFromKernelOfCokernelToImageObject", + [ + [ InverseForMorphisms, 1 ], + [ IsomorphismFromCoimageToCokernelOfKernel, 1 ], + ], + + function ( cat_1, alpha_1 ) + return InverseForMorphisms( cat_1, IsomorphismFromCoimageToCokernelOfKernel( cat_1, alpha_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromCokernelOfKernelToCoimage, + "dualizing the derivation of IsomorphismFromImageObjectToKernelOfCokernel by IsomorphismFromImageObjectToKernelOfCokernel using the universal property of the image", + [ + [ CokernelProjection, 1 ], + [ KernelEmbedding, 1 ], + [ ColiftAlongEpimorphism, 1 ], + [ UniversalMorphismIntoCoimage, 1 ], + ], + + function ( cat_1, alpha_1 ) + local deduped_1_1; + deduped_1_1 := CokernelProjection( cat_1, KernelEmbedding( cat_1, alpha_1 ) ); + return UniversalMorphismIntoCoimage( cat_1, alpha_1, NTuple( 2, deduped_1_1, ColiftAlongEpimorphism( cat_1, deduped_1_1, alpha_1 ) ) ); +end : CategoryFilter := IsAbelianCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromCoproductToDirectSum, + "dualizing the derivation of IsomorphismFromDirectSumToDirectProduct by IsomorphismFromDirectSumToDirectProduct using direct sum projections and universal property of direct product", + [ + [ InjectionOfCofactorOfDirectSum, 2 ], + [ DirectSum, 1 ], + [ UniversalMorphismFromCoproduct, 1 ], + ], + + function ( cat_1, D_1 ) + return UniversalMorphismFromCoproduct( cat_1, D_1, DirectSum( cat_1, D_1 ), List( [ 1 .. Length( D_1 ) ], function ( i_2 ) + return InjectionOfCofactorOfDirectSum( cat_1, D_1, i_2 ); + end ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromCoproductToDirectSum, + "dualizing the derivation of IsomorphismFromDirectSumToDirectProduct by IsomorphismFromDirectSumToDirectProduct as the inverse of IsomorphismFromDirectProductToDirectSum", + [ + [ InverseForMorphisms, 1 ], + [ IsomorphismFromDirectSumToCoproduct, 1 ], + ], + + function ( cat_1, D_1 ) + return InverseForMorphisms( cat_1, IsomorphismFromDirectSumToCoproduct( cat_1, D_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromDirectSumToCoproduct, + "dualizing the derivation of IsomorphismFromDirectProductToDirectSum by IsomorphismFromDirectProductToDirectSum using direct product projections and universal property of direct sum", + [ + [ InjectionOfCofactorOfCoproduct, 2 ], + [ Coproduct, 1 ], + [ UniversalMorphismFromDirectSum, 1 ], + ], + + function ( cat_1, D_1 ) + return UniversalMorphismFromDirectSum( cat_1, D_1, Coproduct( cat_1, D_1 ), List( [ 1 .. Length( D_1 ) ], function ( i_2 ) + return InjectionOfCofactorOfCoproduct( cat_1, D_1, i_2 ); + end ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromDirectSumToCoproduct, + "dualizing the derivation of IsomorphismFromDirectProductToDirectSum by IsomorphismFromDirectProductToDirectSum as the inverse of IsomorphismFromDirectSumToDirectProduct", + [ + [ IsomorphismFromCoproductToDirectSum, 1 ], + [ InverseForMorphisms, 1 ], + ], + + function ( cat_1, D_1 ) + return InverseForMorphisms( cat_1, IsomorphismFromCoproductToDirectSum( cat_1, D_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromInitialObjectToZeroObject, + "dualizing the derivation of IsomorphismFromZeroObjectToTerminalObject by IsomorphismFromZeroObjectToTerminalObject as the unique morphism from zero object to terminal object", + [ + [ UniversalMorphismFromInitialObject, 1 ], + [ ZeroObject, 1 ], + ], + + function ( cat_1 ) + return UniversalMorphismFromInitialObject( cat_1, ZeroObject( cat_1 ) ); +end : CategoryFilter := IsAdditiveCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromInitialObjectToZeroObject, + "dualizing the derivation of IsomorphismFromZeroObjectToTerminalObject by IsomorphismFromZeroObjectToTerminalObject using the universal property of the zero object", + [ + [ UniversalMorphismIntoZeroObject, 1 ], + [ InitialObject, 1 ], + ], + + function ( cat_1 ) + return UniversalMorphismIntoZeroObject( cat_1, InitialObject( cat_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromInitialObjectToZeroObject, + "dualizing the derivation of IsomorphismFromZeroObjectToTerminalObject by IsomorphismFromZeroObjectToTerminalObject as the inverse of IsomorphismFromTerminalObjectToZeroObject", + [ + [ InverseForMorphisms, 1 ], + [ IsomorphismFromZeroObjectToInitialObject, 1 ], + ], + + function ( cat_1 ) + return InverseForMorphisms( cat_1, IsomorphismFromZeroObjectToInitialObject( cat_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromPushoutToCoequalizerOfCoproductDiagram, + "dualizing the derivation of IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct by IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct using the universal property of the fiber product", + [ + [ PostCompose, 4 ], + [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ], + [ Coproduct, 1 ], + [ Coequalizer, 1 ], + [ ProjectionOntoCoequalizerWithGivenCoequalizer, 1 ], + [ UniversalMorphismFromPushout, 1 ], + ], + + function ( cat_1, D_1 ) + local hoisted_4_1, deduped_5_1, deduped_6_1, deduped_7_1, deduped_8_1, deduped_9_1; + deduped_9_1 := List( D_1, Range ); + deduped_8_1 := [ 1 .. Length( D_1 ) ]; + deduped_7_1 := Coproduct( cat_1, deduped_9_1 ); + deduped_6_1 := List( deduped_8_1, function ( i_2 ) + return PostCompose( cat_1, InjectionOfCofactorOfCoproductWithGivenCoproduct( cat_1, deduped_9_1, i_2, deduped_7_1 ), D_1[i_2] ); + end ); + deduped_5_1 := Coequalizer( cat_1, deduped_7_1, deduped_6_1 ); + hoisted_4_1 := ProjectionOntoCoequalizerWithGivenCoequalizer( cat_1, deduped_7_1, deduped_6_1, deduped_5_1 ); + return UniversalMorphismFromPushout( cat_1, D_1, deduped_5_1, List( deduped_8_1, function ( i_2 ) + return PostCompose( cat_1, hoisted_4_1, deduped_6_1[i_2] ); + end ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromPushoutToCoequalizerOfCoproductDiagram, + "dualizing the derivation of IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct by IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct as the inverse of IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram", + [ + [ IsomorphismFromCoequalizerOfCoproductDiagramToPushout, 1 ], + [ InverseForMorphisms, 1 ], + ], + + function ( cat_1, D_1 ) + return InverseForMorphisms( cat_1, IsomorphismFromCoequalizerOfCoproductDiagramToPushout( cat_1, D_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromZeroObjectToInitialObject, + "dualizing the derivation of IsomorphismFromTerminalObjectToZeroObject by IsomorphismFromTerminalObjectToZeroObject as the inverse of IsomorphismFromZeroObjectToTerminalObject", + [ + [ InverseForMorphisms, 1 ], + [ IsomorphismFromInitialObjectToZeroObject, 1 ], + ], + + function ( cat_1 ) + return InverseForMorphisms( cat_1, IsomorphismFromInitialObjectToZeroObject( cat_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( IsomorphismFromZeroObjectToInitialObject, + "dualizing the derivation of IsomorphismFromTerminalObjectToZeroObject by IsomorphismFromTerminalObjectToZeroObject using the universal property of the zero object", + [ + [ UniversalMorphismFromZeroObject, 1 ], + [ InitialObject, 1 ], + ], + + function ( cat_1 ) + return UniversalMorphismFromZeroObject( cat_1, InitialObject( cat_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( MorphismFromCoimageToImageWithGivenObjects, + "dualizing the derivation of MorphismFromCoimageToImageWithGivenObjects by MorphismFromCoimageToImageWithGivenObjects using that images are given by kernels of cokernels", + [ + [ KernelEmbedding, 1 ], + [ CokernelColift, 1 ], + [ CoastrictionToImageWithGivenImageObject, 1 ], + [ PostCompose, 1 ], + [ IsomorphismFromCoimageToCokernelOfKernel, 1 ], + ], + + function ( cat_1, C_1, alpha_1, I_1 ) + return PostCompose( cat_1, CokernelColift( cat_1, KernelEmbedding( cat_1, alpha_1 ), I_1, CoastrictionToImageWithGivenImageObject( cat_1, alpha_1, I_1 ) ), IsomorphismFromCoimageToCokernelOfKernel( cat_1, alpha_1 ) ); +end : CategoryFilter := IsPreAbelianCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( MorphismFromSourceToCoequalizer, + "dualizing the derivation of MorphismFromEqualizerToSink by MorphismFromEqualizerToSink by composing the embedding with the first morphism in the diagram", + [ + [ ProjectionOntoCoequalizer, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, Y_1, morphisms_1 ) + return PostCompose( cat_1, ProjectionOntoCoequalizer( cat_1, Y_1, morphisms_1 ), morphisms_1[1] ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( MorphismFromSourceToCokernelObject, + "dualizing the derivation of MorphismFromKernelObjectToSink by MorphismFromKernelObjectToSink as zero morphism from kernel object to range", + [ + [ CokernelObject, 1 ], + [ ZeroMorphism, 1 ], + ], + + function ( cat_1, alpha_1 ) + return ZeroMorphism( cat_1, Source( alpha_1 ), CokernelObject( cat_1, alpha_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( MorphismFromSourceToPushout, + "dualizing the derivation of MorphismFromFiberProductToSink by MorphismFromFiberProductToSink by composing the first projection with the first morphism in the diagram", + [ + [ InjectionOfCofactorOfPushout, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, morphisms_1 ) + return PostCompose( cat_1, InjectionOfCofactorOfPushout( cat_1, morphisms_1, 1 ), morphisms_1[1] ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( PostCompose, + "dualizing the derivation of PreCompose by PreCompose using PostCompose and swapping arguments", + [ + [ PreCompose, 1 ], + ], + + function ( cat_1, beta_1, alpha_1 ) + return PreCompose( cat_1, alpha_1, beta_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( PostCompose, + "dualizing the derivation of PreCompose by PreCompose by wrapping the arguments in a list", + [ + [ PostComposeList, 1 ], + ], + + function ( cat_1, beta_1, alpha_1 ) + return PostComposeList( cat_1, Source( alpha_1 ), [ beta_1, alpha_1 ], Range( beta_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( PostComposeList, + "dualizing the derivation of PreComposeList by PreComposeList by iterating PreCompose", + [ + [ IdentityMorphism, 2 ], + [ PostCompose, 2 ], + ], + + function ( cat_1, source_1, list_of_morphisms_1, range_1 ) + return Iterated( list_of_morphisms_1, function ( alpha_2, beta_2 ) + return PostCompose( cat_1, alpha_2, beta_2 ); + end, IdentityMorphism( cat_1, range_1 ), IdentityMorphism( cat_1, source_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( PostInverseForMorphisms, + "dualizing the derivation of PreInverseForMorphisms by PreInverseForMorphisms using IdentityMorphism and Lift", + [ + [ IdentityMorphism, 1 ], + [ Colift, 1 ], + ], + + function ( cat_1, alpha_1 ) + return Colift( cat_1, alpha_1, IdentityMorphism( cat_1, Source( alpha_1 ) ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( ProjectionOntoCoequalizer, + "dualizing the derivation of EmbeddingOfEqualizer by EmbeddingOfEqualizer using the kernel embedding of JointPairwiseDifferencesOfMorphismsIntoDirectProduct", + [ + [ CokernelProjection, 1 ], + [ JointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ], + [ PostCompose, 1 ], + [ IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer, 1 ], + ], + + function ( cat_1, Y_1, morphisms_1 ) + return PostCompose( cat_1, IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer( cat_1, Y_1, morphisms_1 ), CokernelProjection( cat_1, JointPairwiseDifferencesOfMorphismsFromCoproduct( cat_1, Y_1, morphisms_1 ) ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( Pushout, + "dualizing the derivation of FiberProduct by FiberProduct as the source of IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram", + [ + [ IsomorphismFromCoequalizerOfCoproductDiagramToPushout, 1 ], + ], + + function ( cat_1, morphisms_1 ) + return Range( IsomorphismFromCoequalizerOfCoproductDiagramToPushout( cat_1, morphisms_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( PushoutFunctorialWithGivenPushouts, + "dualizing the derivation of FiberProductFunctorialWithGivenFiberProducts by FiberProductFunctorialWithGivenFiberProducts using the universality of the limit", + [ + [ UniversalMorphismFromPushoutWithGivenPushout, 1 ], + [ PostCompose, 2 ], + [ InjectionOfCofactorOfPushoutWithGivenPushout, 2 ], + ], + + function ( cat_1, P_1, morphisms_1, L_1, morphismsp_1, Pp_1 ) + return UniversalMorphismFromPushoutWithGivenPushout( cat_1, morphisms_1, Pp_1, List( [ 1 .. Length( L_1 ) ], function ( i_2 ) + return PostCompose( cat_1, InjectionOfCofactorOfPushoutWithGivenPushout( cat_1, morphismsp_1, i_2, Pp_1 ), L_1[i_2] ); + end ), P_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( SomeInjectiveObject, + "dualizing the derivation of SomeProjectiveObject by SomeProjectiveObject as the source of EpimorphismFromSomeProjectiveObject", + [ + [ MonomorphismIntoSomeInjectiveObject, 1 ], + ], + + function ( cat_1, arg2_1 ) + return Range( MonomorphismIntoSomeInjectiveObject( cat_1, arg2_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromCoequalizer, + "dualizing the derivation of UniversalMorphismIntoEqualizer by UniversalMorphismIntoEqualizer using the universality of the kernel representation of the equalizer", + [ + [ JointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ], + [ CokernelColift, 1 ], + [ IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, Y_1, morphisms_1, T_1, tau_1 ) + return PostCompose( cat_1, CokernelColift( cat_1, JointPairwiseDifferencesOfMorphismsFromCoproduct( cat_1, Y_1, morphisms_1 ), T_1, tau_1 ), IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct( cat_1, Y_1, morphisms_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromCoequalizer, + "dualizing the derivation of UniversalMorphismIntoEqualizer by UniversalMorphismIntoEqualizer using LiftAlongMonomorphism and EmbeddingOfEqualizer", + [ + [ ColiftAlongEpimorphism, 1 ], + [ ProjectionOntoCoequalizer, 1 ], + ], + + function ( cat_1, Y_1, morphisms_1, T_1, tau_1 ) + return ColiftAlongEpimorphism( cat_1, ProjectionOntoCoequalizer( cat_1, Y_1, morphisms_1 ), tau_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromCoequalizerWithGivenCoequalizer, + "dualizing the derivation of UniversalMorphismIntoEqualizerWithGivenEqualizer by UniversalMorphismIntoEqualizer using LiftAlongMonomorphism and EmbeddingOfEqualizer", + [ + [ ColiftAlongEpimorphism, 1 ], + [ ProjectionOntoCoequalizerWithGivenCoequalizer, 1 ], + ], + + function ( cat_1, Y_1, morphisms_1, T_1, tau_1, P_1 ) + return ColiftAlongEpimorphism( cat_1, ProjectionOntoCoequalizerWithGivenCoequalizer( cat_1, Y_1, morphisms_1, P_1 ), tau_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromCoproduct, + "dualizing the derivation of UniversalMorphismIntoDirectProduct by UniversalMorphismIntoDirectProduct using UniversalMorphismIntoDirectSum", + [ + [ UniversalMorphismFromDirectSum, 1 ], + [ IsomorphismFromCoproductToDirectSum, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, objects_1, T_1, tau_1 ) + return PostCompose( cat_1, UniversalMorphismFromDirectSum( cat_1, objects_1, T_1, tau_1 ), IsomorphismFromCoproductToDirectSum( cat_1, objects_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromDirectSum, + "dualizing the derivation of UniversalMorphismIntoDirectSum by UniversalMorphismIntoDirectSum using the injections of the direct sum", + [ + [ PostCompose, 2 ], + [ ProjectionInFactorOfDirectSum, 2 ], + [ SumOfMorphisms, 1 ], + [ DirectSum, 1 ], + ], + + function ( cat_1, objects_1, T_1, tau_1 ) + return SumOfMorphisms( cat_1, DirectSum( cat_1, objects_1 ), List( [ 1 .. Length( tau_1 ) ], function ( i_2 ) + return PostCompose( cat_1, tau_1[i_2], ProjectionInFactorOfDirectSum( cat_1, objects_1, i_2 ) ); + end ), T_1 ); +end : CategoryFilter := IsAdditiveCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromDirectSum, + "dualizing the derivation of UniversalMorphismIntoDirectSum by UniversalMorphismIntoDirectSum using UniversalMorphismIntoDirectProduct", + [ + [ UniversalMorphismFromCoproduct, 1 ], + [ IsomorphismFromDirectSumToCoproduct, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, objects_1, T_1, tau_1 ) + return PostCompose( cat_1, UniversalMorphismFromCoproduct( cat_1, objects_1, T_1, tau_1 ), IsomorphismFromDirectSumToCoproduct( cat_1, objects_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromDirectSumWithGivenDirectSum, + "dualizing the derivation of UniversalMorphismIntoDirectSumWithGivenDirectSum by UniversalMorphismIntoDirectSum using the injections of the direct sum", + [ + [ PostCompose, 2 ], + [ ProjectionInFactorOfDirectSumWithGivenDirectSum, 2 ], + [ SumOfMorphisms, 1 ], + ], + + function ( cat_1, objects_1, T_1, tau_1, P_1 ) + return SumOfMorphisms( cat_1, P_1, List( [ 1 .. Length( tau_1 ) ], function ( i_2 ) + return PostCompose( cat_1, tau_1[i_2], ProjectionInFactorOfDirectSumWithGivenDirectSum( cat_1, objects_1, i_2, P_1 ) ); + end ), T_1 ); +end : CategoryFilter := IsAdditiveCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromImage, + "dualizing the derivation of UniversalMorphismIntoCoimage by UniversalMorphismIntoCoimage using UniversalMorphismFromImage and CanonicalIdentificationFromImageObjectToCoimage", + [ + [ UniversalMorphismIntoCoimage, 1 ], + [ CanonicalIdentificationFromCoimageToImageObject, 1 ], + [ InverseForMorphisms, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, alpha_1, tau_1 ) + return PostCompose( cat_1, InverseForMorphisms( cat_1, UniversalMorphismIntoCoimage( cat_1, alpha_1, NTuple( 2, tau_1[1], tau_1[2] ) ) ), CanonicalIdentificationFromCoimageToImageObject( cat_1, alpha_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromInitialObject, + "dualizing the derivation of UniversalMorphismIntoTerminalObject by UniversalMorphismIntoTerminalObject computing the zero morphism", + [ + [ InitialObject, 1 ], + [ ZeroMorphism, 1 ], + ], + + function ( cat_1, T_1 ) + return ZeroMorphism( cat_1, InitialObject( cat_1 ), T_1 ); +end : CategoryFilter := IsAdditiveCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromInitialObject, + "dualizing the derivation of UniversalMorphismIntoTerminalObject by UniversalMorphismFromInitialObject using UniversalMorphismFromZeroObject", + [ + [ UniversalMorphismFromZeroObject, 1 ], + [ IsomorphismFromInitialObjectToZeroObject, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, T_1 ) + return PostCompose( cat_1, UniversalMorphismFromZeroObject( cat_1, T_1 ), IsomorphismFromInitialObjectToZeroObject( cat_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromInitialObjectWithGivenInitialObject, + "dualizing the derivation of UniversalMorphismIntoTerminalObjectWithGivenTerminalObject by UniversalMorphismIntoTerminalObject computing the zero morphism", + [ + [ ZeroMorphism, 1 ], + ], + + function ( cat_1, T_1, P_1 ) + return ZeroMorphism( cat_1, P_1, T_1 ); +end : CategoryFilter := IsAdditiveCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromPushout, + "dualizing the derivation of UniversalMorphismIntoFiberProduct by UniversalMorphismIntoFiberProduct as the universal morphism into equalizer of a univeral morphism into direct product", + [ + [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ], + [ PostCompose, 3 ], + [ UniversalMorphismFromCoproduct, 1 ], + [ UniversalMorphismFromCoequalizer, 1 ], + [ Coproduct, 1 ], + [ IsomorphismFromPushoutToCoequalizerOfCoproductDiagram, 1 ], + ], + + function ( cat_1, morphisms_1, T_1, tau_1 ) + local deduped_3_1, deduped_4_1; + deduped_4_1 := List( morphisms_1, Range ); + deduped_3_1 := Coproduct( cat_1, deduped_4_1 ); + return PostCompose( cat_1, UniversalMorphismFromCoequalizer( cat_1, deduped_3_1, List( [ 1 .. Length( morphisms_1 ) ], function ( i_2 ) + return PostCompose( cat_1, InjectionOfCofactorOfCoproductWithGivenCoproduct( cat_1, deduped_4_1, i_2, deduped_3_1 ), morphisms_1[i_2] ); + end ), T_1, UniversalMorphismFromCoproduct( cat_1, deduped_4_1, T_1, tau_1 ) ), IsomorphismFromPushoutToCoequalizerOfCoproductDiagram( cat_1, morphisms_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromZeroObject, + "dualizing the derivation of UniversalMorphismIntoZeroObject by UniversalMorphismIntoZeroObject computing the zero morphism", + [ + [ ZeroObject, 1 ], + [ ZeroMorphism, 1 ], + ], + + function ( cat_1, T_1 ) + return ZeroMorphism( cat_1, ZeroObject( cat_1 ), T_1 ); +end : CategoryFilter := IsAdditiveCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromZeroObject, + "dualizing the derivation of UniversalMorphismIntoZeroObject by UniversalMorphismIntoZeroObject using UniversalMorphismIntoTerminalObject", + [ + [ UniversalMorphismFromInitialObject, 1 ], + [ IsomorphismFromZeroObjectToInitialObject, 1 ], + [ PostCompose, 1 ], + ], + + function ( cat_1, T_1 ) + return PostCompose( cat_1, UniversalMorphismFromInitialObject( cat_1, T_1 ), IsomorphismFromZeroObjectToInitialObject( cat_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismFromZeroObjectWithGivenZeroObject, + "dualizing the derivation of UniversalMorphismIntoZeroObjectWithGivenZeroObject by UniversalMorphismIntoZeroObject computing the zero morphism", + [ + [ ZeroMorphism, 1 ], + ], + + function ( cat_1, T_1, P_1 ) + return ZeroMorphism( cat_1, P_1, T_1 ); +end : CategoryFilter := IsAdditiveCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismIntoCoimage, + "dualizing the derivation of UniversalMorphismFromImage by UniversalMorphismFromImage using ImageEmbedding and LiftAlongMonomorphism", + [ + [ CoimageProjection, 1 ], + [ ColiftAlongEpimorphism, 1 ], + ], + + function ( cat_1, alpha_1, tau_1 ) + return ColiftAlongEpimorphism( cat_1, tau_1[1], CoimageProjection( cat_1, alpha_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( UniversalMorphismIntoCoimageWithGivenCoimageObject, + "dualizing the derivation of UniversalMorphismFromImageWithGivenImageObject by UniversalMorphismFromImageWithGivenImageObject using ImageEmbeddingWithGivenImageObject and LiftAlongMonomorphism", + [ + [ CoimageProjectionWithGivenCoimageObject, 1 ], + [ ColiftAlongEpimorphism, 1 ], + ], + + function ( cat_1, alpha_1, tau_1, C_1 ) + return ColiftAlongEpimorphism( cat_1, tau_1[1], CoimageProjectionWithGivenCoimageObject( cat_1, alpha_1, C_1 ) ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( ZeroMorphism, + "dualizing the derivation of ZeroMorphism by Zero morphism by composition of morphism into and from zero object", + [ + [ PostCompose, 1 ], + [ UniversalMorphismFromZeroObject, 1 ], + [ UniversalMorphismIntoZeroObject, 1 ], + ], + + function ( cat_1, a_1, b_1 ) + return PostCompose( cat_1, UniversalMorphismFromZeroObject( cat_1, b_1 ), UniversalMorphismIntoZeroObject( cat_1, a_1 ) ); +end : CategoryFilter := IsAdditiveCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); + +## +AddDerivationToCAP( ZeroObjectFunctorialWithGivenZeroObjects, + "dualizing the derivation of ZeroObjectFunctorialWithGivenZeroObjects by ZeroObjectFunctorialWithGivenZeroObjects using the universality of the limit", + [ + [ UniversalMorphismFromZeroObjectWithGivenZeroObject, 1 ], + ], + + function ( cat_1, P_1, Pp_1 ) + return UniversalMorphismFromZeroObjectWithGivenZeroObject( cat_1, Pp_1, P_1 ); +end : CategoryFilter := IsCapCategory, + Weight := 1, + is_autogenerated_by_CompilerForCAP := true ); diff --git a/CAP/gap/DerivedMethods.gi b/CAP/gap/DerivedMethods.gi index 68a895e8f6..203b304a1e 100644 --- a/CAP/gap/DerivedMethods.gi +++ b/CAP/gap/DerivedMethods.gi @@ -21,17 +21,6 @@ AddDerivationToCAP( IsLiftable, end : CategoryFilter := IsTerminalCategory ); -AddDerivationToCAP( IsColiftable, - "Two morphisms with equal sources are mutually coliftable in a terminal category", - [ ], - - function( cat, morphism1, morphism2 ) - - ## equality of sources is part of the specification of the input and checked by the pre-function - return true; - -end : CategoryFilter := IsTerminalCategory ); - ########################### ## ## WithGiven pairs @@ -76,45 +65,6 @@ AddDerivationToCAP( KernelLiftWithGivenKernelObject, end ); -## -AddDerivationToCAP( MorphismFromSourceToCokernelObject, - "MorphismFromSourceToCokernelObject as zero morphism from source to cokernel object", - [ [ CokernelObject, 1 ], - [ ZeroMorphism, 1 ] ], - - function( cat, alpha ) - local C; - - C := CokernelObject( cat, alpha ); - - return ZeroMorphism( cat, Source( alpha ), C ); - - end ); - -## -AddDerivationToCAP( CokernelColift, - "CokernelColift using ColiftAlongEpimorphism and CokernelProjection", - [ [ ColiftAlongEpimorphism, 1 ], - [ CokernelProjection, 1 ] ], - - function( cat, mor, test_object, test_morphism ) - - return ColiftAlongEpimorphism( cat, CokernelProjection( cat, mor ), test_morphism ); - - end ); - -## -AddDerivationToCAP( CokernelColiftWithGivenCokernelObject, - "CokernelColift using ColiftAlongEpimorphism and CokernelProjection", - [ [ ColiftAlongEpimorphism, 1 ], - [ CokernelProjectionWithGivenCokernelObject, 1 ] ], - - function( cat, mor, test_object, test_morphism, cokernel ) - - return ColiftAlongEpimorphism( cat, CokernelProjectionWithGivenCokernelObject( cat, mor, cokernel ), test_morphism ); - -end ); - ## AddDerivationToCAP( UniversalMorphismIntoDirectSum, "UniversalMorphismIntoDirectSum using the injections of the direct sum", @@ -156,47 +106,6 @@ AddDerivationToCAP( UniversalMorphismIntoDirectSumWithGivenDirectSum, end : CategoryFilter := IsAdditiveCategory ); -## -AddDerivationToCAP( UniversalMorphismFromDirectSum, - "UniversalMorphismFromDirectSum using projections of the direct sum", - [ [ PreCompose, 2 ], - [ ProjectionInFactorOfDirectSum, 2 ], - [ SumOfMorphisms, 1 ], - [ DirectSum, 1 ] ], - - function( cat, diagram, test_object, sink ) - local nr_components; - - nr_components := Length( sink ); - - return SumOfMorphisms( cat, - DirectSum( cat, diagram ), - List( [ 1 .. nr_components ], i -> PreCompose( cat, ProjectionInFactorOfDirectSum( cat, diagram, i ), sink[ i ] ) ), - test_object - ); - - end : CategoryFilter := IsAdditiveCategory ); - -## -AddDerivationToCAP( UniversalMorphismFromDirectSumWithGivenDirectSum, - "UniversalMorphismFromDirectSum using projections of the direct sum", - [ [ PreCompose, 2 ], - [ ProjectionInFactorOfDirectSumWithGivenDirectSum, 2 ], - [ SumOfMorphisms, 1 ] ], - - function( cat, diagram, test_object, sink, direct_sum ) - local nr_components; - - nr_components := Length( sink ); - - return SumOfMorphisms( cat, - direct_sum, - List( [ 1 .. nr_components ], i -> PreCompose( cat, ProjectionInFactorOfDirectSumWithGivenDirectSum( cat, diagram, i, direct_sum ), sink[ i ] ) ), - test_object - ); - -end : CategoryFilter := IsAdditiveCategory ); - ## AddDerivationToCAP( ProjectionInFactorOfDirectSum, "ProjectionInFactorOfDirectSum using UniversalMorphismFromDirectSum", @@ -257,66 +166,6 @@ AddDerivationToCAP( ProjectionInFactorOfDirectSumWithGivenDirectSum, end ); -## -AddDerivationToCAP( InjectionOfCofactorOfDirectSum, - "InjectionOfCofactorOfDirectSum using UniversalMorphismIntoDirectSum", - [ [ IdentityMorphism, 1 ], - [ ZeroMorphism, 2 ], - [ UniversalMorphismIntoDirectSum, 1 ] ], - - function( cat, list, injection_number ) - local id, morphisms; - - id := IdentityMorphism( cat, list[injection_number] ); - - morphisms := List( [ 1 .. Length( list ) ], function( i ) - - if i = injection_number then - - return id; - - else - - return ZeroMorphism( cat, list[injection_number], list[i] ); - - fi; - - end ); - - return UniversalMorphismIntoDirectSum( cat, list, list[injection_number], morphisms ); - - end ); - -## -AddDerivationToCAP( InjectionOfCofactorOfDirectSumWithGivenDirectSum, - "InjectionOfCofactorOfDirectSum using UniversalMorphismIntoDirectSum", - [ [ IdentityMorphism, 1 ], - [ ZeroMorphism, 2 ], - [ UniversalMorphismIntoDirectSumWithGivenDirectSum, 1 ] ], - - function( cat, list, injection_number, direct_sum_object ) - local id, morphisms; - - id := IdentityMorphism( cat, list[injection_number] ); - - morphisms := List( [ 1 .. Length( list ) ], function( i ) - - if i = injection_number then - - return id; - - else - - return ZeroMorphism( cat, list[injection_number], list[i] ); - - fi; - - end ); - - return UniversalMorphismIntoDirectSumWithGivenDirectSum( cat, list, list[injection_number], morphisms, direct_sum_object ); - -end ); - ## AddDerivationToCAP( UniversalMorphismIntoTerminalObject, "UniversalMorphismIntoTerminalObject computing the zero morphism", @@ -343,58 +192,6 @@ AddDerivationToCAP( UniversalMorphismIntoTerminalObjectWithGivenTerminalObject, end : CategoryFilter := IsAdditiveCategory ); -## -AddDerivationToCAP( UniversalMorphismFromInitialObject, - "UniversalMorphismFromInitialObject computing the zero morphism", - [ [ InitialObject, 1 ], - [ ZeroMorphism, 1 ] ], - - function( cat, test_sink ) - local initial_object; - - initial_object := InitialObject( cat ); - - return ZeroMorphism( cat, initial_object, test_sink ); - - end : CategoryFilter := IsAdditiveCategory ); - -## -AddDerivationToCAP( UniversalMorphismFromInitialObjectWithGivenInitialObject, - "UniversalMorphismFromInitialObject computing the zero morphism", - [ [ ZeroMorphism, 1 ] ], - - function( cat, test_sink, initial_object ) - - return ZeroMorphism( cat, initial_object, test_sink ); - -end : CategoryFilter := IsAdditiveCategory ); - -## -AddDerivationToCAP( UniversalMorphismFromZeroObject, - "UniversalMorphismFromZeroObject computing the zero morphism", - [ [ ZeroObject, 1 ], - [ ZeroMorphism, 1 ] ], - - function( cat, test_sink ) - local zero_object; - - zero_object := ZeroObject( cat ); - - return ZeroMorphism( cat, zero_object, test_sink ); - - end : CategoryFilter := IsAdditiveCategory ); - -## -AddDerivationToCAP( UniversalMorphismFromZeroObjectWithGivenZeroObject, - "UniversalMorphismFromZeroObject computing the zero morphism", - [ [ ZeroMorphism, 1 ] ], - - function( cat, test_sink, zero_object ) - - return ZeroMorphism( cat, zero_object, test_sink ); - -end : CategoryFilter := IsAdditiveCategory ); - ## AddDerivationToCAP( UniversalMorphismIntoZeroObject, "UniversalMorphismIntoZeroObject computing the zero morphism", @@ -501,100 +298,6 @@ AddDerivationToCAP( MorphismFromFiberProductToSink, end ); -## Pushout from Coproduct and Coequalizer - -## -AddDerivationToCAP( Pushout, - "Pushout as the range of IsomorphismFromCoequalizerOfCoproductDiagramToPushout", - [ [ IsomorphismFromCoequalizerOfCoproductDiagramToPushout, 1 ] ], - - function( cat, diagram ) - - return Range( IsomorphismFromCoequalizerOfCoproductDiagramToPushout( cat, diagram ) ); - -end ); - -## -AddDerivationToCAP( InjectionOfCofactorOfPushout, - "InjectionOfCofactorOfPushout by composing the coproduct injection with the projection onto coequalizer", - [ [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ], - [ PreCompose, 3 ], - [ Coproduct, 1 ], - [ ProjectionOntoCoequalizer, 1 ], - [ ComponentOfMorphismFromCoproduct, 1 ], - [ IsomorphismFromCoequalizerOfCoproductDiagramToPushout, 1 ] ], - - function( cat, diagram, injection_number ) - local D, coproduct, diagram_of_coequalizer, pi; - - D := List( diagram, Range ); - - coproduct := Coproduct( cat, D ); - - diagram_of_coequalizer := List( [ 1 .. Length( D ) ], i -> PreCompose( cat, diagram[i], InjectionOfCofactorOfCoproductWithGivenCoproduct( cat, D, i, coproduct ) ) ); - - pi := ProjectionOntoCoequalizer( cat, coproduct, diagram_of_coequalizer ); - - return PreCompose( cat, ComponentOfMorphismFromCoproduct( cat, pi, D, injection_number ), IsomorphismFromCoequalizerOfCoproductDiagramToPushout( cat, diagram ) ); - - end ); - -## -AddDerivationToCAP( UniversalMorphismFromPushout, - "UniversalMorphismFromPushout as the universal morphism from coequalizer of a univeral morphism from coproduct", - [ [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ], - [ PreCompose, 3 ], - [ UniversalMorphismFromCoproduct, 1 ], - [ UniversalMorphismFromCoequalizer, 1 ], - [ Coproduct, 1 ], - [ IsomorphismFromPushoutToCoequalizerOfCoproductDiagram, 1 ] ], - - function( cat, diagram, test_object, tau ) - local D, coproduct, diagram_of_coequalizer, chi, psi; - - D := List( diagram, Range ); - - coproduct := Coproduct( cat, D ); - - diagram_of_coequalizer := List( [ 1 .. Length( D ) ], i -> PreCompose( cat, diagram[i], InjectionOfCofactorOfCoproductWithGivenCoproduct( cat, D, i, coproduct ) ) ); - - chi := UniversalMorphismFromCoproduct( cat, D, test_object, tau ); - - psi := UniversalMorphismFromCoequalizer( cat, coproduct, diagram_of_coequalizer, test_object, chi ); - - return PreCompose( cat, IsomorphismFromPushoutToCoequalizerOfCoproductDiagram( cat, diagram ), psi ); - - end ); - -## -AddDerivationToCAP( MorphismFromSourceToPushout, - "MorphismFromSourceToPushout by composing the first morphism in the diagram with the first injection", - [ [ InjectionOfCofactorOfPushout, 1 ], - [ PreCompose, 1 ] ], - - function( cat, diagram ) - local iota_1; - - iota_1 := InjectionOfCofactorOfPushout( cat, diagram, 1 ); - - return PreCompose( cat, diagram[1], iota_1 ); - - end ); - -## -AddDerivationToCAP( UniversalMorphismFromZeroObject, - "UniversalMorphismFromZeroObject using UniversalMorphismFromInitialObject", - [ [ IsomorphismFromZeroObjectToInitialObject, 1 ], - [ UniversalMorphismFromInitialObject, 1 ], - [ PreCompose, 1 ] ], - - function( cat, obj ) - - return PreCompose( cat, IsomorphismFromZeroObjectToInitialObject( cat ), - UniversalMorphismFromInitialObject( cat, obj ) ); - - end ); - ## AddDerivationToCAP( UniversalMorphismIntoZeroObject, "UniversalMorphismIntoZeroObject using UniversalMorphismIntoTerminalObject", @@ -652,49 +355,6 @@ AddDerivationToCAP( ComponentOfMorphismIntoDirectSum, end ); -## -AddDerivationToCAP( InjectionOfCofactorOfDirectSum, - "InjectionOfCofactorOfDirectSum using InjectionOfCofactorOfCoproduct", - [ [ InjectionOfCofactorOfCoproduct, 1 ], - [ IsomorphismFromCoproductToDirectSum, 1 ], - [ PreCompose, 1 ] ], - - function( cat, diagram, injection_number ) - - return PreCompose( cat, InjectionOfCofactorOfCoproduct( cat, diagram, injection_number ), - IsomorphismFromCoproductToDirectSum( cat, diagram ) ); - end ); - -## -AddDerivationToCAP( UniversalMorphismFromDirectSum, - "UniversalMorphismFromDirectSum using UniversalMorphismFromCoproduct", - [ [ IsomorphismFromDirectSumToCoproduct, 1 ], - [ UniversalMorphismFromCoproduct, 1 ], - [ PreCompose, 1 ] ], - - function( cat, diagram, test_object, sink ) - - return PreCompose( cat, IsomorphismFromDirectSumToCoproduct( cat, diagram ), - UniversalMorphismFromCoproduct( cat, diagram, test_object, sink ) ); - end ); - -## -AddDerivationToCAP( ComponentOfMorphismFromDirectSum, - "ComponentOfMorphismFromDirectSum using ComponentOfMorphismFromCoproduct", - [ [ IsomorphismFromCoproductToDirectSum, 1 ], - [ ComponentOfMorphismFromCoproduct, 1 ], - [ PreCompose, 1 ] ], - - function( cat, alpha, summands, nr ) - - return ComponentOfMorphismFromCoproduct( cat, - PreCompose( cat, IsomorphismFromCoproductToDirectSum( cat, summands ), alpha ), - summands, - nr - ); - - end ); - ## AddDerivationToCAP( UniversalMorphismIntoTerminalObject, "UniversalMorphismFromInitialObject using UniversalMorphismFromZeroObject", @@ -709,20 +369,6 @@ AddDerivationToCAP( UniversalMorphismIntoTerminalObject, end ); -## -AddDerivationToCAP( UniversalMorphismFromInitialObject, - "UniversalMorphismFromInitialObject using UniversalMorphismFromZeroObject", - [ [ IsomorphismFromInitialObjectToZeroObject, 1 ], - [ UniversalMorphismFromZeroObject, 1 ], - [ PreCompose, 1 ] ], - - function( cat, obj ) - - return PreCompose( cat, IsomorphismFromInitialObjectToZeroObject( cat ), - UniversalMorphismFromZeroObject( cat, obj ) ); - - end ); - ## AddDerivationToCAP( ProjectionInFactorOfDirectProduct, "ProjectionInFactorOfDirectProduct using ProjectionInFactorOfDirectSum", @@ -767,49 +413,6 @@ AddDerivationToCAP( ComponentOfMorphismIntoDirectProduct, end ); -## -AddDerivationToCAP( InjectionOfCofactorOfCoproduct, - "InjectionOfCofactorOfCoproduct using InjectionOfCofactorOfDirectSum", - [ [ InjectionOfCofactorOfDirectSum, 1 ], - [ IsomorphismFromDirectSumToCoproduct, 1 ], - [ PreCompose, 1 ] ], - - function( cat, diagram, injection_number ) - - return PreCompose( cat, InjectionOfCofactorOfDirectSum( cat, diagram, injection_number ), - IsomorphismFromDirectSumToCoproduct( cat, diagram ) ); - end ); - -## -AddDerivationToCAP( UniversalMorphismFromCoproduct, - "UniversalMorphismFromCoproduct using UniversalMorphismFromDirectSum", - [ [ IsomorphismFromCoproductToDirectSum, 1 ], - [ UniversalMorphismFromDirectSum, 1 ], - [ PreCompose, 1 ] ], - - function( cat, diagram, test_object, sink ) - - return PreCompose( cat, IsomorphismFromCoproductToDirectSum( cat, diagram ), - UniversalMorphismFromDirectSum( cat, diagram, test_object, sink ) ); - end ); - -## -AddDerivationToCAP( ComponentOfMorphismFromCoproduct, - "ComponentOfMorphismFromCoproduct using ComponentOfMorphismFromDirectSum", - [ [ IsomorphismFromDirectSumToCoproduct, 1 ], - [ ComponentOfMorphismFromDirectSum, 1 ], - [ PreCompose, 1 ] ], - - function( cat, alpha, cofactors, nr ) - - return ComponentOfMorphismFromDirectSum( cat, - PreCompose( cat, IsomorphismFromDirectSumToCoproduct( cat, cofactors ), alpha ), - cofactors, - nr - ); - - end ); - ## AddDerivationToCAP( UniversalMorphismIntoEqualizer, "UniversalMorphismIntoEqualizer using the universality of the kernel representation of the equalizer", @@ -832,28 +435,6 @@ AddDerivationToCAP( UniversalMorphismIntoEqualizer, end ); -## -AddDerivationToCAP( UniversalMorphismFromCoequalizer, - "UniversalMorphismFromCoequalizer using the universality of the cokernel representation of the coequalizer", - [ [ JointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ], - [ CokernelColift, 1 ], - [ IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ], - [ PreCompose, 1 ] ], - - function( cat, A, diagram, test_object, tau ) - local joint_pairwise_differences, cokernel_colift; - - joint_pairwise_differences := JointPairwiseDifferencesOfMorphismsFromCoproduct( cat, A, diagram ); - - cokernel_colift := CokernelColift( cat, joint_pairwise_differences, test_object, tau ); - - return PreCompose( cat, - IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct( cat, A, diagram ), - cokernel_colift - ); - - end ); - ## AddDerivationToCAP( ImageEmbedding, "ImageEmbedding as the kernel embedding of the cokernel projection", @@ -872,24 +453,6 @@ AddDerivationToCAP( ImageEmbedding, end : CategoryFilter := IsAbelianCategory ); ##FIXME: PreAbelian? -## -AddDerivationToCAP( CoimageProjection, - "CoimageProjection as the cokernel projection of the kernel embedding", - [ [ KernelEmbedding, 1 ], - [ CokernelProjection, 1 ], - [ IsomorphismFromCokernelOfKernelToCoimage, 1 ], - [ PreCompose, 1 ] ], - - function( cat, mor ) - local coimage_projection; - - coimage_projection := CokernelProjection( cat, KernelEmbedding( cat, mor ) ); - - return PreCompose( cat, coimage_projection, - IsomorphismFromCokernelOfKernelToCoimage( cat, mor ) ); - -end : CategoryFilter := IsAbelianCategory ); ##FIXME: PreAbelian? - ## AddDerivationToCAP( CoimageProjection, "CoimageProjection as the coastriction to image", @@ -933,37 +496,7 @@ AddDerivationToCAP( CoastrictionToImageWithGivenImageObject, image_embedding := ImageEmbeddingWithGivenImageObject( cat, morphism, image ); return LiftAlongMonomorphism( cat, image_embedding, morphism ); - -end ); - -## -AddDerivationToCAP( AstrictionToCoimage, - "AstrictionToCoimage using that coimage projection can be seen as a cokernel", - [ [ CoimageProjection, 1 ], - [ ColiftAlongEpimorphism, 1 ] ], - - function( cat, morphism ) - local coimage_projection; - - coimage_projection := CoimageProjection( cat, morphism ); - - return ColiftAlongEpimorphism( cat, coimage_projection, morphism ); - - end ); - -## -AddDerivationToCAP( AstrictionToCoimageWithGivenCoimageObject, - "AstrictionToCoimage using that coimage projection can be seen as a cokernel", - [ [ CoimageProjectionWithGivenCoimageObject, 1 ], - [ ColiftAlongEpimorphism, 1 ] ], - - function( cat, morphism, coimage ) - local coimage_projection; - - coimage_projection := CoimageProjectionWithGivenCoimageObject( cat, morphism, coimage ); - - return ColiftAlongEpimorphism( cat, coimage_projection, morphism ); - + end ); ## @@ -1028,36 +561,6 @@ AddDerivationToCAP( UniversalMorphismFromImageWithGivenImageObject, end ); -## -AddDerivationToCAP( UniversalMorphismIntoCoimage, - "UniversalMorphismIntoCoimage using CoimageProjection and ColiftAlongEpimorphism", - [ [ CoimageProjection, 1 ], - [ ColiftAlongEpimorphism, 1 ] ], - - function( cat, morphism, test_factorization ) - local coimage_projection; - - coimage_projection := CoimageProjection( cat, morphism ); - - return ColiftAlongEpimorphism( cat, test_factorization[1], coimage_projection ); - - end ); - -## -AddDerivationToCAP( UniversalMorphismIntoCoimageWithGivenCoimageObject, - "UniversalMorphismIntoCoimageWithGivenCoimageObject using CoimageProjectionWithGivenCoimageObject and ColiftAlongEpimorphism", - [ [ CoimageProjectionWithGivenCoimageObject, 1 ], - [ ColiftAlongEpimorphism, 1 ] ], - - function( cat, morphism, test_factorization, coimage ) - local coimage_projection; - - coimage_projection := CoimageProjectionWithGivenCoimageObject( cat, morphism, coimage ); - - return ColiftAlongEpimorphism( cat, test_factorization[1], coimage_projection ); - -end ); - ## AddDerivationToCAP( UniversalMorphismIntoCoimage, "UniversalMorphismIntoCoimage using UniversalMorphismFromImage and CanonicalIdentificationFromImageObjectToCoimage", @@ -1114,45 +617,6 @@ AddDerivationToCAP( MorphismFromEqualizerToSink, end ); -## -AddDerivationToCAP( UniversalMorphismFromCoequalizer, - "UniversalMorphismFromCoequalizer using ColiftAlongEpimorphism and ProjectionOntoCoequalizer", - [ [ ColiftAlongEpimorphism, 1 ], - [ ProjectionOntoCoequalizer, 1 ] ], - - function( cat, A, diagram, test_object, test_morphism ) - - return ColiftAlongEpimorphism( cat, ProjectionOntoCoequalizer( cat, A, diagram ), test_morphism ); - - end ); - -## -AddDerivationToCAP( UniversalMorphismFromCoequalizerWithGivenCoequalizer, - "UniversalMorphismFromCoequalizer using ColiftAlongEpimorphism and ProjectionOntoCoequalizer", - [ [ ColiftAlongEpimorphism, 1 ], - [ ProjectionOntoCoequalizerWithGivenCoequalizer, 1 ] ], - - function( cat, A, diagram, test_object, test_morphism, coequalizer ) - - return ColiftAlongEpimorphism( cat, ProjectionOntoCoequalizerWithGivenCoequalizer( cat, A, diagram, coequalizer ), test_morphism ); - -end ); - -## -AddDerivationToCAP( MorphismFromSourceToCoequalizer, - "MorphismFromSourceToCoequalizer by composing the first morphism in the diagram with the projection", - [ [ ProjectionOntoCoequalizer, 1 ], - [ PreCompose, 1 ] ], - - function( cat, A, diagram ) - local pi; - - pi := ProjectionOntoCoequalizer( cat, A, diagram ); - - return PreCompose( cat, diagram[1], pi ); - - end ); - ## AddDerivationToCAP( ImageObjectFunctorialWithGivenImageObjects, "ImageObjectFunctorialWithGivenImageObjects using the universality", @@ -1168,21 +632,6 @@ AddDerivationToCAP( ImageObjectFunctorialWithGivenImageObjects, end ); -## -AddDerivationToCAP( CoimageObjectFunctorialWithGivenCoimageObjects, - "CoimageObjectFunctorialWithGivenCoimageObjects using the universality", - [ [ ColiftAlongEpimorphism, 1 ], - [ CoimageProjectionWithGivenCoimageObject, 2 ], - [ PreCompose, 1 ] ], - - function( cat, C, alpha, mu, alphap, Cp ) - - return ColiftAlongEpimorphism( cat, - CoimageProjectionWithGivenCoimageObject( cat, alpha, C ), - PreCompose( cat, mu, CoimageProjectionWithGivenCoimageObject( cat, alphap, Cp ) ) ); - -end ); - ## AddDerivationToCAP( ProjectiveCoverObject, "ProjectiveCoverObject as the source of EpimorphismFromProjectiveCoverObject", @@ -1194,17 +643,6 @@ AddDerivationToCAP( ProjectiveCoverObject, end ); -## -AddDerivationToCAP( InjectiveEnvelopeObject, - "InjectiveEnvelopeObject as the range of MonomorphismIntoInjectiveEnvelopeObject", - [ [ MonomorphismIntoInjectiveEnvelopeObject, 1 ] ], - - function( cat, obj ) - - return Range( MonomorphismIntoInjectiveEnvelopeObject( cat, obj ) ); - -end ); - ########################### ## ## Methods returning a boolean @@ -1257,18 +695,6 @@ AddDerivationToCAP( IsProjective, end ); -## -AddDerivationToCAP( IsInjective, - "IsInjective by checking if the object is a retract of some injective object", - [ [ MonomorphismIntoSomeInjectiveObject, 1 ], - [ IsSplitMonomorphism, 1 ] ], - - function( cat, object ) - - return IsSplitMonomorphism( cat, MonomorphismIntoSomeInjectiveObject( cat, object ) ); - -end ); - ## AddDerivationToCAP( IsOne, "IsOne by comparing with the identity morphism", @@ -1382,29 +808,6 @@ AddDerivationToCAP( IsTerminal, end ); -## -AddDerivationToCAP( IsInitial, - "IsInitial using IsZeroForObjects", - [ [ IsZeroForObjects, 1 ] ], - - function( cat, object ) - - return IsZeroForObjects( cat, object ); - -end : CategoryFilter := IsAdditiveCategory ); #Ab-Category? - -## -AddDerivationToCAP( IsInitial, - "IsInitial using IsIsomorphism( cat, UniversalMorphismFromInitialObject )", - [ [ IsIsomorphism, 1 ], - [ UniversalMorphismFromInitialObject, 1 ] ], - - function( cat, object ) - - return IsIsomorphism( cat, UniversalMorphismFromInitialObject( cat, object ) ); - -end ); - ## AddDerivationToCAP( IsEqualForMorphismsOnMor, "IsEqualForMorphismsOnMor using IsEqualForMorphisms", @@ -1474,38 +877,6 @@ AddDerivationToCAP( IsMonomorphism, end ); -## -AddDerivationToCAP( IsEpimorphism, - "IsEpimorphism by deciding if the cokernel is a zero object", - [ [ IsZeroForObjects, 1 ], - [ CokernelObject, 1 ] ], - - function( cat, morphism ) - - return IsZeroForObjects( cat, CokernelObject( cat, morphism ) ); - -end : CategoryFilter := IsAdditiveCategory ); - -## -AddDerivationToCAP( IsEpimorphism, - "IsEpimorphism by deciding if the codiagonal morphism is an isomorphism", - [ [ IdentityMorphism, 1 ], - [ UniversalMorphismFromPushout, 1 ], - [ IsIsomorphism, 1 ] ], - - function( cat, morphism ) - local pushout_diagram, identity, codiagonal_morphism; - - pushout_diagram := [ morphism, morphism ]; - - identity := IdentityMorphism( cat, Range( morphism ) ); - - codiagonal_morphism := UniversalMorphismFromPushout( cat, pushout_diagram, Range( morphism ), [ identity, identity ] ); - - return IsIsomorphism( cat, codiagonal_morphism ); - -end ); - ## AddDerivationToCAP( IsIsomorphism, "IsIsomorphism by deciding if it is a mono and an epi", @@ -1542,30 +913,6 @@ AddDerivationToCAP( IsIsomorphism, end ); -## -AddDerivationToCAP( IsIsomorphism, - "IsIsomorphism by deciding if it is a mono and a split epi", - [ [ IsMonomorphism, 1 ], - [ IsSplitEpimorphism, 1 ] ], - - function( cat, morphism ) - - return IsMonomorphism( cat, morphism ) and IsSplitEpimorphism( cat, morphism ); - -end ); - -## -AddDerivationToCAP( IsSplitEpimorphism, - "IsSplitEpimorphism by using IsLiftable", - [ [ IsLiftable, 1 ], - [ IdentityMorphism, 1 ] ], - - function( cat, morphism ) - - return IsLiftable( cat, IdentityMorphism( cat, Range( morphism ) ), morphism ); - -end ); - ## AddDerivationToCAP( IsSplitMonomorphism, "IsSplitMonomorphism by using IsColiftable", @@ -1589,17 +936,6 @@ AddDerivationToCAP( IsEqualAsSubobjects, end ); -## -AddDerivationToCAP( IsEqualAsFactorobjects, - "IsEqualAsFactorobjects(factor1, factor2) if factor1 dominates factor2 and vice versa", - [ [ IsCodominating, 2 ] ], - - function( cat, factor1, factor2 ) - - return IsCodominating( cat, factor1, factor2 ) and IsCodominating( cat, factor2, factor1 ); - -end ); - ## AddDerivationToCAP( IsDominating, "IsDominating using IsLiftableAlongMonomorphism", @@ -1646,52 +982,6 @@ AddDerivationToCAP( IsDominating, end ); -## -AddDerivationToCAP( IsCodominating, - "IsCodominating using IsColiftableAlongEpimorphism", - [ [ IsColiftableAlongEpimorphism, 1 ] ], - - function( cat, factor1, factor2 ) - - return IsColiftableAlongEpimorphism( cat, factor2, factor1 ); - -end ); - -## -AddDerivationToCAP( IsCodominating, - "IsCodominating using IsDominating and duality by kernel", - [ [ KernelEmbedding, 2 ], - [ IsDominating, 1 ] ], - - function( cat, factor1, factor2 ) - local kernel_embedding_1, kernel_embedding_2; - - kernel_embedding_1 := KernelEmbedding( cat, factor1 ); - - kernel_embedding_2 := KernelEmbedding( cat, factor2 ); - - return IsDominating( cat, kernel_embedding_2, kernel_embedding_1 ); - -end ); - -## -AddDerivationToCAP( IsCodominating, - "IsCodominating(factor1, factor2) by deciding if KernelEmbedding(cat, factor2) composed with factor1 is zero", - [ [ KernelEmbedding, 1 ], - [ PreCompose, 1 ], - [ IsZeroForMorphisms, 1 ] ], - - function( cat, factor1, factor2 ) - local kernel_embedding, composition; - - kernel_embedding := KernelEmbedding( cat, factor2 ); - - composition := PreCompose( cat, kernel_embedding, factor1 ); - - return IsZeroForMorphisms( cat, composition ); - -end ); - ## AddDerivationToCAP( IsLiftableAlongMonomorphism, "IsLiftableAlongMonomorphism using IsLiftable", @@ -1703,17 +993,6 @@ AddDerivationToCAP( IsLiftableAlongMonomorphism, end ); -## -AddDerivationToCAP( IsColiftableAlongEpimorphism, - "IsColiftableAlongEpimorphism using IsColiftable", - [ [ IsColiftable, 1 ] ], - - function( cat, epsilon, tau ) - - return IsColiftable( cat, epsilon, tau ); - -end ); - ## AddDerivationToCAP( IsProjective, "", @@ -1726,18 +1005,6 @@ AddDerivationToCAP( IsProjective, end ); -## -AddDerivationToCAP( IsInjective, - "", - [ [ MonomorphismIntoInjectiveEnvelopeObject, 1 ], - [ IsIsomorphism, 1 ] ], - - function( cat, alpha ) - - return IsIsomorphism( cat, MonomorphismIntoInjectiveEnvelopeObject( cat, alpha ) ); - -end ); - ########################### ## ## Methods returning a morphism where the source and range can directly be read of from the input @@ -1779,17 +1046,6 @@ AddDerivationToCAP( ZeroMorphism, end : CategoryFilter := IsAbCategory ); -## -AddDerivationToCAP( PostCompose, - "PostCompose using PreCompose and swapping arguments", - [ [ PreCompose, 1 ] ], - - function( cat, post_mor, pre_mor ) - - return PreCompose( cat, pre_mor, post_mor ); - -end ); - ## AddDerivationToCAP( PreCompose, "PreCompose using PostCompose and swapping arguments", @@ -1829,34 +1085,6 @@ AddDerivationToCAP( PreComposeList, end ); -## -AddDerivationToCAP( PostCompose, - "PostCompose by wrapping the arguments in a list", - [ [ PostComposeList, 1 ] ], - - function( cat, post_mor, pre_mor ) - - return PostComposeList( cat, Source( pre_mor ), [ post_mor, pre_mor ], Range( post_mor ) ); - -end ); - -## -AddDerivationToCAP( PostComposeList, - "PostComposeList by iterating PostCompose", - [ [ IdentityMorphism, 2 ], - [ PostCompose, 2 ] ], - - function( cat, source, morphism_list, range ) - local id_source, id_range; - - id_source := IdentityMorphism( cat, source ); - - id_range := IdentityMorphism( cat, range ); - - return Iterated( morphism_list, { beta, alpha } -> PostCompose( cat, beta, alpha ), id_range, id_source ); - -end ); - ## AddDerivationToCAP( InverseForMorphisms, "InverseForMorphisms using LiftAlongMonomorphism of an identity morphism", @@ -1872,21 +1100,6 @@ AddDerivationToCAP( InverseForMorphisms, end ); -## -AddDerivationToCAP( InverseForMorphisms, - "InverseForMorphisms using ColiftAlongEpimorphism of an identity morphism", - [ [ IdentityMorphism, 1 ], - [ ColiftAlongEpimorphism, 1 ] ], - - function( cat, mor ) - local identity_of_source; - - identity_of_source := IdentityMorphism( cat, Source( mor ) ); - - return ColiftAlongEpimorphism( cat, mor, identity_of_source ); - -end ); - ## AddDerivationToCAP( PreInverseForMorphisms, "PreInverseForMorphisms using IdentityMorphism and Lift", @@ -1899,18 +1112,6 @@ AddDerivationToCAP( PreInverseForMorphisms, end ); -## -AddDerivationToCAP( PostInverseForMorphisms, - "PostInverseForMorphisms using IdentityMorphism and Colift", - [ [ IdentityMorphism, 1 ], - [ Colift, 1 ] ], - - function( cat, mor ) - - return Colift( cat, mor, IdentityMorphism( cat, Source( mor ) ) ); - -end ); - ## AddDerivationToCAP( AdditionForMorphisms, "AdditionForMorphisms using SumOfMorphisms", @@ -2010,29 +1211,6 @@ AddDerivationToCAP( ProjectiveLift, end ); - -## -AddDerivationToCAP( ColiftAlongEpimorphism, - "ColiftAlongEpimorphism using Colift", - [ [ Colift, 1 ] ], - - function( cat, alpha, beta ) - - return Colift( cat, alpha, beta ); - -end ); - -## -AddDerivationToCAP( InjectiveColift, - "InjectiveColift using Colift", - [ [ Colift, 1 ] ], - - function( cat, alpha, beta ) - - return Colift( cat, alpha, beta ); - -end ); - ## AddDerivationToCAP( RandomMorphismByInteger, "RandomMorphismByInteger using RandomObjectByInteger and RandomMorphismWithFixedSourceByInteger", @@ -2204,61 +1382,18 @@ AddDerivationToCAP( IsomorphismFromImageObjectToKernelOfCokernel, [ [ KernelEmbedding, 1 ], [ CokernelProjection, 1 ], [ LiftAlongMonomorphism, 1 ], - [ UniversalMorphismFromImage, 1 ] ], - - function( cat, morphism ) - local kernel_emb, morphism_to_kernel; - - kernel_emb := KernelEmbedding( cat, CokernelProjection( cat, morphism ) ); - - morphism_to_kernel := LiftAlongMonomorphism( cat, kernel_emb, morphism ); - - return UniversalMorphismFromImage( cat, morphism, [ morphism_to_kernel, kernel_emb ] ); - -end : CategoryFilter := IsAbelianCategory ); - -## -AddDerivationToCAP( IsomorphismFromCokernelOfKernelToCoimage, - "IsomorphismFromCokernelOfKernelToCoimage as the inverse of IsomorphismFromCoimageToCokernelOfKernel", - [ [ InverseForMorphisms, 1 ], - [ IsomorphismFromCoimageToCokernelOfKernel, 1 ] ], - - function( cat, morphism ) - - return InverseForMorphisms( cat, IsomorphismFromCoimageToCokernelOfKernel( cat, morphism ) ); - -end ); - -## -AddDerivationToCAP( IsomorphismFromCokernelOfKernelToCoimage, - "IsomorphismFromCokernelOfKernelToCoimage using the universal property of the coimage", - [ [ CokernelProjection, 1 ], - [ KernelEmbedding, 1 ], - [ ColiftAlongEpimorphism, 1 ], - [ UniversalMorphismIntoCoimage, 1 ] ], - - function( cat, morphism ) - local cokernel_proj, morphism_from_cokernel; - - cokernel_proj := CokernelProjection( cat, KernelEmbedding( cat, morphism ) ); - - morphism_from_cokernel := ColiftAlongEpimorphism( cat, cokernel_proj, morphism ); - - return UniversalMorphismIntoCoimage( cat, morphism, [ cokernel_proj, morphism_from_cokernel ] ); - -end : CategoryFilter := IsAbelianCategory ); - -## -AddDerivationToCAP( IsomorphismFromCoimageToCokernelOfKernel, - "IsomorphismFromCoimageToCokernelOfKernel as the inverse of IsomorphismFromCokernelOfKernelToCoimage", - [ [ InverseForMorphisms, 1 ], - [ IsomorphismFromCokernelOfKernelToCoimage, 1 ] ], + [ UniversalMorphismFromImage, 1 ] ], function( cat, morphism ) + local kernel_emb, morphism_to_kernel; - return InverseForMorphisms( cat, IsomorphismFromCokernelOfKernelToCoimage( cat, morphism ) ); + kernel_emb := KernelEmbedding( cat, CokernelProjection( cat, morphism ) ); -end ); + morphism_to_kernel := LiftAlongMonomorphism( cat, kernel_emb, morphism ); + + return UniversalMorphismFromImage( cat, morphism, [ morphism_to_kernel, kernel_emb ] ); + +end : CategoryFilter := IsAbelianCategory ); ## AddDerivationToCAP( IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct, @@ -2302,48 +1437,6 @@ AddDerivationToCAP( IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIn end ); -## -AddDerivationToCAP( IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct, - "IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct using the universal property of the coequalizer", - [ [ JointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ], - [ CokernelObject, 1 ], - [ CokernelProjectionWithGivenCokernelObject, 1 ], - [ UniversalMorphismFromCoequalizer, 1 ] ], - - function( cat, A, diagram ) - local joint_pairwise_differences, cokernel_object, cokernel_proj; - - joint_pairwise_differences := JointPairwiseDifferencesOfMorphismsFromCoproduct( cat, A, diagram ); - - cokernel_object := CokernelObject( cat, joint_pairwise_differences ); - - cokernel_proj := CokernelProjectionWithGivenCokernelObject( cat, joint_pairwise_differences, cokernel_object ); - - return UniversalMorphismFromCoequalizer( cat, A, diagram, cokernel_object, cokernel_proj ); - -end ); - -## -AddDerivationToCAP( IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer, - "IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer using the universal property of the cokernel", - [ [ JointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ], - [ Coequalizer, 1 ], - [ ProjectionOntoCoequalizerWithGivenCoequalizer, 1 ], - [ CokernelColift, 1 ] ], - - function( cat, A, diagram ) - local joint_pairwise_differences, coequalizer, coequalizer_projection; - - joint_pairwise_differences := JointPairwiseDifferencesOfMorphismsFromCoproduct( cat, A, diagram ); - - coequalizer := Coequalizer( cat, A, diagram ); - - coequalizer_projection := ProjectionOntoCoequalizerWithGivenCoequalizer( cat, A, diagram, coequalizer ); - - return CokernelColift( cat, joint_pairwise_differences, coequalizer, coequalizer_projection ); - -end ); - ## AddDerivationToCAP( IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram, "IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram using the universal property of the equalizer", @@ -2429,114 +1522,6 @@ AddDerivationToCAP( IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct end ); -## -AddDerivationToCAP( IsomorphismFromPushoutToCoequalizerOfCoproductDiagram, - "IsomorphismFromPushoutToCoequalizerOfCoproductDiagram using the universal property of the pushout", - [ [ Coproduct, 1 ], - [ PreCompose, 4 ], - [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ], - [ Coequalizer, 1 ], - [ ProjectionOntoCoequalizerWithGivenCoequalizer, 1 ], - [ UniversalMorphismFromPushout, 1 ] ], - - function( cat, diagram ) - local ranges_of_diagram, coproduct, coproduct_diagram, coequalizer, 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 := Coequalizer( cat, coproduct, coproduct_diagram ); - - coequalizer_projection := ProjectionOntoCoequalizerWithGivenCoequalizer( cat, coproduct, coproduct_diagram, coequalizer ); - - coequalizer_of_coproduct_diagram := List( [ 1 .. Length( coproduct_diagram ) ], i -> PreCompose( cat, coproduct_diagram[ i ], coequalizer_projection ) ); - - return UniversalMorphismFromPushout( cat, diagram, coequalizer, coequalizer_of_coproduct_diagram ); - -end ); - -## -AddDerivationToCAP( IsomorphismFromPushoutToCoequalizerOfCoproductDiagram, - "IsomorphismFromPushoutToCoequalizerOfCoproductDiagram as the inverse of IsomorphismFromCoequalizerOfCoproductDiagramToPushout", - [ [ IsomorphismFromCoequalizerOfCoproductDiagramToPushout, 1 ], - [ InverseForMorphisms, 1 ] ], - - function( cat, diagram ) - - return InverseForMorphisms( cat, IsomorphismFromCoequalizerOfCoproductDiagramToPushout( cat, diagram ) ); - -end ); - -## -AddDerivationToCAP( IsomorphismFromCoequalizerOfCoproductDiagramToPushout, - "IsomorphismFromCoequalizerOfCoproductDiagramToPushout using the universal property of the coequalizer", - [ [ Coproduct, 1 ], - [ PreCompose, 2 ], - [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ], - [ InjectionOfCofactorOfPushoutWithGivenPushout, 2 ], - [ UniversalMorphismFromCoproductWithGivenCoproduct, 1 ], - [ Pushout, 1 ], - [ UniversalMorphismFromCoequalizer, 1 ] ], - - function( cat, diagram ) - local ranges_of_diagram, coproduct, coproduct_diagram, pushout, test_sink, 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 ) ) ); - - pushout := Pushout( cat, diagram ); - - test_sink := List( [ 1 .. Length( diagram ) ], i -> InjectionOfCofactorOfPushoutWithGivenPushout( cat, diagram, i, pushout ) ); - - pushout_injection := UniversalMorphismFromCoproductWithGivenCoproduct( cat, ranges_of_diagram, pushout, test_sink, coproduct ); - - return UniversalMorphismFromCoequalizer( cat, coproduct, coproduct_diagram, pushout, pushout_injection ); - -end ); - -## -AddDerivationToCAP( IsomorphismFromCoequalizerOfCoproductDiagramToPushout, - "IsomorphismFromCoequalizerOfCoproductDiagramToPushout as the inverse of IsomorphismFromPushoutToCoequalizerOfCoproductDiagram", - [ [ IsomorphismFromPushoutToCoequalizerOfCoproductDiagram, 1 ], - [ InverseForMorphisms, 1 ] ], - - function( cat, diagram ) - - return InverseForMorphisms( cat, IsomorphismFromPushoutToCoequalizerOfCoproductDiagram( cat, diagram ) ); - -end ); - -## -AddDerivationToCAP( ColiftAlongEpimorphism, - "ColiftAlongEpimorphism by inverting the cokernel colift from the cokernel of the kernel to the range of a given epimorphism", - [ [ KernelEmbedding, 1 ], - [ CokernelColift, 2 ], - [ PreCompose, 1 ], - [ InverseForMorphisms, 1 ] ], - - function( cat, epimorphism, test_morphism ) - local kernel_emb, cokernel_colift_to_range_of_epimorphism, cokernel_colift_to_range_of_test_morphism; - - kernel_emb := KernelEmbedding( cat, epimorphism ); - - cokernel_colift_to_range_of_epimorphism := - CokernelColift( cat, kernel_emb, Range( epimorphism ), epimorphism ); - - cokernel_colift_to_range_of_test_morphism := - CokernelColift( cat, kernel_emb, Range( test_morphism ), test_morphism ); - - return PreCompose( cat, InverseForMorphisms( cat, cokernel_colift_to_range_of_epimorphism ), cokernel_colift_to_range_of_test_morphism ); - -end : CategoryFilter := IsAbelianCategory ); - ## AddDerivationToCAP( LiftAlongMonomorphism, "LiftAlongMonomorphism by inverting the kernel lift from the source to the kernel of the cokernel of a given monomorphism", @@ -2572,18 +1557,6 @@ AddDerivationToCAP( ComponentOfMorphismIntoDirectProduct, end ); -## -AddDerivationToCAP( ComponentOfMorphismFromCoproduct, - "ComponentOfMorphismFromCoproduct by composing with the coproduct injection", - [ [ InjectionOfCofactorOfCoproduct, 1 ], - [ PreCompose, 1 ] ], - - function( cat, alpha, cofactors, nr ) - - return PreCompose( cat, InjectionOfCofactorOfCoproduct( cat, cofactors, nr ), alpha ); - -end ); - ## AddDerivationToCAP( ComponentOfMorphismIntoDirectSum, "ComponentOfMorphismIntoDirectSum by composing with the direct sum projection", @@ -2596,18 +1569,6 @@ AddDerivationToCAP( ComponentOfMorphismIntoDirectSum, end ); -## -AddDerivationToCAP( ComponentOfMorphismFromDirectSum, - "ComponentOfMorphismFromDirectSum by composing with the direct sum injection", - [ [ InjectionOfCofactorOfDirectSum, 1 ], - [ PreCompose, 1 ] ], - - function( cat, alpha, summands, nr ) - - return PreCompose( cat, InjectionOfCofactorOfDirectSum( cat, summands, nr ), alpha ); - -end ); - ## AddDerivationToCAP( MorphismBetweenDirectSumsWithGivenDirectSums, "MorphismBetweenDirectSumsWithGivenDirectSums using universal morphisms of direct sums (without support for empty limits)", @@ -2837,84 +1798,6 @@ AddDerivationToCAP( EmbeddingOfEqualizer, end ); -## -AddDerivationToCAP( ProjectionOntoCoequalizer, - "ProjectionOntoCoequalizer using the cokernel projection of JointPairwiseDifferencesOfMorphismsFromCoproduct", - [ [ CokernelProjection, 1 ], - [ JointPairwiseDifferencesOfMorphismsFromCoproduct, 1 ], - [ PreCompose, 1 ], - [ IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer, 1 ] ], - - function( cat, A, diagram ) - local cokernel_proj_of_pairwise_differences; - - cokernel_proj_of_pairwise_differences := CokernelProjection( cat, JointPairwiseDifferencesOfMorphismsFromCoproduct( cat, A, diagram ) ); - - return PreCompose( cat, cokernel_proj_of_pairwise_differences, - IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer( cat, A, diagram ) ); - -end ); - -## -AddDerivationToCAP( IsomorphismFromInitialObjectToZeroObject, - "IsomorphismFromInitialObjectToZeroObject as the unique morphism from initial object to zero object", - [ [ UniversalMorphismFromInitialObject, 1 ], - [ ZeroObject, 1 ] ], - - function( cat ) - - return UniversalMorphismFromInitialObject( cat, ZeroObject( cat ) ); - -end : CategoryFilter := IsAdditiveCategory ); - -## -AddDerivationToCAP( IsomorphismFromInitialObjectToZeroObject, - "IsomorphismFromInitialObjectToZeroObject using the universal property of the zero object", - [ [ UniversalMorphismIntoZeroObject, 1 ], - [ InitialObject, 1 ] ], - - function( cat ) - - return UniversalMorphismIntoZeroObject( cat, InitialObject( cat ) ); - -end ); - -## -AddDerivationToCAP( IsomorphismFromInitialObjectToZeroObject, - "IsomorphismFromInitialObjectToZeroObject as the inverse of IsomorphismFromZeroObjectToInitialObject", - [ [ InverseForMorphisms, 1 ], - [ IsomorphismFromZeroObjectToInitialObject, 1 ] ], - - function( cat ) - - return InverseForMorphisms( cat, IsomorphismFromZeroObjectToInitialObject( cat ) ); - -end ); - -## -AddDerivationToCAP( IsomorphismFromZeroObjectToInitialObject, - "IsomorphismFromZeroObjectToInitialObject as the inverse of IsomorphismFromInitialObjectToZeroObject", - [ [ InverseForMorphisms, 1 ], - [ IsomorphismFromInitialObjectToZeroObject, 1 ] ], - - function( cat ) - - return InverseForMorphisms( cat, IsomorphismFromInitialObjectToZeroObject( cat ) ); - -end ); - -## -AddDerivationToCAP( IsomorphismFromZeroObjectToInitialObject, - "IsomorphismFromZeroObjectToInitialObject using the universal property of the zero object", - [ [ UniversalMorphismFromZeroObject, 1 ], - [ InitialObject, 1 ] ], - - function( cat ) - - return UniversalMorphismFromZeroObject( cat, InitialObject( cat ) ); - -end ); - ## AddDerivationToCAP( IsomorphismFromZeroObjectToTerminalObject, "IsomorphismFromZeroObjectToTerminalObject as the unique morphism from zero object to terminal object", @@ -3032,62 +1915,6 @@ AddDerivationToCAP( IsomorphismFromDirectSumToDirectProduct, end ); -## -AddDerivationToCAP( IsomorphismFromCoproductToDirectSum, - "IsomorphismFromCoproductToDirectSum using cofactor injections and the universal property of the coproduct", - [ [ InjectionOfCofactorOfDirectSum, 2 ], - [ DirectSum, 1 ], - [ UniversalMorphismFromCoproduct, 1 ] ], - - function( cat, diagram ) - local sink; - - sink := List( [ 1 .. Length( diagram ) ], i -> InjectionOfCofactorOfDirectSum( cat, diagram, i ) ); - - return UniversalMorphismFromCoproduct( cat, diagram, DirectSum( cat, diagram ), sink ); - -end ); - -## -AddDerivationToCAP( IsomorphismFromCoproductToDirectSum, - "IsomorphismFromCoproductToDirectSum as the inverse of IsomorphismFromDirectSumToCoproduct", - [ [ InverseForMorphisms, 1 ], - [ IsomorphismFromDirectSumToCoproduct, 1 ] ], - - function( cat, diagram ) - - return InverseForMorphisms( cat, IsomorphismFromDirectSumToCoproduct( cat, diagram ) ); - -end ); - -## -AddDerivationToCAP( IsomorphismFromDirectSumToCoproduct, - "IsomorphismFromDirectSumToCoproduct using cofactor injections and the universal property of the direct sum", - [ [ InjectionOfCofactorOfCoproduct, 2 ], - [ Coproduct, 1 ], - [ UniversalMorphismFromDirectSum, 1 ] ], - - function( cat, diagram ) - local sink; - - sink := List( [ 1 .. Length( diagram ) ], i -> InjectionOfCofactorOfCoproduct( cat, diagram, i ) ); - - return UniversalMorphismFromDirectSum( cat, diagram, Coproduct( cat, diagram ), sink ); - -end ); - -## -AddDerivationToCAP( IsomorphismFromDirectSumToCoproduct, - "IsomorphismFromDirectSumToCoproduct as the inverse of IsomorphismFromCoproductToDirectSum", - [ [ InverseForMorphisms, 1 ], - [ IsomorphismFromCoproductToDirectSum, 1 ] ], - - function( cat, diagram ) - - return InverseForMorphisms( cat, IsomorphismFromCoproductToDirectSum( cat, diagram ) ); - -end ); - ## B -β→ C ←α- A, ℓ•β = α ⇔ ν(ℓ)•H(A,β) = ν(α) ## AddDerivationToCAP( Lift, @@ -3524,17 +2351,6 @@ AddDerivationToCAP( KernelObject, end ); -## -AddDerivationToCAP( CokernelObject, - "CokernelObject as the range of CokernelProjection", - [ [ CokernelProjection, 1 ] ], - - function( cat, mor ) - - return Range( CokernelProjection( cat, mor ) ); - -end ); - ## AddDerivationToCAP( Coproduct, "Coproduct as the range of the first injection", @@ -3568,17 +2384,6 @@ AddDerivationToCAP( DirectProduct, end ); -## -AddDerivationToCAP( Coproduct, - "Coproduct as the range of IsomorphismFromDirectSumToCoproduct", - [ [ IsomorphismFromDirectSumToCoproduct, 1 ] ], - - function( cat, object_product_list ) - - return Range( IsomorphismFromDirectSumToCoproduct( cat, object_product_list ) ); - -end ); - ## AddDerivationToCAP( TerminalObject, "TerminalObject as the source of IsomorphismFromTerminalObjectToZeroObject", @@ -3601,29 +2406,6 @@ AddDerivationToCAP( TerminalObject, end ); -## -AddDerivationToCAP( InitialObject, - "InitialObject as the source of IsomorphismFromInitialObjectToZeroObject", - [ [ IsomorphismFromInitialObjectToZeroObject, 1 ] ], - - function( cat ) - - return Source( IsomorphismFromInitialObjectToZeroObject( cat ) ); - -end ); - -## -AddDerivationToCAP( InitialObject, - "InitialObject as the range of IsomorphismFromZeroObjectToInitialObject", - [ [ IsomorphismFromZeroObjectToInitialObject, 1 ] ], - - function( cat ) - - return Range( IsomorphismFromZeroObjectToInitialObject( cat ) ); - -end ); - - ## AddDerivationToCAP( ImageObject, "ImageObject as the source of ImageEmbedding", @@ -3657,39 +2439,6 @@ AddDerivationToCAP( ImageObject, end ); -## -AddDerivationToCAP( CoimageObject, - "CoimageObject as the range of CoimageProjection", - [ [ CoimageProjection, 1 ] ], - - function( cat, morphism ) - - return Range( CoimageProjection( cat, morphism ) ); - -end ); - -## -AddDerivationToCAP( CoimageObject, - "CoimageObject as the range of IsomorphismFromCokernelOfKernelToCoimage", - [ [ IsomorphismFromCokernelOfKernelToCoimage, 1 ] ], - - function( cat, morphism ) - - return Range( IsomorphismFromCokernelOfKernelToCoimage( cat, morphism ) ); - -end ); - -## -AddDerivationToCAP( CoimageObject, - "CoimageObject as the source of IsomorphismFromCoimageToCokernelOfKernel", - [ [ IsomorphismFromCoimageToCokernelOfKernel, 1 ] ], - - function( cat, morphism ) - - return Source( IsomorphismFromCoimageToCokernelOfKernel( cat, morphism ) ); - -end ); - ## AddDerivationToCAP( CoimageObject, "CoimageObject as the range of CanonicalIdentificationFromImageObjectToCoimage", @@ -3723,17 +2472,6 @@ AddDerivationToCAP( SomeProjectiveObject, end ); -## -AddDerivationToCAP( SomeInjectiveObject, - "SomeInjectiveObject as the range of MonomorphismIntoSomeInjectiveObject", - [ [ MonomorphismIntoSomeInjectiveObject, 1 ] ], - - function( cat, obj ) - - return Range( MonomorphismIntoSomeInjectiveObject( cat, obj ) ); - -end ); - ## AddDerivationToCAP( Equalizer, "Equalizer as the source of EmbeddingOfEqualizer", @@ -3745,17 +2483,6 @@ AddDerivationToCAP( Equalizer, end ); -## -AddDerivationToCAP( Coequalizer, - "Coequalizer as the range of ProjectionOntoCoequalizer", - [ [ ProjectionOntoCoequalizer, 1 ] ], - - function( cat, A, diagram ) - - return Range( ProjectionOntoCoequalizer( cat, A, diagram ) ); - -end ); - ## AddDerivationToCAP( HomologyObject, "HomologyObject as the source of IsomorphismFromHomologyObjectToItsConstructionAsAnImageObject", diff --git a/CAP/gap/Finalize.gi b/CAP/gap/Finalize.gi index 0225a8a79b..ca472cfa69 100644 --- a/CAP/gap/Finalize.gi +++ b/CAP/gap/Finalize.gi @@ -367,7 +367,15 @@ InstallMethod( Finalize, fi; - derivation_list := ShallowCopy( CAP_INTERNAL_FINAL_DERIVATION_LIST.final_derivation_list ); + if ValueOption( "disable_derivations" ) = true then + + derivation_list := [ ]; + + else + + derivation_list := ShallowCopy( CAP_INTERNAL_FINAL_DERIVATION_LIST.final_derivation_list ); + + fi; weight_list := category!.derivations_weight_list; diff --git a/CAP/gap/InstallAdds.gi b/CAP/gap/InstallAdds.gi index b9b9c8270c..e3fde592b6 100644 --- a/CAP/gap/InstallAdds.gi +++ b/CAP/gap/InstallAdds.gi @@ -687,6 +687,7 @@ BindGlobal( "CAP_INTERNAL_INSTALL_WITH_GIVEN_DERIVATION_PAIR", function( without Concatenation( with_given_name, " by calling ", without_given_name, " with the WithGiven argument(s) dropped" ), [ [ ValueGlobal( without_given_name ), 1 ] ], with_given_via_without_given_function + : is_with_given_derivation := true ); AddDerivationToCAP( @@ -694,6 +695,7 @@ BindGlobal( "CAP_INTERNAL_INSTALL_WITH_GIVEN_DERIVATION_PAIR", function( without Concatenation( without_given_name, " by calling ", with_given_name, " with the WithGiven object(s)" ), Concatenation( [ [ ValueGlobal( with_given_name ), 1 ] ], List( additional_preconditions, x -> [ ValueGlobal( x[1] ), x[2] ] ) ), without_given_via_with_given_function + : is_with_given_derivation := true ); end ); diff --git a/CAP/gap/LimitConvenience.gi b/CAP/gap/LimitConvenience.gi index b6347f96f4..d81789eb15 100644 --- a/CAP/gap/LimitConvenience.gi +++ b/CAP/gap/LimitConvenience.gi @@ -298,29 +298,30 @@ end ); fi; - # derive functorials from the universality of the limit/colimit - Assert( 0, Length( limit.diagram_morphism_filter_list ) <= 1 ); - Assert( 0, Length( limit.diagram_morphism_arguments_names ) <= 1 ); - - input_arguments_names := functorial_with_given_record.input_arguments_names; - - source_argument_name := input_arguments_names[2]; - range_argument_name := Last( input_arguments_names ); - - source_diagram_arguments_names := limit.functorial_source_diagram_arguments_names; - range_diagram_arguments_names := limit.functorial_range_diagram_arguments_names; - - # EqualizerFunctorialWithGivenEqualizers would have 8 arguments if the source objects would be given - # -> we have to work around this and derive the source objects from the morphism between the diagrams. - equalizer_preprocessing := ""; - - if Length( limit.diagram_filter_list ) > 0 then + # derive functorials from the universality of the limit + # only do this for limits, colimits will be handled by the automatic dualization of derivations + if limit_colimit = "limit" then - if limit.number_of_targets = 1 then - - Assert( 0, limit.diagram_morphism_arguments_names = [ "mu" ] ); + Assert( 0, Length( limit.diagram_morphism_filter_list ) <= 1 ); + Assert( 0, Length( limit.diagram_morphism_arguments_names ) <= 1 ); + + input_arguments_names := functorial_with_given_record.input_arguments_names; + + source_argument_name := input_arguments_names[2]; + range_argument_name := Last( input_arguments_names ); + + source_diagram_arguments_names := limit.functorial_source_diagram_arguments_names; + range_diagram_arguments_names := limit.functorial_range_diagram_arguments_names; + + # EqualizerFunctorialWithGivenEqualizers would have 8 arguments if the source objects would be given + # -> we have to work around this and derive the source objects from the morphism between the diagrams. + equalizer_preprocessing := ""; + + if Length( limit.diagram_filter_list ) > 0 then - if limit_colimit = "limit" then + if limit.number_of_targets = 1 then + + Assert( 0, limit.diagram_morphism_arguments_names = [ "mu" ] ); test_string := ReplacedStringViaRecord( "PreCompose( cat, projection_with_given( cat, source_diagram..., source_object ), mu )", @@ -332,44 +333,23 @@ end ); ); additional_preconditions := [ "[ PreCompose, 1 ]", Concatenation( "[ ", limit.limit_projection_with_given_name, ", 1 ]" ) ]; - - elif limit_colimit = "colimit" then - - test_string := ReplacedStringViaRecord( - "PreCompose( cat, mu, injection_with_given( cat, range_diagram..., range_object ) )", - rec( - injection_with_given := limit.colimit_injection_with_given_name, - range_diagram := range_diagram_arguments_names, - range_object := range_argument_name, - ) - ); - - additional_preconditions := [ "[ PreCompose, 1 ]", Concatenation( "[ ", limit.colimit_injection_with_given_name, ", 1 ]" ) ]; - - else - - Error( "this should never happen" ); - - fi; - - if limit.number_of_unbound_morphisms > 1 then - - if limit.limit_object_name <> "Equalizer" then - Error( "This is a hack which might not be valid in general." ); + if limit.number_of_unbound_morphisms > 1 then + + if limit.limit_object_name <> "Equalizer" then + + Error( "This is a hack which might not be valid in general." ); + + fi; + + # we are in the Equalizer case, which needs special handling (see above) + equalizer_preprocessing := "local Y, Yp;\n \n Y := Source( mu );\n Yp := Range( mu );\n "; fi; - # we are in the Equalizer case, which needs special handling (see above) - equalizer_preprocessing := "local Y, Yp;\n \n Y := Source( mu );\n Yp := Range( mu );\n "; + else - fi; - - else - - Assert( 0, limit.diagram_morphism_arguments_names = [ "L" ] ); - - if limit_colimit = "limit" then + Assert( 0, limit.diagram_morphism_arguments_names = [ "L" ] ); test_string := ReplacedStringViaRecord( "List( [ 1 .. Length( L ) ], i -> PreCompose( cat, projection_with_given( cat, source_diagram..., i, source_object ), L[i] ) )", @@ -382,56 +362,24 @@ end ); additional_preconditions := [ "[ PreCompose, 2 ]", Concatenation( "[ ", limit.limit_projection_with_given_name, ", 2 ]" ) ]; - elif limit_colimit = "colimit" then - - test_string := ReplacedStringViaRecord( - "List( [ 1 .. Length( L ) ], i -> PreCompose( cat, L[i], injection_with_given( cat, range_diagram..., i, range_object ) ) )", - rec( - injection_with_given := limit.colimit_injection_with_given_name, - range_diagram := range_diagram_arguments_names, - range_object := range_argument_name, - ) - ); - - additional_preconditions := [ "[ PreCompose, 2 ]", Concatenation( "[ ", limit.colimit_injection_with_given_name, ", 2 ]" ) ]; - - else - - Error( "this should never happen" ); - fi; + test_arguments := [ test_string ]; + + else + + Assert( 0, limit.diagram_morphism_arguments_names = [ ] ); + + test_arguments := [ ]; + + additional_preconditions := [ ]; + fi; - test_arguments := [ test_string ]; - - else - - Assert( 0, limit.diagram_morphism_arguments_names = [ ] ); - - test_arguments := [ ]; - - additional_preconditions := [ ]; - - fi; - - if limit_colimit = "limit" then - universal_morphism_with_given_name := limit.limit_universal_morphism_with_given_name; call_arguments := Concatenation( [ "cat" ], range_diagram_arguments_names, [ source_argument_name ], test_arguments, [ range_argument_name ] ); - elif limit_colimit = "colimit" then - - universal_morphism_with_given_name := limit.colimit_universal_morphism_with_given_name; - call_arguments := Concatenation( [ "cat" ], source_diagram_arguments_names, [ range_argument_name ], test_arguments, [ source_argument_name ] ); - - else - - Error( "this should never happen" ); - - fi; - - current_string := ReplacedStringViaRecord( """ + current_string := ReplacedStringViaRecord( """ ## AddDerivationToCAP( functorial_with_given_name, "functorial_with_given_name using the universality of the limit_colimit", @@ -443,23 +391,23 @@ AddDerivationToCAP( functorial_with_given_name, end ); """, - rec( - functorial_with_given_name := functorial_with_given_name, - input_arguments := input_arguments_names, - preconditions := Concatenation( [ Concatenation( "[", universal_morphism_with_given_name, ", 1 ]" ) ], additional_preconditions ), - equalizer_preprocessing := equalizer_preprocessing, - universal_morphism_with_given := universal_morphism_with_given_name, - call_arguments := call_arguments, - limit_colimit := limit_colimit, - ) - ); - - output_string := Concatenation( output_string, current_string ); - - # derive functorial of empty limits from IdentityMorphism - if Length( limit.diagram_filter_list ) = 0 and (limit.limit_object_name <> limit.colimit_object_name or limit_colimit = "limit") then + rec( + functorial_with_given_name := functorial_with_given_name, + input_arguments := input_arguments_names, + preconditions := Concatenation( [ Concatenation( "[", universal_morphism_with_given_name, ", 1 ]" ) ], additional_preconditions ), + equalizer_preprocessing := equalizer_preprocessing, + universal_morphism_with_given := universal_morphism_with_given_name, + call_arguments := call_arguments, + limit_colimit := limit_colimit, + ) + ); - current_string := ReplacedStringViaRecord( """ + output_string := Concatenation( output_string, current_string ); + + # derive functorial of empty limits from IdentityMorphism + if Length( limit.diagram_filter_list ) = 0 then + + current_string := ReplacedStringViaRecord( """ ## AddDerivationToCAP( functorial_name, "functorial_name by taking the identity morphism of object_name", @@ -472,13 +420,15 @@ AddDerivationToCAP( functorial_name, end ); """, - rec( - functorial_name := functorial_name, - object_name := object_name, - ) - ); - - output_string := Concatenation( output_string, current_string ); + rec( + functorial_name := functorial_name, + object_name := object_name, + ) + ); + + output_string := Concatenation( output_string, current_string ); + + fi; fi; diff --git a/CAP/gap/LimitConvenienceOutput.gi b/CAP/gap/LimitConvenienceOutput.gi index b598d6ba8c..b89071d448 100644 --- a/CAP/gap/LimitConvenienceOutput.gi +++ b/CAP/gap/LimitConvenienceOutput.gi @@ -264,17 +264,6 @@ InstallOtherMethodForCompilerForCAP( CoproductFunctorialWithGivenCoproducts, end ); -## -AddDerivationToCAP( CoproductFunctorialWithGivenCoproducts, - "CoproductFunctorialWithGivenCoproducts using the universality of the colimit", - [ [UniversalMorphismFromCoproductWithGivenCoproduct, 1 ], [ PreCompose, 2 ], [ InjectionOfCofactorOfCoproductWithGivenCoproduct, 2 ] ], - - function( cat, P, objects, L, objectsp, Pp ) - - return UniversalMorphismFromCoproductWithGivenCoproduct( cat, objects, Pp, List( [ 1 .. Length( L ) ], i -> PreCompose( cat, L[i], InjectionOfCofactorOfCoproductWithGivenCoproduct( cat, objectsp, i, Pp ) ) ), P ); - -end ); - ## InstallMethod( UniversalMorphismIntoDirectSum, [ IsList ], @@ -494,17 +483,6 @@ AddDerivationToCAP( DirectSumFunctorialWithGivenDirectSums, end ); -## -AddDerivationToCAP( DirectSumFunctorialWithGivenDirectSums, - "DirectSumFunctorialWithGivenDirectSums using the universality of the colimit", - [ [UniversalMorphismFromDirectSumWithGivenDirectSum, 1 ], [ PreCompose, 2 ], [ InjectionOfCofactorOfDirectSumWithGivenDirectSum, 2 ] ], - - function( cat, P, objects, L, objectsp, Pp ) - - return UniversalMorphismFromDirectSumWithGivenDirectSum( cat, objects, Pp, List( [ 1 .. Length( L ) ], i -> PreCompose( cat, L[i], InjectionOfCofactorOfDirectSumWithGivenDirectSum( cat, objectsp, i, Pp ) ) ), P ); - -end ); - InstallOtherMethod( UniversalMorphismIntoFiberProduct, [ IsList, IsList ], @@ -596,17 +574,6 @@ AddDerivationToCAP( FiberProductFunctorialWithGivenFiberProducts, end ); -## -AddDerivationToCAP( PushoutFunctorialWithGivenPushouts, - "PushoutFunctorialWithGivenPushouts using the universality of the colimit", - [ [UniversalMorphismFromPushoutWithGivenPushout, 1 ], [ PreCompose, 2 ], [ InjectionOfCofactorOfPushoutWithGivenPushout, 2 ] ], - - function( cat, P, morphisms, L, morphismsp, Pp ) - - return UniversalMorphismFromPushoutWithGivenPushout( cat, morphisms, Pp, List( [ 1 .. Length( L ) ], i -> PreCompose( cat, L[i], InjectionOfCofactorOfPushoutWithGivenPushout( cat, morphismsp, i, Pp ) ) ), P ); - -end ); - InstallOtherMethod( UniversalMorphismIntoEqualizer, [ IsCapCategoryObject, IsList, IsCapCategoryMorphism ], @@ -702,21 +669,6 @@ AddDerivationToCAP( EqualizerFunctorialWithGivenEqualizers, end ); -## -AddDerivationToCAP( CoequalizerFunctorialWithGivenCoequalizers, - "CoequalizerFunctorialWithGivenCoequalizers using the universality of the colimit", - [ [UniversalMorphismFromCoequalizerWithGivenCoequalizer, 1 ], [ PreCompose, 1 ], [ ProjectionOntoCoequalizerWithGivenCoequalizer, 1 ] ], - - function( cat, P, morphisms, mu, morphismsp, Pp ) - local Y, Yp; - - Y := Source( mu ); - Yp := Range( mu ); - - return UniversalMorphismFromCoequalizerWithGivenCoequalizer( cat, Y, morphisms, Pp, PreCompose( cat, mu, ProjectionOntoCoequalizerWithGivenCoequalizer( cat, Yp, morphismsp, Pp ) ), P ); - -end ); - InstallOtherMethod( KernelLift, [ IsCapCategoryMorphism, IsCapCategoryMorphism ], @@ -808,17 +760,6 @@ AddDerivationToCAP( KernelObjectFunctorialWithGivenKernelObjects, end ); -## -AddDerivationToCAP( CokernelObjectFunctorialWithGivenCokernelObjects, - "CokernelObjectFunctorialWithGivenCokernelObjects using the universality of the colimit", - [ [CokernelColiftWithGivenCokernelObject, 1 ], [ PreCompose, 1 ], [ CokernelProjectionWithGivenCokernelObject, 1 ] ], - - function( cat, P, alpha, mu, alphap, Pp ) - - return CokernelColiftWithGivenCokernelObject( cat, alpha, Pp, PreCompose( cat, mu, CokernelProjectionWithGivenCokernelObject( cat, alphap, Pp ) ), P ); - -end ); - ## AddDerivationToCAP( TerminalObjectFunctorialWithGivenTerminalObjects, "TerminalObjectFunctorialWithGivenTerminalObjects using the universality of the limit", @@ -842,29 +783,6 @@ AddDerivationToCAP( TerminalObjectFunctorial, end ); -## -AddDerivationToCAP( InitialObjectFunctorialWithGivenInitialObjects, - "InitialObjectFunctorialWithGivenInitialObjects using the universality of the colimit", - [ [UniversalMorphismFromInitialObjectWithGivenInitialObject, 1 ] ], - - function( cat, P, Pp ) - - return UniversalMorphismFromInitialObjectWithGivenInitialObject( cat, Pp, P ); - -end ); - -## -AddDerivationToCAP( InitialObjectFunctorial, - "InitialObjectFunctorial by taking the identity morphism of InitialObject", - [ [ InitialObject, 1 ], - [ IdentityMorphism, 1 ] ], - - function( cat ) - - return IdentityMorphism( cat, InitialObject( cat ) ); - -end ); - ## AddDerivationToCAP( ZeroObjectFunctorialWithGivenZeroObjects, "ZeroObjectFunctorialWithGivenZeroObjects using the universality of the limit", @@ -887,14 +805,3 @@ AddDerivationToCAP( ZeroObjectFunctorial, return IdentityMorphism( cat, ZeroObject( cat ) ); end ); - -## -AddDerivationToCAP( ZeroObjectFunctorialWithGivenZeroObjects, - "ZeroObjectFunctorialWithGivenZeroObjects using the universality of the colimit", - [ [UniversalMorphismFromZeroObjectWithGivenZeroObject, 1 ] ], - - function( cat, P, Pp ) - - return UniversalMorphismFromZeroObjectWithGivenZeroObject( cat, Pp, P ); - -end ); diff --git a/CAP/read.g b/CAP/read.g index a7e7298f55..20133b0dfa 100644 --- a/CAP/read.g +++ b/CAP/read.g @@ -36,6 +36,8 @@ ReadPackage( "CAP", "gap/DerivedMethods.gi" ); ReadPackage( "CAP", "gap/LimitConvenienceOutput.gi" ); +ReadPackage( "CAP", "gap/DerivedMethods.autogen.gi" ); + ReadPackage( "CAP", "gap/OppositeCategory.gi" ); ReadPackage( "CAP", "gap/ProductCategory.gi" ); diff --git a/CompilerForCAP/PackageInfo.g b/CompilerForCAP/PackageInfo.g index fd480bb9a9..f34c3976c8 100644 --- a/CompilerForCAP/PackageInfo.g +++ b/CompilerForCAP/PackageInfo.g @@ -10,7 +10,7 @@ SetPackageInfo( rec( PackageName := "CompilerForCAP", Subtitle := "Speed up computations in CAP categories", -Version := "2023.09-02", +Version := "2023.09-03", 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", diff --git a/CompilerForCAP/gap/LogicTemplates.gi b/CompilerForCAP/gap/LogicTemplates.gi index 2fdd4b49ee..d125c1862f 100644 --- a/CompilerForCAP/gap/LogicTemplates.gi +++ b/CompilerForCAP/gap/LogicTemplates.gi @@ -343,6 +343,15 @@ InstallGlobalFunction( CAP_JIT_INTERNAL_ENHANCE_LOGIC_TEMPLATE, function ( templ end ); +# x -> x => ID_FUNC +CapJitAddLogicTemplate( + rec( + variable_names := [ ], + src_template := "x -> x", + dst_template := "ID_FUNC", + ) +); + # ID_FUNC( value ) => value CapJitAddLogicTemplate( rec( @@ -352,6 +361,16 @@ CapJitAddLogicTemplate( ) ); +# List( list, ID_FUNC ) => list +CapJitAddLogicTemplate( + rec( + variable_names := [ "list" ], + variable_filters := [ IsList ], + src_template := "List( list, ID_FUNC )", + dst_template := "list", + ) +); + # List( List( L, f ), g ) => List( L, x -> g( f( x ) ) ) CapJitAddLogicTemplate( rec( @@ -445,6 +464,15 @@ CapJitAddLogicTemplate( ) ); +# Length( [ 1 .. n ] ) => n +CapJitAddLogicTemplate( + rec( + variable_names := [ "n" ], + src_template := "Length( [ 1 .. n ] )", + dst_template := "n", + ) +); + # [ 1 .. range_end ][i] => i CapJitAddLogicTemplate( rec( diff --git a/CompilerForCAP/gap/PrecompileCategory.gi b/CompilerForCAP/gap/PrecompileCategory.gi index 56c9609090..e32ff769ce 100644 --- a/CompilerForCAP/gap/PrecompileCategory.gi +++ b/CompilerForCAP/gap/PrecompileCategory.gi @@ -14,8 +14,8 @@ InstallGlobalFunction( "CapJitPrecompileCategory", function ( category_construct fi; # check if category_constructor returns a new instance of the category every time - cat1 := CallFuncList( category_constructor, given_arguments : no_precompiled_code := true ); - cat2 := CallFuncList( category_constructor, given_arguments : no_precompiled_code := true ); + cat1 := CallFuncList( category_constructor, given_arguments : no_precompiled_code := true, overhead := false ); + cat2 := CallFuncList( category_constructor, given_arguments : no_precompiled_code := true, overhead := false ); if IsIdenticalObj( cat1, cat2 ) then @@ -25,7 +25,7 @@ InstallGlobalFunction( "CapJitPrecompileCategory", function ( category_construct fi; # check that category_constructor supports `FinalizeCategory` - cat := CallFuncList( category_constructor, given_arguments : FinalizeCategory := false, no_precompiled_code := true ); + cat := CallFuncList( category_constructor, given_arguments : FinalizeCategory := false, no_precompiled_code := true, overhead := false ); if IsFinalized( cat ) then diff --git a/CompilerForCAP/tst/Logic.tst b/CompilerForCAP/tst/Logic.tst index f7274a9e74..cd036a634c 100644 --- a/CompilerForCAP/tst/Logic.tst +++ b/CompilerForCAP/tst/Logic.tst @@ -6,7 +6,7 @@ true # gap> func := function ( ) -> return List( [ 1, 2 ], x -> x ); end;; +> return List( [ 1, 2 ], x -> x^2 ); end;; # gap> tree := ENHANCED_SYNTAX_TREE( func );; @@ -14,15 +14,15 @@ gap> tree := CapJitAppliedLogic( tree );; gap> Display( ENHANCED_SYNTAX_TREE_CODE( tree ) ); function ( ) return [ function ( x_2 ) - return x_2; + return x_2^2; end( 1 ), function ( x_2 ) - return x_2; + return x_2^2; end( 2 ) ]; end # gap> func := function ( L1, L2 ) -> return List( Concatenation( L1, L2 ), x -> x ); end;; +> return List( Concatenation( L1, L2 ), x -> x^2 ); end;; # gap> tree := ENHANCED_SYNTAX_TREE( func );; @@ -30,9 +30,9 @@ gap> tree := CapJitAppliedLogic( tree );; gap> Display( ENHANCED_SYNTAX_TREE_CODE( tree ) ); function ( L1_1, L2_1 ) return Concatenation( List( L1_1, function ( x_2 ) - return x_2; + return x_2^2; end ), List( L2_1, function ( x_2 ) - return x_2; + return x_2^2; end ) ); end @@ -164,13 +164,13 @@ function ( list1_1, list2_1, list3_1 ) end # -gap> func := cat -> CapCategory( CreateCapCategoryObjectWithAttributes( cat ) );; +gap> func := { cat, size } -> CapCategory( CreateCapCategoryObjectWithAttributes( cat, Size, 1 ) );; # gap> tree := ENHANCED_SYNTAX_TREE( func );; gap> tree := CapJitAppliedLogic( tree );; gap> Display( ENHANCED_SYNTAX_TREE_CODE( tree ) ); -function ( cat_1 ) +function ( cat_1, size_1 ) return cat_1; end diff --git a/CompilerForCAP/tst/generate_opposite_derivations.tst b/CompilerForCAP/tst/generate_opposite_derivations.tst new file mode 100644 index 0000000000..09bc28bc76 --- /dev/null +++ b/CompilerForCAP/tst/generate_opposite_derivations.tst @@ -0,0 +1,497 @@ +gap> START_TEST( "generate_opposite_derivations" ); + +# +gap> LoadPackage( "CompilerForCAP", false ); +true + +# +gap> LoadPackage( "CAP", false ); +true + +# +# We introduce functions for viewing objects in different instances of "the same" category. +# We do not actually call those functions, so we do not need an implementation. +gap> BindGlobal( "CoercedObject", function ( cat_from, cat_to, object ) +> +> Error( "not implemented" ); +> +> end ); + +# +gap> BindGlobal( "CoercedMorphism", function ( cat_from, cat_to, object ) +> +> Error( "not implemented" ); +> +> end ); + +# +gap> CapJitAddTypeSignature( "CoercedObject", [ IsCapCategory, IsCapCategory, IsCapCategoryObject ], function ( input_types ) +> +> return CapJitDataTypeOfObjectOfCategory( input_types[2].category ); +> +> end ); + +# +gap> CapJitAddTypeSignature( "CoercedMorphism", [ IsCapCategory, IsCapCategory, IsCapCategoryMorphism ], function ( input_types ) +> +> return CapJitDataTypeOfMorphismOfCategory( input_types[2].category ); +> +> end ); + +# +# add logic templates which cancel coercions +gap> CapJitAddLogicTemplate( +> rec( +> variable_names := [ "cat", "cat2", "object" ], +> src_template := "CoercedObject( cat2, cat, CoercedObject( cat, cat2, object ) )", +> dst_template := "object", +> ) +> ); +gap> CapJitAddLogicTemplate( +> rec( +> variable_names := [ "cat", "cat2", "morphism" ], +> src_template := "CoercedMorphism( cat2, cat, CoercedMorphism( cat, cat2, morphism ) )", +> dst_template := "morphism", +> ) +> ); +gap> CapJitAddLogicTemplate( +> rec( +> variable_names := [ "cat", "cat2", "morphism" ], +> src_template := "CoercedObject( cat2, cat, Source( CoercedMorphism( cat, cat2, morphism ) ) )", +> dst_template := "Source( morphism )", +> ) +> ); +gap> CapJitAddLogicTemplate( +> rec( +> variable_names := [ "cat", "cat2", "morphism" ], +> src_template := "CoercedObject( cat2, cat, Range( CoercedMorphism( cat, cat2, morphism ) ) )", +> dst_template := "Range( morphism )", +> ) +> ); + +# +# checks if `filter` is a filter of the form `HasProperty and Property` for a categorical property +# and returns `[ "Property", "DualProperty" ]` if this is the case +# `IsCapCategory` is handled as a self-dual special case +gap> BindGlobal( "PropertyAndOppositeProperty", function ( filter ) +> local names_filter, pos; +> +> if IsIdenticalObj( filter, IsCapCategory ) then +> +> return [ "IsCapCategory", "IsCapCategory" ]; +> +> fi; +> +> if not IsFilter( filter ) then +> +> return fail; +> +> fi; +> +> names_filter := NamesFilter( filter ); +> +> if not Length( names_filter ) = 2 then +> +> return fail; +> +> fi; +> +> # `HasFilter` comes after `Filter` (if `Filter` was declared via `DeclareFilter`) +> if names_filter[2] <> Concatenation( "Has", names_filter[1] ) then +> +> return fail; +> +> fi; +> +> pos := PositionProperty( CAP_INTERNAL_CATEGORICAL_PROPERTIES_LIST, x -> x[1] = names_filter[1] ); +> +> if pos = fail then +> +> return fail; +> +> fi; +> +> return CAP_INTERNAL_CATEGORICAL_PROPERTIES_LIST[pos]; +> +> end ); + +# +gap> CAP_JIT_INTERNAL_COPY_OF_CATEGORY := fail;; + +# +gap> BindGlobal( "GenerateOppositeDerivation", function ( derivation ) +> local operation_name, dual_operation_name, list_of_operations_to_install, property_pair, properties, dummy, op, op_op, copy, info, input_arguments_names, filter_list, return_type, prepared_arguments_strings, recoercion_function_string, compiled_func; +> +> PushOptions( rec( disable_derivations := true, overhead := false ) ); +> +> operation_name := TargetOperation( derivation ); +> +> dual_operation_name := CAP_INTERNAL_METHOD_NAME_RECORD.(operation_name).dual_operation; +> +> # create a dummy category with dual preconditions +> list_of_operations_to_install := List( UsedOperationsWithMultiplesAndCategoryGetters( derivation ), x -> CAP_INTERNAL_METHOD_NAME_RECORD.(x[1]).dual_operation ); +> +> property_pair := PropertyAndOppositeProperty( CategoryFilter( derivation ) ); +> +> if property_pair[2] = "IsCapCategory" then +> +> properties := [ ]; +> +> else +> +> properties := [ property_pair[2] ]; +> +> fi; +> +> dummy := DummyCategory( rec( +> name := Concatenation( "Dummy for ", dual_operation_name ), +> list_of_operations_to_install := list_of_operations_to_install, +> properties := properties, +> ) ); +> +> StopCompilationAtPrimitivelyInstalledOperationsOfCategory( dummy ); +> +> # dualize the category +> op := Opposite( dummy : only_primitive_operations := true, FinalizeCategory := false ); +> +> # trigger the derivation manually +> TryToInstallDerivation( op!.derivations_weight_list, derivation ); +> +> Assert( 0, CanCompute( op, operation_name ) ); +> +> Finalize( op ); +> +> # take the opposite again, where the dual operation is now available +> op_op := Opposite( op, Concatenation( "Double opposite of ", Name( dummy ) ) ); +> +> Assert( 0, CanCompute( op_op, dual_operation_name ) ); +> +> # reinterpret the double dual as the original category +> copy := ReinterpretationOfCategory( op_op, rec( +> name := Concatenation( "Copy of ", Name( dummy ), " (as double opposite of itself)" ), +> category_filter := IsDummyCategory, +> category_object_filter := IsDummyCategoryObject, +> category_morphism_filter := IsDummyCategoryMorphism, +> object_constructor := { copy, orig_object } -> CoercedObject( OppositeCategory( OppositeCategory( ModelingCategory( copy ) ) ), copy, orig_object ), +> object_datum := { copy, copy_object } -> CoercedObject( copy, OppositeCategory( OppositeCategory( ModelingCategory( copy ) ) ), copy_object ), +> morphism_constructor := { copy, source, orig_morphism, range } -> CoercedMorphism( OppositeCategory( OppositeCategory( ModelingCategory( copy ) ) ), copy, orig_morphism ), +> morphism_datum := { copy, copy_morphism } -> CoercedMorphism( copy, OppositeCategory( OppositeCategory( ModelingCategory( copy ) ) ), copy_morphism ), +> modeling_tower_object_constructor := { copy, orig_object } -> ObjectConstructor( ModelingCategory( copy ), ObjectConstructor( OppositeCategory( ModelingCategory( copy ) ), orig_object ) ), +> modeling_tower_object_datum := { copy, tower_object } -> Opposite( Opposite( tower_object ) ), +> modeling_tower_morphism_constructor := { copy, source, orig_morphism, range } -> MorphismConstructor( ModelingCategory( copy ), source, MorphismConstructor( OppositeCategory( ModelingCategory( copy ) ), Opposite( range ), orig_morphism, Opposite( source ) ), range ), +> modeling_tower_morphism_datum := { copy, tower_morphism } -> Opposite( Opposite( tower_morphism ) ), +> ) ); +> +> # to compute the dual operation in the original category, we coerce objects and morphism to the copy, +> # compute the dual operation there, and re-coerce the result back to the original category +> info := CAP_INTERNAL_METHOD_NAME_RECORD.(dual_operation_name); +> +> input_arguments_names := info.input_arguments_names; +> filter_list := info.filter_list; +> return_type := info.return_type; +> +> prepared_arguments_strings := List( [ 1 .. Length( filter_list ) ], function( i ) +> local filter, argument_name; +> +> filter := filter_list[i]; +> argument_name := input_arguments_names[i]; +> +> if filter = "category" then +> +> return "copy"; +> +> elif filter = "object" then +> +> return Concatenation( "CoercedObject( cat, copy, ", argument_name, " )" ); +> +> elif filter = "morphism" then +> +> return Concatenation( "CoercedMorphism( cat, copy, ", argument_name, " )" ); +> +> elif filter in [ "integer", "element_of_commutative_ring_of_linear_structure", "nonneg_integer_or_infinity", "list_of_elements_of_commutative_ring_of_linear_structure" ] then +> +> return argument_name; +> +> elif filter = "list_of_objects" then +> +> return Concatenation( "List( ", argument_name, ", x -> CoercedObject( cat, copy, x ) )" ); +> +> elif filter = "list_of_morphisms" then +> +> return Concatenation( "List( ", argument_name, ", x -> CoercedMorphism( cat, copy, x ) )" ); +> +> elif filter = "pair_of_morphisms" then +> +> return Concatenation( "Pair( CoercedMorphism( cat, copy, ", argument_name, "[1] ), CoercedMorphism( cat, copy, ", argument_name, "[2] ) )" ); +> +> elif filter = "list_of_integers_and_list_of_morphisms" then +> +> return Concatenation( "Pair( ", argument_name, "[1], List( ", argument_name, "[2], x -> CoercedMorphism( cat, copy, x ) ) )" ); +> +> else +> +> Error( "this case is not handled yet" ); +> +> fi; +> +> end ); +> +> if return_type = "bool" then +> +> recoercion_function_string := "IdFunc"; +> +> elif return_type = "object" then +> +> recoercion_function_string := "(obj -> CoercedObject( copy, cat, obj ))"; +> +> elif return_type = "morphism" then +> +> recoercion_function_string := "(mor -> CoercedMorphism( copy, cat, mor ))"; +> +> else +> +> Error( "this case is not handled yet" ); +> +> fi; +> +> CAP_JIT_INTERNAL_COPY_OF_CATEGORY := copy; +> +> compiled_func := CapJitCompiledFunction( +> EvalString( ReplacedStringViaRecord( +> """ +> function( input_arguments... ) +> local copy; +> +> copy := CAP_JIT_INTERNAL_COPY_OF_CATEGORY; +> +> return recoercion_function( dual_operation( prepared_arguments... ) ); +> +> end +> """, +> rec( +> input_arguments := input_arguments_names, +> prepared_arguments := prepared_arguments_strings, +> dual_operation := dual_operation_name, +> recoercion_function := recoercion_function_string, +> ) +> ) ), +> dummy, +> filter_list, +> return_type +> ); +> +> Assert( 0, ValueOption( "disable_derivations" ) = true ); +> Assert( 0, ValueOption( "overhead" ) = false ); +> +> PopOptions( ); +> +> Assert( 0, ValueOption( "disable_derivations" ) = fail ); +> Assert( 0, ValueOption( "overhead" ) = fail ); +> +> return compiled_func; +> +> end ); + +# +# collect all derivations +gap> derivations_by_target := CAP_INTERNAL_DERIVATION_GRAPH!.derivations_by_target;; +gap> derivations := Concatenation( List( SortedList( RecNames( derivations_by_target ) ), name -> derivations_by_target.(name) ) );; + +# +# exclude various derivations +gap> derivations := Filtered( derivations, function ( d ) +> local info, used_op_names_with_multiples_and_category_getters, dualized_used_op_names_with_multiples_and_category_getters, x; +> +> # exclude previously autogenerated derivations +> if d!.is_autogenerated_by_CompilerForCAP then +> +> return false; +> +> fi; +> +> # exclude WithGiven derivations; those are automatically generated anyway +> if d!.is_with_given_derivation then +> +> return false; +> +> fi; +> +> info := CAP_INTERNAL_METHOD_NAME_RECORD.(TargetOperation( d )); +> +> # exclude operations without duals +> if not IsBound( info.dual_operation ) then +> +> return false; +> +> fi; +> +> # exclude operations from other packages for now +> if PackageOfCAPOperation( info.dual_operation ) <> "CAP" then +> +> return false; +> +> fi; +> +> # exclude random functions +> if StartsWith( TargetOperation( d ), "Random" ) then +> +> return false; +> +> fi; +> +> # exclude operations possibly returning fail +> if EndsWith( info.return_type, "fail" ) then +> +> return false; +> +> fi; +> +> # exclude derivations with category filters for which we have no dual +> if PropertyAndOppositeProperty( CategoryFilter( d ) ) = fail then +> +> return false; +> +> fi; +> +> # exclude derivations with FunctionCalledBeforeInstallation +> if HasFunctionCalledBeforeInstallation( d ) then +> +> return false; +> +> fi; +> +> used_op_names_with_multiples_and_category_getters := UsedOperationsWithMultiplesAndCategoryGetters( d ); +> +> dualized_used_op_names_with_multiples_and_category_getters := [ ]; +> +> for x in used_op_names_with_multiples_and_category_getters do +> +> # exclude if preconditions do not have duals +> if not IsBound( CAP_INTERNAL_METHOD_NAME_RECORD.(x[1]).dual_operation ) then +> +> return false; +> +> fi; +> +> # exclude operations from other packages for now +> if PackageOfCAPOperation( CAP_INTERNAL_METHOD_NAME_RECORD.(x[1]).dual_operation ) <> "CAP" then +> +> return false; +> +> fi; +> +> # exclude if other categories are involved +> if x[3] <> fail then +> +> return false; +> +> fi; +> +> Add( dualized_used_op_names_with_multiples_and_category_getters, [ CAP_INTERNAL_METHOD_NAME_RECORD.(x[1]).dual_operation, x[2], x[3] ] ); +> +> od; +> +> # exclude if the derivation is self-dual +> if info.dual_operation = TargetOperation( d ) and Set( used_op_names_with_multiples_and_category_getters ) = Set( dualized_used_op_names_with_multiples_and_category_getters ) then +> +> return false; +> +> fi; +> +> # exclude if twocells are involved +> if "twocell" in info.filter_list or ForAny( used_op_names_with_multiples_and_category_getters, x -> "twocell" in CAP_INTERNAL_METHOD_NAME_RECORD.(x[1]).filter_list ) then +> +> return false; +> +> fi; +> +> return true; +> +> end );; + +# +# sort derivations by the names of the dual operations +gap> StableSortBy( derivations, d -> CAP_INTERNAL_METHOD_NAME_RECORD.(TargetOperation( d )).dual_operation ); + +# +gap> output_string := +> """# SPDX-License-Identifier: GPL-2.0-or-later +> # CAP: Categories, Algorithms, Programming +> # +> # Implementations +> # +> # THIS FILE IS AUTOMATICALLY GENERATED, SEE CompilerForCAP/tst/generate_opposite_derivations.tst +> """;; + +# +# loop over derivations and dualize them +# +gap> for derivation in derivations do +> +> operation_name := TargetOperation( derivation ); +> dual_operation_name := CAP_INTERNAL_METHOD_NAME_RECORD.(operation_name).dual_operation; +> +> description := DerivationName( derivation ); +> +> description_op := Concatenation( "dualizing the derivation of ", TargetOperation( derivation ), " by ", description ); +> +> func := GenerateOppositeDerivation( derivation ); +> +> preconditions_string := JoinStringsWithSeparator( List( UsedOperationsWithMultiplesAndCategoryGetters( derivation ), function( x ) +> local operation_name, dual_operation_name; +> +> Assert( 0, x[3] = fail ); +> +> operation_name := x[1]; +> +> dual_operation_name := CAP_INTERNAL_METHOD_NAME_RECORD.(operation_name).dual_operation; +> +> return Concatenation( " [ ", dual_operation_name, ", ", String( x[2] ), " ],\n" ); +> +> end ), "" ); +> +> function_string := CapJitPrettyPrintFunction( func ); +> +> if PositionSublist( function_string, "CAP_JIT_INTERNAL_GLOBAL_VARIABLE_" ) <> fail then +> +> # COVERAGE_IGNORE_NEXT_LINE +> Error( "Could not get rid of all global variables, see ." ); +> +> fi; +> +> current_string := Concatenation( +> "\n", +> "##\n", +> "AddDerivationToCAP( ", dual_operation_name, ",\n", +> " \"", description_op, "\",\n", +> " [\n", +> preconditions_string, +> " ],\n", +> " \n", +> " ", function_string, " : CategoryFilter := ", PropertyAndOppositeProperty( CategoryFilter( derivation ) )[2], ",\n", +> " Weight := ", String( DerivationWeight( derivation ) ), ",\n", +> " is_autogenerated_by_CompilerForCAP := true );\n" +> ); +> +> output_string := Concatenation( output_string, current_string ); +> +> od; + +# +# write result to file +gap> if not IsExistingFileInPackageForHomalg( "CAP", "DerivedMethods.autogen.gi" ) or output_string <> ReadFileFromPackageForHomalg( "CAP", "DerivedMethods.autogen.gi" ) then +> +> output_path := Filename( DirectoryTemporary( ), "DerivedMethods.autogen.gi" ); +> +> WriteFileForHomalg( output_path, output_string ); +> +> Display( Concatenation( +> "WARNING: The file DerivedMethods.autogen.gi differs from the automatically generated one. ", +> "You can view the automatically generated file at the following path: ", +> output_path +> ) ); +> +> fi; + +# +gap> STOP_TEST( "generate_opposite_derivations" ); diff --git a/FreydCategoriesForCAP/PackageInfo.g b/FreydCategoriesForCAP/PackageInfo.g index 08a4ae7ff8..2bb4426e18 100644 --- a/FreydCategoriesForCAP/PackageInfo.g +++ b/FreydCategoriesForCAP/PackageInfo.g @@ -10,7 +10,7 @@ SetPackageInfo( rec( PackageName := "FreydCategoriesForCAP", Subtitle := "Freyd categories - Formal (co)kernels for additive categories", -Version := "2023.09-02", +Version := "2023.09-03", 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", diff --git a/FreydCategoriesForCAP/gap/CategoryOfRowsAsAdditiveClosureOfRingAsCategory_CompilerLogic.gi b/FreydCategoriesForCAP/gap/CategoryOfRowsAsAdditiveClosureOfRingAsCategory_CompilerLogic.gi index 4c1b4ee104..e92d243176 100644 --- a/FreydCategoriesForCAP/gap/CategoryOfRowsAsAdditiveClosureOfRingAsCategory_CompilerLogic.gi +++ b/FreydCategoriesForCAP/gap/CategoryOfRowsAsAdditiveClosureOfRingAsCategory_CompilerLogic.gi @@ -89,15 +89,6 @@ CapJitAddLogicTemplate( ) ); -# Length( [ 1 .. n ] ) => n -CapJitAddLogicTemplate( - rec( - variable_names := [ "n" ], - src_template := "Length( [ 1 .. n ] )", - dst_template := "n", - ) -); - # n - 1 + 1 => n CapJitAddLogicTemplate( rec( @@ -134,15 +125,6 @@ CapJitAddLogicTemplate( ) ); -# List( L, x -> x ) => L -CapJitAddLogicTemplate( - rec( - variable_names := [ "list" ], - src_template := "List( list, x -> x )", - dst_template := "list", - ) -); - # EntriesOfHomalgMatrixAsListList( matrix )[row][col] => matrix[row][col] CapJitAddLogicTemplate( rec( diff --git a/LinearAlgebraForCAP/PackageInfo.g b/LinearAlgebraForCAP/PackageInfo.g index e70932c956..2207edf36b 100644 --- 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 := "2023.09-02", +Version := "2023.09-03", 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", diff --git a/LinearAlgebraForCAP/gap/CompilerLogic.gi b/LinearAlgebraForCAP/gap/CompilerLogic.gi index 35d36b9e9c..7d268bb610 100644 --- a/LinearAlgebraForCAP/gap/CompilerLogic.gi +++ b/LinearAlgebraForCAP/gap/CompilerLogic.gi @@ -54,12 +54,3 @@ CapJitAddLogicTemplate( needed_packages := [ [ "MatricesForHomalg", ">= 2020.05.19" ] ], ) ); - -# Length( [ 1 .. n ] ) -> n -CapJitAddLogicTemplate( - rec( - variable_names := [ "n" ], - src_template := "Length( [ 1 .. n ] )", - dst_template := "n" - ) -); diff --git a/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi b/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi index 596d46837b..5a33bb1a17 100644 --- a/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi +++ b/LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi @@ -639,7 +639,7 @@ function ( cat_1, Y_1, morphisms_1 ) end ######## - , 2819 : IsPrecompiledDerivation := true ); + , 2824 : IsPrecompiledDerivation := true ); ## AddCoequalizerFunctorial( cat, @@ -659,7 +659,7 @@ function ( cat_1, morphisms_1, mu_1, morphismsp_1 ) end ######## - , 11479 : IsPrecompiledDerivation := true ); + , 11500 : IsPrecompiledDerivation := true ); ## AddCoequalizerFunctorialWithGivenCoequalizers( cat, @@ -679,7 +679,7 @@ function ( cat_1, P_1, morphisms_1, mu_1, morphismsp_1, Pp_1 ) end ######## - , 5840 : IsPrecompiledDerivation := true ); + , 5851 : IsPrecompiledDerivation := true ); ## AddCoevaluationForDual( cat, @@ -782,7 +782,7 @@ function ( cat_1, alpha_1, mu_1, alphap_1 ) end ######## - , 602 : IsPrecompiledDerivation := true ); + , 603 : IsPrecompiledDerivation := true ); ## AddCoimageObjectFunctorialWithGivenCoimageObjects( cat, @@ -793,7 +793,7 @@ function ( cat_1, C_1, alpha_1, mu_1, alphap_1, Cp_1 ) end ######## - , 401 : IsPrecompiledDerivation := true ); + , 402 : IsPrecompiledDerivation := true ); ## AddCoimageProjection( cat, @@ -867,7 +867,7 @@ function ( cat_1, alpha_1, mu_1, alphap_1 ) end ######## - , 605 : IsPrecompiledDerivation := true ); + , 606 : IsPrecompiledDerivation := true ); ## AddCokernelObjectFunctorialWithGivenCokernelObjects( cat, @@ -880,7 +880,7 @@ function ( cat_1, P_1, alpha_1, mu_1, alphap_1, Pp_1 ) end ######## - , 404 : IsPrecompiledDerivation := true ); + , 405 : IsPrecompiledDerivation := true ); ## AddCokernelProjection( cat, @@ -942,7 +942,7 @@ function ( cat_1, alpha_1, I_1, i_1 ) end ######## - , 402 : IsPrecompiledDerivation := true ); + , 403 : IsPrecompiledDerivation := true ); ## AddComponentOfMorphismFromDirectSum( cat, @@ -1015,7 +1015,7 @@ function ( cat_1, objects_1, L_1, objectsp_1 ) end ######## - , 2118 : IsPrecompiledDerivation := true ); + , 2123 : IsPrecompiledDerivation := true ); ## AddCoproductFunctorialWithGivenCoproducts( cat, @@ -1035,7 +1035,7 @@ function ( cat_1, P_1, objects_1, L_1, objectsp_1, Pp_1 ) end ######## - , 1713 : IsPrecompiledDerivation := true ); + , 1718 : IsPrecompiledDerivation := true ); ## AddDirectProduct( cat, @@ -1472,7 +1472,7 @@ function ( cat_1, H_1_1, L_1, H_2_1 ) end ######## - , 3010 : IsPrecompiledDerivation := true ); + , 3011 : IsPrecompiledDerivation := true ); ## AddHomomorphismStructureOnMorphisms( cat, @@ -1629,7 +1629,7 @@ function ( cat_1, objects_1, k_1 ) end ######## - , 503 : IsPrecompiledDerivation := true ); + , 504 : IsPrecompiledDerivation := true ); ## AddInjectionOfCofactorOfCoproductWithGivenCoproduct( cat, @@ -1645,7 +1645,7 @@ function ( cat_1, objects_1, k_1, P_1 ) end ######## - , 504 : IsPrecompiledDerivation := true ); + , 505 : IsPrecompiledDerivation := true ); ## AddInjectionOfCofactorOfDirectSum( cat, @@ -1701,7 +1701,7 @@ function ( cat_1, morphisms_1, k_1 ) end ######## - , 9061 : IsPrecompiledDerivation := true ); + , 9079 : IsPrecompiledDerivation := true ); ## AddInjectionOfCofactorOfPushoutWithGivenPushout( cat, @@ -1726,7 +1726,7 @@ function ( cat_1, morphisms_1, k_1, P_1 ) end ######## - , 9062 : IsPrecompiledDerivation := true ); + , 9080 : IsPrecompiledDerivation := true ); ## AddInjectiveColift( cat, @@ -2555,7 +2555,7 @@ function ( cat_1, D_1 ) end ######## - , 4330 : IsPrecompiledDerivation := true ); + , 4337 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct( cat, @@ -2572,7 +2572,7 @@ function ( cat_1, A_1, D_1 ) end ######## - , 1409 : IsPrecompiledDerivation := true ); + , 1411 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromCoimageToCokernelOfKernel( cat, @@ -2603,7 +2603,7 @@ function ( cat_1, A_1, D_1 ) end ######## - , 1409 : IsPrecompiledDerivation := true ); + , 1411 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromCokernelOfKernelToCoimage( cat, @@ -3091,7 +3091,7 @@ function ( cat_1, D_1 ) end ######## - , 4330 : IsPrecompiledDerivation := true ); + , 4337 : IsPrecompiledDerivation := true ); ## AddIsomorphismFromTensorProductWithCoDualObjectToInternalCoHom( cat, @@ -3176,7 +3176,7 @@ function ( cat_1, A_1, D_1 ) end ######## - , 1208 : IsPrecompiledDerivation := true ); + , 1210 : IsPrecompiledDerivation := true ); ## AddJointPairwiseDifferencesOfMorphismsIntoDirectProduct( cat, @@ -4230,7 +4230,7 @@ function ( cat_1, Y_1, morphisms_1 ) end ######## - , 2919 : IsPrecompiledDerivation := true ); + , 2925 : IsPrecompiledDerivation := true ); ## AddMorphismFromSourceToCoequalizerWithGivenCoequalizer( cat, @@ -4247,7 +4247,7 @@ function ( cat_1, Y_1, morphisms_1, P_1 ) end ######## - , 2920 : IsPrecompiledDerivation := true ); + , 2926 : IsPrecompiledDerivation := true ); ## AddMorphismFromSourceToCokernelObject( cat, @@ -4301,7 +4301,7 @@ function ( cat_1, morphisms_1 ) end ######## - , 9162 : IsPrecompiledDerivation := true ); + , 9181 : IsPrecompiledDerivation := true ); ## AddMorphismFromSourceToPushoutWithGivenPushout( cat, @@ -4327,7 +4327,7 @@ function ( cat_1, morphisms_1, P_1 ) end ######## - , 9163 : IsPrecompiledDerivation := true ); + , 9182 : IsPrecompiledDerivation := true ); ## AddMorphismFromTensorProductToInternalCoHom( cat, @@ -4480,8 +4480,8 @@ end function ( cat_1, source_1, list_of_morphisms_1, range_1 ) local deduped_1_1; deduped_1_1 := UnderlyingRing( cat_1 ); - return CreateCapCategoryMorphismWithAttributes( cat_1, source_1, range_1, UnderlyingMatrix, Iterated( List( list_of_morphisms_1, UnderlyingMatrix ), function ( beta_2, alpha_2 ) - return alpha_2 * beta_2; + return CreateCapCategoryMorphismWithAttributes( cat_1, source_1, range_1, UnderlyingMatrix, Iterated( List( list_of_morphisms_1, UnderlyingMatrix ), function ( alpha_2, beta_2 ) + return beta_2 * alpha_2; end, HomalgIdentityMatrix( Dimension( range_1 ), deduped_1_1 ), HomalgIdentityMatrix( Dimension( source_1 ), deduped_1_1 ) ) ); end ######## @@ -4668,7 +4668,7 @@ function ( cat_1, Y_1, morphisms_1 ) end ######## - , 2818 : IsPrecompiledDerivation := true ); + , 2823 : IsPrecompiledDerivation := true ); ## AddProjectionOntoCoequalizerWithGivenCoequalizer( cat, @@ -4685,7 +4685,7 @@ function ( cat_1, Y_1, morphisms_1, P_1 ) end ######## - , 2819 : IsPrecompiledDerivation := true ); + , 2824 : IsPrecompiledDerivation := true ); ## AddProjectiveLift( cat, @@ -4719,7 +4719,7 @@ function ( cat_1, morphisms_1 ) end ######## - , 4331 : IsPrecompiledDerivation := true ); + , 4338 : IsPrecompiledDerivation := true ); ## AddPushoutFunctorial( cat, @@ -4759,7 +4759,7 @@ function ( cat_1, morphisms_1, L_1, morphismsp_1 ) end ######## - , 36252 : IsPrecompiledDerivation := true ); + , 36322 : IsPrecompiledDerivation := true ); ## AddPushoutFunctorialWithGivenPushouts( cat, @@ -4798,7 +4798,7 @@ function ( cat_1, P_1, morphisms_1, L_1, morphismsp_1, Pp_1 ) end ######## - , 27589 : IsPrecompiledDerivation := true ); + , 27645 : IsPrecompiledDerivation := true ); ## AddRankMorphism( cat, @@ -5792,7 +5792,7 @@ function ( cat_1, Y_1, morphisms_1, T_1, tau_1 ) end ######## - , 2919 : IsPrecompiledDerivation := true ); + , 2924 : IsPrecompiledDerivation := true ); ## AddUniversalMorphismFromCoequalizerWithGivenCoequalizer( cat, @@ -5809,7 +5809,7 @@ function ( cat_1, Y_1, morphisms_1, T_1, tau_1, P_1 ) end ######## - , 2920 : IsPrecompiledDerivation := true ); + , 2925 : IsPrecompiledDerivation := true ); ## AddUniversalMorphismFromCoproduct( cat, @@ -5822,7 +5822,7 @@ function ( cat_1, objects_1, T_1, tau_1 ) end ######## - , 503 : IsPrecompiledDerivation := true ); + , 504 : IsPrecompiledDerivation := true ); ## AddUniversalMorphismFromCoproductWithGivenCoproduct( cat, @@ -5835,7 +5835,7 @@ function ( cat_1, objects_1, T_1, tau_1, P_1 ) end ######## - , 504 : IsPrecompiledDerivation := true ); + , 505 : IsPrecompiledDerivation := true ); ## AddUniversalMorphismFromDirectSum( cat, @@ -5934,7 +5934,7 @@ function ( cat_1, morphisms_1, T_1, tau_1 ) end ######## - , 9263 : IsPrecompiledDerivation := true ); + , 9281 : IsPrecompiledDerivation := true ); ## AddUniversalMorphismFromPushoutWithGivenPushout( cat, @@ -5958,7 +5958,7 @@ function ( cat_1, morphisms_1, T_1, tau_1, P_1 ) end ######## - , 9264 : IsPrecompiledDerivation := true ); + , 9282 : IsPrecompiledDerivation := true ); ## AddUniversalMorphismFromZeroObject( cat,