|
# 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( 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 := IsPreAbelianCategory,
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( 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, arg3_1 ), KernelEmbedding( cat_1, arg2_1 ) );
end : CategoryFilter := IsAbelianCategory,
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( 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,
--> --------------------
--> maximum size reached
--> --------------------
[ zur Elbe Produktseite wechseln0.60Quellennavigators
Analyse erneut starten
]
|
