|
# SPDX-License-Identifier: GPL-2.0-or-later
# CAP: Categories, Algorithms, Programming
#
# Implementations
#
###########################
##
## In a terminal category
##
###########################
AddDerivationToCAP( IsLiftable,
"Two morphisms with equal targets are mutually liftable in a terminal category",
[ ],
function( cat, morphism1, morphism2 )
## equality of targets is part of the specification of the input and checked by the pre-function
return true;
end : CategoryFilter := IsTerminalCategory );
###########################
##
## In a finite category
##
###########################
##
AddDerivationToCAP( SetOfMorphismsOfFiniteCategory,
"SetOfMorphismsOfFiniteCategory using SetOfObjectsOfCategory and MorphismsOfExternalHom",
[ [ SetOfObjectsOfCategory, 1 ],
[ MorphismsOfExternalHom, 4 ] ],
function( C )
local objs;
objs := SetOfObjectsOfCategory( C );
## varying the target (column-index) before varying the source ("row"-index)
## in the for-loops below is enforced by SetOfMorphismsOfFiniteCategory for IsCategoryFromNerveData,
## which in turn is enforced by our convention for ProjectionInFactorOfDirectProduct in SkeletalFinSets,
## which is the "double-reverse" convention of the GAP command Cartesian:
# gap> A := FinSet( 3 );
# |3|
# gap> B := FinSet( 4 );
# |4|
# gap> data := List( [ A, B ], AsList );
# [ [ 0 .. 2 ], [ 0 .. 3 ] ]
# gap> pi1 := ProjectionInFactorOfDirectProduct( [ A, B ], 1 );
# |12| → |3|
# gap> pi2 := ProjectionInFactorOfDirectProduct( [ A, B ], 2 );
# |12| → |4|
# gap> List( [ 0 .. 11 ], i -> [ pi1(i), pi2(i) ] );
# [ [ 0, 0 ], [ 1, 0 ], [ 2, 0 ], [ 0, 1 ], [ 1, 1 ], [ 2, 1 ], [ 0, 2 ], [ 1, 2 ], [ 2, 2 ], [ 0, 3 ], [ 1, 3 ], [ 2, 3 ] ]
# gap> List( Cartesian( Reversed( data ) ), Reversed );
# [ [ 0, 0 ], [ 1, 0 ], [ 2, 0 ], [ 0, 1 ], [ 1, 1 ], [ 2, 1 ], [ 0, 2 ], [ 1, 2 ], [ 2, 2 ], [ 0, 3 ], [ 1, 3 ], [ 2, 3 ] ]
# gap> L1 = L2;
# true
# gap> Cartesian( data );
# [ [ 0, 0 ], [ 0, 1 ], [ 0, 2 ], [ 0, 3 ], [ 1, 0 ], [ 1, 1 ], [ 1, 2 ], [ 1, 3 ], [ 2, 0 ], [ 2, 1 ], [ 2, 2 ], [ 2, 3 ] ]
# gap> L1 = L3;
# false
return Concatenation( List( objs, t ->
Concatenation( List( objs, s ->
MorphismsOfExternalHom( C, s, t ) ) ) ) );
end : CategoryFilter := cat -> HasIsFiniteCategory( cat ) and IsFiniteCategory( cat ) );
###########################
##
## WithGiven pairs
##
###########################
AddDerivationToCAP( MorphismFromKernelObjectToSink,
"MorphismFromKernelObjectToSink as zero morphism from kernel object to range",
[ [ KernelObject, 1 ],
[ ZeroMorphism, 1 ] ],
function( cat, alpha )
local K;
K := KernelObject( cat, alpha );
return ZeroMorphism( cat, K, Range( alpha ) );
end );
##
AddDerivationToCAP( KernelLift,
"KernelLift using LiftAlongMonomorphism and KernelEmbedding",
[ [ LiftAlongMonomorphism, 1 ],
[ KernelEmbedding, 1 ] ],
function( cat, mor, test_object, test_morphism )
return LiftAlongMonomorphism( cat, KernelEmbedding( cat, mor ), test_morphism );
end );
##
AddDerivationToCAP( KernelLiftWithGivenKernelObject,
"KernelLift using LiftAlongMonomorphism and KernelEmbedding",
[ [ LiftAlongMonomorphism, 1 ],
[ KernelEmbeddingWithGivenKernelObject, 1 ] ],
function( cat, mor, test_object, test_morphism, kernel )
return LiftAlongMonomorphism( cat, KernelEmbeddingWithGivenKernelObject( cat, mor, kernel ), test_morphism );
end );
##
AddDerivationToCAP( UniversalMorphismIntoDirectSum,
"UniversalMorphismIntoDirectSum using the injections of the direct sum",
[ [ PreCompose, 2 ],
[ InjectionOfCofactorOfDirectSum, 2 ],
[ SumOfMorphisms, 1 ],
[ DirectSum, 1 ] ],
function( cat, diagram, test_object, source )
local nr_components;
nr_components := Length( source );
return SumOfMorphisms( cat,
test_object,
List( [ 1 .. nr_components ], i -> PreCompose( cat, source[ i ], InjectionOfCofactorOfDirectSum( cat, diagram, i ) ) ),
DirectSum( cat, diagram )
);
end : CategoryFilter := IsAdditiveCategory );
##
AddDerivationToCAP( UniversalMorphismIntoDirectSumWithGivenDirectSum,
"UniversalMorphismIntoDirectSum using the injections of the direct sum",
[ [ PreCompose, 2 ],
[ InjectionOfCofactorOfDirectSumWithGivenDirectSum, 2 ],
[ SumOfMorphisms, 1 ] ],
function( cat, diagram, test_object, source, direct_sum )
local nr_components;
nr_components := Length( source );
return SumOfMorphisms( cat,
test_object,
List( [ 1 .. nr_components ], i -> PreCompose( cat, source[ i ], InjectionOfCofactorOfDirectSumWithGivenDirectSum( cat, diagram, i, direct_sum ) ) ),
direct_sum
);
end : CategoryFilter := IsAdditiveCategory );
##
AddDerivationToCAP( ProjectionInFactorOfDirectSum,
"ProjectionInFactorOfDirectSum using UniversalMorphismFromDirectSum",
[ [ IdentityMorphism, 1 ],
[ ZeroMorphism, 2 ],
[ UniversalMorphismFromDirectSum, 1 ] ],
function( cat, list, projection_number )
local id, morphisms;
id := IdentityMorphism( cat, list[projection_number] );
morphisms := List( [ 1 .. Length( list ) ], function( i )
if i = projection_number then
return id;
else
return ZeroMorphism( cat, list[i], list[projection_number] );
fi;
end );
return UniversalMorphismFromDirectSum( cat, list, list[projection_number], morphisms );
end );
##
AddDerivationToCAP( ProjectionInFactorOfDirectSumWithGivenDirectSum,
"ProjectionInFactorOfDirectSum using UniversalMorphismFromDirectSum",
[ [ IdentityMorphism, 1 ],
[ ZeroMorphism, 2 ],
[ UniversalMorphismFromDirectSumWithGivenDirectSum, 1 ] ],
function( cat, list, projection_number, direct_sum_object )
local id, morphisms;
id := IdentityMorphism( cat, list[projection_number] );
morphisms := List( [ 1 .. Length( list ) ], function( i )
if i = projection_number then
return id;
else
return ZeroMorphism( cat, list[i], list[projection_number] );
fi;
end );
return UniversalMorphismFromDirectSumWithGivenDirectSum( cat, list, list[projection_number], morphisms, direct_sum_object );
end );
##
AddDerivationToCAP( UniversalMorphismIntoTerminalObject,
"UniversalMorphismIntoTerminalObject computing the zero morphism",
[ [ TerminalObject, 1 ],
[ ZeroMorphism, 1 ] ],
function( cat, test_source )
local terminal_object;
terminal_object := TerminalObject( cat );
return ZeroMorphism( cat, test_source, terminal_object );
end : CategoryFilter := IsAdditiveCategory );
##
AddDerivationToCAP( UniversalMorphismIntoTerminalObjectWithGivenTerminalObject,
"UniversalMorphismIntoTerminalObject computing the zero morphism",
[ [ ZeroMorphism, 1 ] ],
function( cat, test_source, terminal_object )
return ZeroMorphism( cat, test_source, terminal_object );
end : CategoryFilter := IsAdditiveCategory );
##
AddDerivationToCAP( UniversalMorphismIntoZeroObject,
"UniversalMorphismIntoZeroObject computing the zero morphism",
[ [ ZeroObject, 1 ],
[ ZeroMorphism, 1 ] ],
function( cat, test_source )
local zero_object;
zero_object := ZeroObject( cat );
return ZeroMorphism( cat, test_source, zero_object );
end : CategoryFilter := IsAdditiveCategory );
##
AddDerivationToCAP( UniversalMorphismIntoZeroObjectWithGivenZeroObject,
"UniversalMorphismIntoZeroObject computing the zero morphism",
[ [ ZeroMorphism, 1 ] ],
function( cat, test_source, zero_object )
return ZeroMorphism( cat, test_source, zero_object );
end : CategoryFilter := IsAdditiveCategory );
## FiberProduct from DirectProduct and Equalizer
##
AddDerivationToCAP( FiberProduct,
"FiberProduct as the source of IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram",
[ [ IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram, 1 ] ],
function( cat, diagram )
return Source( IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram( cat, diagram ) );
end );
##
AddDerivationToCAP( ProjectionInFactorOfFiberProduct,
"ProjectionInFactorOfFiberProduct by composing the embedding of equalizer with the direct product projection",
[ [ ProjectionInFactorOfDirectProductWithGivenDirectProduct, 2 ],
[ PreCompose, 3 ],
[ EmbeddingOfEqualizer, 1 ],
[ DirectProduct, 1 ],
[ ComponentOfMorphismIntoDirectProduct, 1 ],
[ IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram, 1 ] ],
function( cat, diagram, projection_number )
local D, direct_product, diagram_of_equalizer, iota;
D := List( diagram, Source );
direct_product := DirectProduct( cat, D );
diagram_of_equalizer := List( [ 1 .. Length( D ) ], i -> PreCompose( cat, ProjectionInFactorOfDirectProductWithGivenDirectProduct( cat, D, i, direct_product ), diagram[i] ) );
iota := EmbeddingOfEqualizer( cat, direct_product, diagram_of_equalizer );
return PreCompose( cat, IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram( cat, diagram ), ComponentOfMorphismIntoDirectProduct( cat, iota, D, projection_number ) );
end );
##
AddDerivationToCAP( UniversalMorphismIntoFiberProduct,
"UniversalMorphismIntoFiberProduct as the universal morphism into equalizer of a univeral morphism into direct product",
[ [ ProjectionInFactorOfDirectProductWithGivenDirectProduct, 2 ],
[ PreCompose, 3 ],
[ UniversalMorphismIntoDirectProduct, 1 ],
[ UniversalMorphismIntoEqualizer, 1 ],
[ DirectProduct, 1 ],
[ IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct, 1 ] ],
function( cat, diagram, test_object, tau )
local D, direct_product, diagram_of_equalizer, chi, psi;
D := List( diagram, Source );
direct_product := DirectProduct( cat, D );
diagram_of_equalizer := List( [ 1 .. Length( D ) ], i -> PreCompose( cat, ProjectionInFactorOfDirectProductWithGivenDirectProduct( cat, D, i, direct_product ), diagram[i] ) );
chi := UniversalMorphismIntoDirectProduct( cat, D, test_object, tau );
psi := UniversalMorphismIntoEqualizer( cat, direct_product, diagram_of_equalizer, test_object, chi );
return PreCompose( cat, psi, IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct( cat, diagram ) );
end );
##
AddDerivationToCAP( MorphismFromFiberProductToSink,
"MorphismFromFiberProductToSink by composing the first projection with the first morphism in the diagram",
[ [ ProjectionInFactorOfFiberProduct, 1 ],
[ PreCompose, 1 ] ],
function( cat, diagram )
local pi_1;
pi_1 := ProjectionInFactorOfFiberProduct( cat, diagram, 1 );
return PreCompose( cat, pi_1, diagram[1] );
end );
##
AddDerivationToCAP( UniversalMorphismIntoZeroObject,
"UniversalMorphismIntoZeroObject using UniversalMorphismIntoTerminalObject",
[ [ UniversalMorphismIntoTerminalObject, 1 ],
[ IsomorphismFromTerminalObjectToZeroObject, 1 ],
[ PreCompose, 1 ] ],
function( cat, obj )
return PreCompose( cat, UniversalMorphismIntoTerminalObject( cat, obj ),
IsomorphismFromTerminalObjectToZeroObject( cat ) );
end );
##
AddDerivationToCAP( ProjectionInFactorOfDirectSum,
"ProjectionInFactorOfDirectSum using ProjectionInFactorOfDirectProduct",
[ [ IsomorphismFromDirectSumToDirectProduct, 1 ],
[ ProjectionInFactorOfDirectProduct, 1 ],
[ PreCompose, 1 ] ],
function( cat, diagram, projection_number )
return PreCompose( cat, IsomorphismFromDirectSumToDirectProduct( cat, diagram ),
ProjectionInFactorOfDirectProduct( cat, diagram, projection_number ) );
end );
##
AddDerivationToCAP( UniversalMorphismIntoDirectSum,
"UniversalMorphismIntoDirectSum using UniversalMorphismIntoDirectProduct",
[ [ UniversalMorphismIntoDirectProduct, 1 ],
[ IsomorphismFromDirectProductToDirectSum, 1 ],
[ PreCompose, 1 ] ],
function( cat, diagram, test_object, source )
return PreCompose( cat, UniversalMorphismIntoDirectProduct( cat, diagram, test_object, source ),
IsomorphismFromDirectProductToDirectSum( cat, diagram ) );
end );
##
AddDerivationToCAP( ComponentOfMorphismIntoDirectSum,
"ComponentOfMorphismIntoDirectSum using ComponentOfMorphismIntoDirectProduct",
[ [ IsomorphismFromDirectSumToDirectProduct, 1 ],
[ ComponentOfMorphismIntoDirectProduct, 1 ],
[ PreCompose, 1 ] ],
function( cat, alpha, summands, nr )
return ComponentOfMorphismIntoDirectProduct( cat,
PreCompose( cat, alpha, IsomorphismFromDirectSumToDirectProduct( cat, summands ) ),
summands,
nr
);
end );
##
AddDerivationToCAP( UniversalMorphismIntoTerminalObject,
"UniversalMorphismFromInitialObject using UniversalMorphismFromZeroObject",
[ [ UniversalMorphismIntoZeroObject, 1 ],
[ IsomorphismFromZeroObjectToTerminalObject, 1 ],
[ PreCompose, 1 ] ],
function( cat, obj )
return PreCompose( cat, UniversalMorphismIntoZeroObject( cat, obj ),
IsomorphismFromZeroObjectToTerminalObject( cat ) );
end );
##
AddDerivationToCAP( ProjectionInFactorOfDirectProduct,
"ProjectionInFactorOfDirectProduct using ProjectionInFactorOfDirectSum",
[ [ IsomorphismFromDirectProductToDirectSum, 1 ],
[ ProjectionInFactorOfDirectSum, 1 ],
[ PreCompose, 1 ] ],
function( cat, diagram, projection_number )
return PreCompose( cat, IsomorphismFromDirectProductToDirectSum( cat, diagram ),
ProjectionInFactorOfDirectSum( cat, diagram, projection_number ) );
end );
##
AddDerivationToCAP( UniversalMorphismIntoDirectProduct,
"UniversalMorphismIntoDirectProduct using UniversalMorphismIntoDirectSum",
[ [ UniversalMorphismIntoDirectSum, 1 ],
[ IsomorphismFromDirectSumToDirectProduct, 1 ],
[ PreCompose, 1 ] ],
function( cat, diagram, test_object, source )
return PreCompose( cat, UniversalMorphismIntoDirectSum( cat, diagram, test_object, source ),
IsomorphismFromDirectSumToDirectProduct( cat, diagram ) );
end );
##
AddDerivationToCAP( ComponentOfMorphismIntoDirectProduct,
"ComponentOfMorphismIntoDirectProduct using ComponentOfMorphismIntoDirectSum",
[ [ IsomorphismFromDirectProductToDirectSum, 1 ],
[ ComponentOfMorphismIntoDirectSum, 1 ],
[ PreCompose, 1 ] ],
function( cat, alpha, factors, nr )
return ComponentOfMorphismIntoDirectSum( cat,
PreCompose( cat, alpha, IsomorphismFromDirectProductToDirectSum( cat, factors ) ),
factors,
nr
);
end );
##
AddDerivationToCAP( UniversalMorphismIntoEqualizer,
"UniversalMorphismIntoEqualizer using the universality of the kernel representation of the equalizer",
[ [ JointPairwiseDifferencesOfMorphismsIntoDirectProduct, 1 ],
[ KernelLift, 1 ],
[ IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer, 1 ],
[ PreCompose, 1 ] ],
function( cat, A, diagram, test_object, tau )
local joint_pairwise_differences, kernel_lift;
joint_pairwise_differences := JointPairwiseDifferencesOfMorphismsIntoDirectProduct( cat, A, diagram );
kernel_lift := KernelLift( cat, joint_pairwise_differences, test_object, tau );
return PreCompose( cat,
kernel_lift,
IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer( cat, A, diagram )
);
end );
##
AddDerivationToCAP( ImageEmbedding,
"ImageEmbedding as the kernel embedding of the cokernel projection",
[ [ CokernelProjection, 1 ],
[ KernelEmbedding, 1 ],
[ IsomorphismFromImageObjectToKernelOfCokernel, 1 ],
[ PreCompose, 1 ] ],
function( cat, mor )
local image_embedding;
image_embedding := KernelEmbedding( cat, CokernelProjection( cat, mor ) );
return PreCompose( cat, IsomorphismFromImageObjectToKernelOfCokernel( cat, mor ),
image_embedding );
end : CategoryFilter := IsPreAbelianCategory );
##
AddDerivationToCAP( CoastrictionToImage,
"CoastrictionToImage using that image embedding can be seen as a kernel",
[ [ ImageEmbedding, 1 ],
[ LiftAlongMonomorphism, 1 ] ],
function( cat, morphism )
local image_embedding;
image_embedding := ImageEmbedding( cat, morphism );
return LiftAlongMonomorphism( cat, image_embedding, morphism );
end );
##
AddDerivationToCAP( CoastrictionToImageWithGivenImageObject,
"CoastrictionToImage using that image embedding can be seen as a kernel",
[ [ ImageEmbeddingWithGivenImageObject, 1 ],
[ LiftAlongMonomorphism, 1 ] ],
function( cat, morphism, image )
local image_embedding;
image_embedding := ImageEmbeddingWithGivenImageObject( cat, morphism, image );
return LiftAlongMonomorphism( cat, image_embedding, morphism );
end );
##
AddDerivationToCAP( UniversalMorphismFromImage,
"UniversalMorphismFromImage using ImageEmbedding and LiftAlongMonomorphism",
[ [ ImageEmbedding, 1 ],
[ LiftAlongMonomorphism, 1 ] ],
function( cat, morphism, test_factorization )
local image_embedding;
image_embedding := ImageEmbedding( cat, morphism );
return LiftAlongMonomorphism( cat, test_factorization[2], image_embedding );
end );
##
AddDerivationToCAP( UniversalMorphismFromImageWithGivenImageObject,
"UniversalMorphismFromImageWithGivenImageObject using ImageEmbeddingWithGivenImageObject and LiftAlongMonomorphism",
[ [ ImageEmbeddingWithGivenImageObject, 1 ],
[ LiftAlongMonomorphism, 1 ] ],
function( cat, morphism, test_factorization, image )
local image_embedding;
image_embedding := ImageEmbeddingWithGivenImageObject( cat, morphism, image );
return LiftAlongMonomorphism( cat, test_factorization[2], image_embedding );
end );
##
AddDerivationToCAP( UniversalMorphismIntoEqualizer,
"UniversalMorphismIntoEqualizer using LiftAlongMonomorphism and EmbeddingOfEqualizer",
[ [ LiftAlongMonomorphism, 1 ],
[ EmbeddingOfEqualizer, 1 ] ],
function( cat, A, diagram, test_object, test_morphism )
return LiftAlongMonomorphism( cat, EmbeddingOfEqualizer( cat, A, diagram ), test_morphism );
end );
##
AddDerivationToCAP( UniversalMorphismIntoEqualizerWithGivenEqualizer,
"UniversalMorphismIntoEqualizer using LiftAlongMonomorphism and EmbeddingOfEqualizer",
[ [ LiftAlongMonomorphism, 1 ],
[ EmbeddingOfEqualizerWithGivenEqualizer, 1 ] ],
function( cat, A, diagram, test_object, test_morphism, equalizer )
return LiftAlongMonomorphism( cat, EmbeddingOfEqualizerWithGivenEqualizer( cat, A, diagram, equalizer ), test_morphism );
end );
##
AddDerivationToCAP( MorphismFromEqualizerToSink,
"MorphismFromEqualizerToSink by composing the embedding with the first morphism in the diagram",
[ [ EmbeddingOfEqualizer, 1 ],
[ PreCompose, 1 ] ],
function( cat, A, diagram )
local iota;
iota := EmbeddingOfEqualizer( cat, A, diagram );
return PreCompose( cat, iota, diagram[1] );
end );
##
AddDerivationToCAP( ImageObjectFunctorialWithGivenImageObjects,
"ImageObjectFunctorialWithGivenImageObjects using the universality",
[ [ LiftAlongMonomorphism, 1 ],
[ ImageEmbeddingWithGivenImageObject, 2 ],
[ PreCompose, 1 ] ],
function( cat, I, alpha, nu, alphap, Ip )
return LiftAlongMonomorphism( cat,
ImageEmbeddingWithGivenImageObject( cat, alphap, Ip ),
PreCompose( cat, ImageEmbeddingWithGivenImageObject( cat, alpha, I ), nu ) );
end );
##
AddDerivationToCAP( ProjectiveCoverObject,
"ProjectiveCoverObject as the source of EpimorphismFromProjectiveCoverObject",
[ [ EpimorphismFromProjectiveCoverObject, 1 ] ],
function( cat, obj )
return Source( EpimorphismFromProjectiveCoverObject( cat, obj ) );
end );
###########################
##
## Methods returning a boolean
##
###########################
##
AddDerivationToCAP( IsEqualForObjects,
"skeletality",
[ [ IsIsomorphicForObjects, 1 ] ],
function( cat, object_1, object_2 )
return IsIsomorphicForObjects( cat, object_1, object_2 );
end : CategoryFilter := IsSkeletalCategory );
##
AddDerivationToCAP( IsIsomorphicForObjects,
"skeletality",
[ [ IsEqualForObjects, 1 ] ],
function( cat, object_1, object_2 )
return IsEqualForObjects( cat, object_1, object_2 );
end : CategoryFilter := IsSkeletalCategory );
##
AddDerivationToCAP( IsBijectiveObject,
"IsBijectiveObject by checking if the object is both projective and injective",
[ [ IsProjective, 1 ],
[ IsInjective, 1 ] ],
function( cat, object )
return IsProjective( cat, object ) and IsInjective( cat, object );
end );
##
AddDerivationToCAP( IsProjective,
"IsProjective by checking if the object is a retract of some projective object",
[ [ EpimorphismFromSomeProjectiveObject, 1 ],
[ IsSplitEpimorphism, 1 ] ],
function( cat, object )
return IsSplitEpimorphism( cat, EpimorphismFromSomeProjectiveObject( cat, object ) );
end );
##
AddDerivationToCAP( IsOne,
"IsOne by comparing with the identity morphism",
[ [ IdentityMorphism, 1 ],
[ IsCongruentForMorphisms, 1 ] ],
function( cat, morphism )
local object;
object := Source( morphism );
return IsCongruentForMorphisms( cat, IdentityMorphism( cat, object ), morphism );
end );
##
AddDerivationToCAP( IsEndomorphism,
"IsEndomorphism by deciding whether source and range are equal as objects",
[ [ IsEqualForObjects, 1 ] ],
function( cat, morphism )
return IsEqualForObjects( cat, Source( morphism ), Range( morphism ) );
end );
##
AddDerivationToCAP( IsAutomorphism,
"IsAutomorphism by checking IsEndomorphism and IsIsomorphism",
[ [ IsEndomorphism, 1 ],
[ IsIsomorphism, 1 ] ],
function( cat, morphism )
return IsEndomorphism( cat, morphism ) and IsIsomorphism( cat, morphism );
end );
##
AddDerivationToCAP( IsZeroForMorphisms,
"IsZeroForMorphisms by deciding whether the given morphism is congruent to the zero morphism",
[ [ ZeroMorphism, 1 ],
[ IsCongruentForMorphisms, 1 ] ],
function( cat, morphism )
local zero_morphism;
zero_morphism := ZeroMorphism( cat, Source( morphism ), Range( morphism ) );
return IsCongruentForMorphisms( cat, zero_morphism, morphism );
end );
##
AddDerivationToCAP( IsEqualToIdentityMorphism,
"IsEqualToIdentityMorphism using IsEqualForMorphismsOnMor and IdentityMorphism",
[ [ IsEqualForMorphismsOnMor, 1 ],
[ IdentityMorphism, 1 ] ],
function( cat, morphism )
return IsEqualForMorphismsOnMor( cat, morphism, IdentityMorphism( cat, Source( morphism ) ) );
end );
##
AddDerivationToCAP( IsEqualToZeroMorphism,
"IsEqualToZeroMorphism using IsEqualForMorphisms and ZeroMorphism",
[ [ IsEqualForMorphisms, 1 ],
[ ZeroMorphism, 1 ] ],
function( cat, morphism )
return IsEqualForMorphisms( cat, morphism, ZeroMorphism( cat, Source( morphism ), Range( morphism ) ) );
end );
##
AddDerivationToCAP( IsZeroForObjects,
"IsZeroForObjects by comparing identity morphism with zero morphism",
[ [ IsCongruentForMorphisms, 1 ],
[ IdentityMorphism, 1 ],
[ ZeroMorphism, 1 ] ],
function( cat, object )
return IsCongruentForMorphisms( cat, IdentityMorphism( cat, object ), ZeroMorphism( cat, object, object ) );
end );
##
AddDerivationToCAP( IsTerminal,
"IsTerminal using IsZeroForObjects",
[ [ IsZeroForObjects, 1 ] ],
function( cat, object )
return IsZeroForObjects( cat, object );
end : CategoryFilter := IsAdditiveCategory ); #Ab-Category?
##
AddDerivationToCAP( IsTerminal,
"IsTerminal using IsIsomorphism( cat, UniversalMorphismIntoTerminalObject )",
[ [ IsIsomorphism, 1 ],
[ UniversalMorphismIntoTerminalObject, 1 ] ],
function( cat, object )
return IsIsomorphism( cat, UniversalMorphismIntoTerminalObject( cat, object ) );
end );
##
AddDerivationToCAP( IsWellDefinedForMorphismsWithGivenSourceAndRange,
"checking that source and range coincide with the given ones and then checking well-definedness as usual",
[ [ IsEqualForObjects, 2 ],
[ IsWellDefinedForMorphisms, 1 ] ],
function( cat, source, morphism, range )
# Mathematically, we would first like to check if `morphism` has the expected source and range.
# However, `IsEqualForObjects` expects well-defined objects, so we first have to check if source and range
# of `morphism` are well-defined. We do this via `IsWellDefinedForMorphisms`, which checks well-definedness of
# source and range via a redirect function.
return IsWellDefinedForMorphisms( cat, morphism ) and
IsEqualForObjects( cat, Source( morphism ), source ) and
IsEqualForObjects( cat, Range( morphism ), range );
end );
##
AddDerivationToCAP( IsEqualForMorphismsOnMor,
"IsEqualForMorphismsOnMor using IsEqualForMorphisms",
[ [ IsEqualForMorphisms, 1 ],
[ IsEqualForObjects, 2 ] ],
function( cat, morphism_1, morphism_2 )
local value_1, value_2;
value_1 := IsEqualForObjects( cat, Source( morphism_1 ), Source( morphism_2 ) );
value_2 := IsEqualForObjects( cat, Range( morphism_1 ), Range( morphism_2 ) );
if value_1 and value_2 then
return IsEqualForMorphisms( cat, morphism_1, morphism_2 );
else
return false;
fi;
end );
##
AddDerivationToCAP( IsIdempotent,
"IsIdempotent by comparing the square of the morphism with itself",
[ [ IsCongruentForMorphisms, 1 ],
[ PreCompose, 1 ] ],
function( cat, morphism )
return IsCongruentForMorphisms( cat, PreCompose( cat, morphism, morphism ), morphism );
end );
##
AddDerivationToCAP( IsMonomorphism,
"IsMonomorphism by deciding if the kernel is a zero object",
[ [ IsZeroForObjects, 1 ],
[ KernelObject, 1 ] ],
function( cat, morphism )
return IsZeroForObjects( cat, KernelObject( cat, morphism ) );
end : CategoryFilter := IsAdditiveCategory );
##
AddDerivationToCAP( IsMonomorphism,
"IsMonomorphism by deciding if the diagonal morphism is an isomorphism",
[ [ IsIsomorphism, 1 ],
[ IdentityMorphism, 1 ],
[ UniversalMorphismIntoFiberProduct, 1 ] ],
function( cat, morphism )
local pullback_diagram, pullback_projection_1, pullback_projection_2, identity, diagonal_morphism;
pullback_diagram := [ morphism, morphism ];
identity := IdentityMorphism( cat, Source( morphism ) );
diagonal_morphism := UniversalMorphismIntoFiberProduct( cat, pullback_diagram, Source( morphism ), [ identity, identity ] );
return IsIsomorphism( cat, diagonal_morphism );
end );
##
AddDerivationToCAP( IsIsomorphism,
"IsIsomorphism by deciding if it is a mono and an epi",
[ [ IsMonomorphism, 1 ],
[ IsEpimorphism, 1 ] ],
function( cat, morphism )
return IsMonomorphism( cat, morphism ) and IsEpimorphism( cat, morphism );
end : CategoryFilter := IsAbelianCategory );
##
AddDerivationToCAP( IsIsomorphism,
"IsIsomorphism by deciding if it is a split mono and a split epi",
[ [ IsSplitMonomorphism, 1 ],
[ IsSplitEpimorphism, 1 ] ],
function( cat, morphism )
return IsSplitMonomorphism( cat, morphism ) and IsSplitEpimorphism( cat, morphism );
end );
##
AddDerivationToCAP( IsIsomorphism,
"IsIsomorphism by deciding if it is a split mono and an epi",
[ [ IsSplitMonomorphism, 1 ],
[ IsEpimorphism, 1 ] ],
function( cat, morphism )
return IsSplitMonomorphism( cat, morphism ) and IsEpimorphism( cat, morphism );
end );
##
AddDerivationToCAP( IsSplitMonomorphism,
"IsSplitMonomorphism by using IsColiftable",
[ [ IsColiftable, 1 ],
[ IdentityMorphism, 1 ] ],
function( cat, morphism )
return IsColiftable( cat, morphism, IdentityMorphism( cat, Source( morphism ) ) );
end );
##
AddDerivationToCAP( IsEqualAsSubobjects,
"IsEqualAsSubobjects(sub1, sub2) if sub1 dominates sub2 and vice versa",
[ [ IsDominating, 2 ] ],
function( cat, sub1, sub2 )
return IsDominating( cat, sub1, sub2 ) and IsDominating( cat, sub2, sub1 );
end );
##
AddDerivationToCAP( IsDominating,
"IsDominating using IsLiftableAlongMonomorphism",
[ [ IsLiftableAlongMonomorphism, 1 ] ],
function( cat, sub1, sub2 )
return IsLiftableAlongMonomorphism( cat, sub2, sub1 );
end );
##
AddDerivationToCAP( IsDominating,
"IsDominating using IsCodominating and duality by cokernel",
[ [ CokernelProjection, 2 ],
[ IsCodominating, 1 ] ],
function( cat, sub1, sub2 )
local cokernel_projection_1, cokernel_projection_2;
cokernel_projection_1 := CokernelProjection( cat, sub1 );
cokernel_projection_2 := CokernelProjection( cat, sub2 );
return IsCodominating( cat, cokernel_projection_2, cokernel_projection_1 );
end : CategoryFilter := IsAbelianCategory );
##
AddDerivationToCAP( IsDominating,
"IsDominating(sub1, sub2) by deciding if sub1 composed with CokernelProjection(cat, sub2) is zero",
[ [ CokernelProjection, 1 ],
[ PreCompose, 1 ],
[ IsZeroForMorphisms, 1 ] ],
function( cat, sub1, sub2 )
local cokernel_projection, composition;
cokernel_projection := CokernelProjection( cat, sub2 );
composition := PreCompose( cat, sub1, cokernel_projection );
return IsZeroForMorphisms( cat, composition );
end );
##
AddDerivationToCAP( IsLiftableAlongMonomorphism,
"IsLiftableAlongMonomorphism using IsLiftable",
[ [ IsLiftable, 1 ] ],
function( cat, iota, tau )
return IsLiftable( cat, tau, iota );
end );
##
AddDerivationToCAP( IsProjective,
"",
[ [ EpimorphismFromProjectiveCoverObject, 1 ],
[ IsIsomorphism, 1 ] ],
function( cat, alpha )
return IsIsomorphism( cat, EpimorphismFromProjectiveCoverObject( cat, alpha ) );
end );
###########################
##
## Methods returning a morphism where the source and range can directly be read of from the input
##
###########################
##
AddDerivationToCAP( SomeIsomorphismBetweenObjects,
"skeletality",
[ [ IdentityMorphism, 1 ] ],
function( cat, object_1, object_2 )
return IdentityMorphism( cat, object_1 );
end : CategoryFilter := IsSkeletalCategory );
##
AddDerivationToCAP( ZeroMorphism,
"Zero morphism by composition of morphism into and from zero object",
[ [ PreCompose, 1 ],
[ UniversalMorphismIntoZeroObject, 1 ],
[ UniversalMorphismFromZeroObject, 1 ] ],
function( cat, obj_source, obj_range )
return PreCompose( cat, UniversalMorphismIntoZeroObject( cat, obj_source ), UniversalMorphismFromZeroObject( cat, obj_range ) );
end : CategoryFilter := IsAdditiveCategory );
##
AddDerivationToCAP( ZeroMorphism,
"computing the empty sum of morphisms",
[ [ SumOfMorphisms, 1 ] ],
function( cat, obj_source, obj_range )
return SumOfMorphisms( cat, obj_source, [ ], obj_range );
end : CategoryFilter := IsAbCategory );
##
AddDerivationToCAP( PreCompose,
"PreCompose using PostCompose and swapping arguments",
[ [ PostCompose, 1 ] ],
function( cat, pre_mor, post_mor )
return PostCompose( cat, post_mor, pre_mor );
end );
##
AddDerivationToCAP( PreCompose,
"PreCompose by wrapping the arguments in a list",
[ [ PreComposeList, 1 ] ],
function( cat, pre_mor, post_mor )
return PreComposeList( cat, Source( pre_mor ), [ pre_mor, post_mor ], Range( post_mor ) );
end );
##
AddDerivationToCAP( PreComposeList,
"PreComposeList by iterating PreCompose",
[ [ IdentityMorphism, 2 ],
[ PreCompose, 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, { alpha, beta } -> PreCompose( cat, alpha, beta ), id_source, id_range );
end );
##
AddDerivationToCAP( InverseForMorphisms,
"InverseForMorphisms using LiftAlongMonomorphism of an identity morphism",
[ [ IdentityMorphism, 1 ],
[ LiftAlongMonomorphism, 1 ] ],
function( cat, mor )
local identity_of_range;
identity_of_range := IdentityMorphism( cat, Range( mor ) );
return LiftAlongMonomorphism( cat, mor, identity_of_range );
end );
##
AddDerivationToCAP( PreInverseForMorphisms,
"PreInverseForMorphisms using IdentityMorphism and Lift",
[ [ IdentityMorphism, 1 ],
[ Lift, 1 ] ],
function( cat, mor )
return Lift( cat, IdentityMorphism( cat, Range( mor ) ), mor );
end );
##
AddDerivationToCAP( AdditionForMorphisms,
"AdditionForMorphisms using SumOfMorphisms",
[ [ SumOfMorphisms, 1 ] ],
function( cat, mor1, mor2 )
return SumOfMorphisms( cat, Source( mor1 ), [ mor1, mor2 ], Range( mor1 ) );
end : CategoryFilter := IsAbCategory );
##
AddDerivationToCAP( AdditionForMorphisms,
"AdditionForMorphisms(mor1, mor2) as the composition of (mor1,mor2) with the codiagonal morphism",
[ [ UniversalMorphismIntoDirectSum, 1 ],
[ IdentityMorphism, 1 ],
[ UniversalMorphismFromDirectSum, 1 ],
[ PreCompose, 1 ] ],
function( cat, mor1, mor2 )
local return_value, B, identity_morphism_B, componentwise_morphism, addition_morphism;
B := Range( mor1 );
componentwise_morphism := UniversalMorphismIntoDirectSum( cat, [ B, B ], Source( mor1 ), [ mor1, mor2 ] );
identity_morphism_B := IdentityMorphism( cat, B );
addition_morphism := UniversalMorphismFromDirectSum( cat, [ B, B ], B, [ identity_morphism_B, identity_morphism_B ] );
return PreCompose( cat, componentwise_morphism, addition_morphism );
end : CategoryFilter := IsAdditiveCategory );
##
AddDerivationToCAP( SubtractionForMorphisms,
"SubtractionForMorphisms(mor1, mor2) as the sum of mor1 and the additive inverse of mor2",
[ [ AdditionForMorphisms, 1 ],
[ AdditiveInverseForMorphisms, 1 ] ],
function( cat, mor1, mor2 )
return AdditionForMorphisms( cat, mor1, AdditiveInverseForMorphisms( cat, mor2 ) );
end : CategoryFilter := IsAbCategory );
##
AddDerivationToCAP( SumOfMorphisms,
"SumOfMorphisms using AdditionForMorphisms and ZeroMorphism",
[ [ AdditionForMorphisms, 2 ],
[ ZeroMorphism, 1 ] ],
function( cat, obj1, mors, obj2 )
local zero_morphism;
zero_morphism := ZeroMorphism( cat, obj1, obj2 );
return Iterated( mors, { alpha, beta } -> AdditionForMorphisms( cat, alpha, beta ), zero_morphism );
end : CategoryFilter := IsAbCategory );
##
AddDerivationToCAP( LinearCombinationOfMorphisms,
"LinearCombinationOfMorphisms using SumOfMorphisms and MultiplyWithElementOfCommutativeRingForMorphisms",
[ [ MultiplyWithElementOfCommutativeRingForMorphisms, 2 ],
[ SumOfMorphisms, 1 ] ],
function( cat, obj1, coeffs, mors, obj2 )
local morphisms;
morphisms := ListN( coeffs, mors, { r, alpha } -> MultiplyWithElementOfCommutativeRingForMorphisms( cat, r, alpha ) );
return SumOfMorphisms( cat, obj1, morphisms, obj2 );
end : CategoryFilter := IsLinearCategoryOverCommutativeRing );
##
AddDerivationToCAP( LiftAlongMonomorphism,
"LiftAlongMonomorphism using Lift",
[ [ Lift, 1 ] ],
function( cat, alpha, beta )
## Caution with the order of the arguments!
return Lift( cat, beta, alpha );
end );
##
AddDerivationToCAP( ProjectiveLift,
"ProjectiveLift using Lift",
[ [ Lift, 1 ] ],
function( cat, alpha, beta )
return Lift( cat, alpha, beta );
end );
##
AddDerivationToCAP( RandomMorphismByInteger,
"RandomMorphismByInteger using RandomObjectByInteger and RandomMorphismWithFixedSourceByInteger",
[ [ RandomObjectByInteger, 1 ],
[ RandomMorphismWithFixedSourceByInteger, 1 ] ],
function( cat, n )
return RandomMorphismWithFixedSourceByInteger( cat, RandomObjectByInteger( cat, n ), 1 + Log2Int( n ) );
end );
##
AddDerivationToCAP( RandomMorphismByInteger,
"RandomMorphismByInteger using RandomObjectByInteger and RandomMorphismWithFixedRangeByInteger",
[ [ RandomObjectByInteger, 1 ],
[ RandomMorphismWithFixedRangeByInteger, 1 ] ],
function( cat, n )
return RandomMorphismWithFixedRangeByInteger( cat, RandomObjectByInteger( cat, n ), 1 + Log2Int( n ) );
end );
##
AddDerivationToCAP( RandomMorphismWithFixedSourceByInteger,
"RandomMorphismWithFixedSourceByInteger using RandomObjectByInteger and RandomMorphismWithFixedSourceAndRangeByInteger",
[ [ RandomObjectByInteger, 1 ],
[ RandomMorphismWithFixedSourceAndRangeByInteger, 1 ] ],
function( cat, S, n )
return RandomMorphismWithFixedSourceAndRangeByInteger( cat, S, RandomObjectByInteger( cat, n ), 1 + Log2Int( n ) );
end : CategoryFilter := IsAbCategory );
##
AddDerivationToCAP( RandomMorphismWithFixedRangeByInteger,
"RandomMorphismWithFixedRangeByInteger using RandomObjectByInteger and RandomMorphismWithFixedSourceAndRangeByInteger",
[ [ RandomObjectByInteger, 1 ],
[ RandomMorphismWithFixedSourceAndRangeByInteger, 1 ] ],
function( cat, R, n )
return RandomMorphismWithFixedSourceAndRangeByInteger( cat, RandomObjectByInteger( cat, n ), R, 1 + Log2Int( n ) );
end : CategoryFilter := IsAbCategory );
##
AddDerivationToCAP( RandomMorphismByInteger,
"RandomMorphismByInteger using RandomObjectByInteger and RandomMorphismWithFixedSourceAndRangeByInteger",
[ [ RandomObjectByInteger, 2 ],
[ RandomMorphismWithFixedSourceAndRangeByInteger, 1 ] ],
function( cat, n )
return RandomMorphismWithFixedSourceAndRangeByInteger( cat, RandomObjectByInteger( cat, n ), RandomObjectByInteger( cat, n ), 1 + Log2Int( n ) );
end : CategoryFilter := IsAbCategory );
##
AddDerivationToCAP( RandomMorphismByList,
"RandomMorphismByList using RandomObjectByList and RandomMorphismWithFixedSourceByList",
[ [ RandomObjectByList, 1 ],
[ RandomMorphismWithFixedSourceByList, 1 ] ],
function( cat, L )
if Length( L ) <> 2 or not ForAll( L, IsList ) then
Error( "the list passed to 'RandomMorphismByList' in ", Name( cat ), " must be a list consisting of two lists!\n" );
fi;
return RandomMorphismWithFixedSourceByList( cat, RandomObjectByList( cat, L[1] ), L[2] );
end );
##
AddDerivationToCAP( RandomMorphismByList,
"RandomMorphismByList using RandomObjectByList and RandomMorphismWithFixedRangeByList",
[ [ RandomObjectByList, 1 ],
[ RandomMorphismWithFixedRangeByList, 1 ] ],
function( cat, L )
if Length( L ) <> 2 or not ForAll( L, IsList ) then
Error( "the list passed to 'RandomMorphismByList' in ", Name( cat ), " must be a list consisting of two lists!\n" );
fi;
return RandomMorphismWithFixedRangeByList( cat, RandomObjectByList( cat, L[1] ), L[2] );
end );
##
AddDerivationToCAP( RandomMorphismWithFixedSourceByList,
"RandomMorphismWithFixedSourceByList using RandomObjectByList and RandomMorphismWithFixedSourceAndRangeByList",
[ [ RandomObjectByList, 1 ],
[ RandomMorphismWithFixedSourceAndRangeByList, 1 ] ],
function( cat, S, L )
if Length( L ) <> 2 or not ForAll( L, IsList ) then
Error( "the list passed to 'RandomMorphismWithFixedSourceByList' in ", Name( cat ), " must be a list consisting of two lists!\n" );
fi;
return RandomMorphismWithFixedSourceAndRangeByList( cat, S, RandomObjectByList( cat, L[1] ), L[2] );
end : CategoryFilter := IsAbCategory );
##
AddDerivationToCAP( RandomMorphismWithFixedRangeByList,
"RandomMorphismWithFixedRangeByList using RandomObjectByList and RandomMorphismWithFixedSourceAndRangeByList",
[ [ RandomObjectByList, 1 ],
[ RandomMorphismWithFixedSourceAndRangeByList, 1 ] ],
function( cat, R, L )
if Length( L ) <> 2 or not ForAll( L, IsList ) then
Error( "the list passed to 'RandomMorphismWithFixedRangeByList' in ", Name( cat ), " must be a list consisting of two lists!\n" );
fi;
return RandomMorphismWithFixedSourceAndRangeByList( cat, RandomObjectByList( cat, L[1] ), R, L[2] );
end : CategoryFilter := IsAbCategory );
##
AddDerivationToCAP( RandomMorphismByList,
"RandomMorphismByList using RandomObjectByList and RandomMorphismWithFixedSourceAndRangeByList",
[ [ RandomObjectByList, 2 ],
[ RandomMorphismWithFixedSourceAndRangeByList, 1 ] ],
function( cat, L )
if Length( L ) <> 3 or not ForAll( L, IsList ) then
Error( "the list passed to 'RandomMorphismByList' in ", Name( cat ), " must be a list consisting of three lists!\n" );
fi;
return RandomMorphismWithFixedSourceAndRangeByList( cat, RandomObjectByList( cat, L[1] ), RandomObjectByList( cat, L[2] ), L[3] );
end : CategoryFilter := IsAbCategory );
##
AddDerivationToCAP( IsomorphismFromKernelOfCokernelToImageObject,
"IsomorphismFromKernelOfCokernelToImageObject as the inverse of IsomorphismFromImageObjectToKernelOfCokernel",
[ [ InverseForMorphisms, 1 ],
[ IsomorphismFromImageObjectToKernelOfCokernel, 1 ] ],
function( cat, morphism )
return InverseForMorphisms( cat, IsomorphismFromImageObjectToKernelOfCokernel( cat, morphism ) );
end );
##
AddDerivationToCAP( IsomorphismFromImageObjectToKernelOfCokernel,
"IsomorphismFromImageObjectToKernelOfCokernel as the inverse of IsomorphismFromKernelOfCokernelToImageObject",
[ [ InverseForMorphisms, 1 ],
[ IsomorphismFromKernelOfCokernelToImageObject, 1 ] ],
function( cat, morphism )
return InverseForMorphisms( cat, IsomorphismFromKernelOfCokernelToImageObject( cat, morphism ) );
end );
##
AddDerivationToCAP( IsomorphismFromImageObjectToKernelOfCokernel,
"IsomorphismFromImageObjectToKernelOfCokernel using the universal property of the image",
[ [ 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, Pair( morphism_to_kernel, kernel_emb ) );
end : CategoryFilter := IsAbelianCategory );
##
AddDerivationToCAP( IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct,
"IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct using the universal property of the kernel",
[ [ JointPairwiseDifferencesOfMorphismsIntoDirectProduct, 1 ],
[ Equalizer, 1 ],
[ EmbeddingOfEqualizerWithGivenEqualizer, 1 ],
[ KernelLift, 1 ] ],
function( cat, A, diagram )
local joint_pairwise_differences, equalizer, equalizer_embedding;
joint_pairwise_differences := JointPairwiseDifferencesOfMorphismsIntoDirectProduct( cat, A, diagram );
equalizer := Equalizer( cat, A, diagram );
equalizer_embedding := EmbeddingOfEqualizerWithGivenEqualizer( cat, A, diagram, equalizer );
return KernelLift( cat, joint_pairwise_differences, equalizer, equalizer_embedding );
end );
##
AddDerivationToCAP( IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer,
"IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer using the universal property of the equalizer",
[ [ JointPairwiseDifferencesOfMorphismsIntoDirectProduct, 1 ],
[ KernelObject, 1 ],
[ KernelEmbeddingWithGivenKernelObject, 1 ],
[ UniversalMorphismIntoEqualizer, 1 ] ],
function( cat, A, diagram )
local joint_pairwise_differences, kernel_object, kernel_embedding;
joint_pairwise_differences := JointPairwiseDifferencesOfMorphismsIntoDirectProduct( cat, A, diagram );
kernel_object := KernelObject( cat, joint_pairwise_differences );
kernel_embedding := KernelEmbeddingWithGivenKernelObject( cat, joint_pairwise_differences, kernel_object );
return UniversalMorphismIntoEqualizer( cat, A, diagram, kernel_object, kernel_embedding );
end );
##
AddDerivationToCAP( IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram,
"IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram using the universal property of the equalizer",
[ [ DirectProduct, 1 ],
[ PreCompose, 2 ],
[ ProjectionInFactorOfDirectProductWithGivenDirectProduct, 2 ],
[ ProjectionInFactorOfFiberProductWithGivenFiberProduct, 2 ],
[ UniversalMorphismIntoDirectProductWithGivenDirectProduct, 1 ],
[ FiberProduct, 1 ],
[ UniversalMorphismIntoEqualizer, 1 ] ],
function( cat, diagram )
local sources_of_diagram, direct_product, direct_product_diagram, fiber_product, test_source, fiber_product_embedding;
sources_of_diagram := List( diagram, Source );
direct_product := DirectProduct( cat, sources_of_diagram );
direct_product_diagram := List( [ 1.. Length( sources_of_diagram ) ],
i -> PreCompose( cat, ProjectionInFactorOfDirectProductWithGivenDirectProduct( cat, sources_of_diagram, i, direct_product ), diagram[ i ] ) );
fiber_product := FiberProduct( cat, diagram );
test_source := List( [ 1 .. Length( diagram ) ], i -> ProjectionInFactorOfFiberProductWithGivenFiberProduct( cat, diagram, i, fiber_product ) );
fiber_product_embedding := UniversalMorphismIntoDirectProductWithGivenDirectProduct( cat, sources_of_diagram, fiber_product, test_source, direct_product );
return UniversalMorphismIntoEqualizer( cat, direct_product, direct_product_diagram, fiber_product, fiber_product_embedding );
end );
##
AddDerivationToCAP( IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram,
"IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram as the inverse of IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct",
[ [ IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct, 1 ],
[ InverseForMorphisms, 1 ] ],
function( cat, diagram )
return InverseForMorphisms( cat, IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct( cat, diagram ) );
end );
##
AddDerivationToCAP( IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct,
"IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct using the universal property of the fiber product",
[ [ PreCompose, 4 ],
[ ProjectionInFactorOfDirectProductWithGivenDirectProduct, 2 ],
[ DirectProduct, 1 ],
[ Equalizer, 1 ],
[ EmbeddingOfEqualizerWithGivenEqualizer, 1 ],
[ UniversalMorphismIntoFiberProduct, 1 ] ],
function( cat, diagram )
local sources_of_diagram, direct_product, direct_product_diagram, equalizer, equalizer_embedding, equalizer_of_direct_product_diagram;
sources_of_diagram := List( diagram, Source );
direct_product := DirectProduct( cat, sources_of_diagram );
direct_product_diagram := List( [ 1.. Length( sources_of_diagram ) ],
i -> PreCompose( cat, ProjectionInFactorOfDirectProductWithGivenDirectProduct( cat, sources_of_diagram, i, direct_product ), diagram[ i ] ) );
equalizer := Equalizer( cat, direct_product, direct_product_diagram );
equalizer_embedding := EmbeddingOfEqualizerWithGivenEqualizer( cat, direct_product, direct_product_diagram, equalizer );
equalizer_of_direct_product_diagram := List( [ 1 .. Length( direct_product_diagram ) ], i -> PreCompose( cat, equalizer_embedding, direct_product_diagram[ i ] ) );
return UniversalMorphismIntoFiberProduct( cat, diagram, equalizer, equalizer_of_direct_product_diagram );
end );
##
AddDerivationToCAP( IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct,
"IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct as the inverse of IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram",
[ [ IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram, 1 ],
[ InverseForMorphisms, 1 ] ],
function( cat, diagram )
return InverseForMorphisms( cat, IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram( cat, diagram ) );
end );
##
AddDerivationToCAP( LiftAlongMonomorphism,
"LiftAlongMonomorphism by inverting the kernel lift from the source to the kernel of the cokernel of a given monomorphism",
[ [ CokernelProjection, 1 ],
[ KernelLift, 2 ],
[ PreCompose, 1 ],
[ InverseForMorphisms, 1 ] ],
function( cat, monomorphism, test_morphism )
local cokernel_proj, kernel_lift_from_source_of_monomorphism, kernel_lift_from_source_of_test_morphism;
cokernel_proj := CokernelProjection( cat, monomorphism );
kernel_lift_from_source_of_monomorphism :=
KernelLift( cat, cokernel_proj, Source( monomorphism ), monomorphism );
kernel_lift_from_source_of_test_morphism :=
KernelLift( cat, cokernel_proj, Source( test_morphism ), test_morphism );
return PreCompose( cat, kernel_lift_from_source_of_test_morphism, InverseForMorphisms( cat, kernel_lift_from_source_of_monomorphism ) );
end : CategoryFilter := IsAbelianCategory );
##
AddDerivationToCAP( ComponentOfMorphismIntoDirectProduct,
"ComponentOfMorphismIntoDirectProduct by composing with the direct product projection",
[ [ ProjectionInFactorOfDirectProduct, 1 ],
[ PreCompose, 1 ] ],
function( cat, alpha, factors, nr )
return PreCompose( cat, alpha, ProjectionInFactorOfDirectProduct( cat, factors, nr ) );
end );
##
AddDerivationToCAP( ComponentOfMorphismIntoDirectSum,
"ComponentOfMorphismIntoDirectSum by composing with the direct sum projection",
[ [ ProjectionInFactorOfDirectSum, 1 ],
[ PreCompose, 1 ] ],
function( cat, alpha, summands, nr )
return PreCompose( cat, alpha, ProjectionInFactorOfDirectSum( cat, summands, nr ) );
end );
##
AddDerivationToCAP( MorphismBetweenDirectSumsWithGivenDirectSums,
"MorphismBetweenDirectSumsWithGivenDirectSums using universal morphisms of direct sums (without support for empty limits)",
[ [ ZeroMorphism, 1 ],
[ UniversalMorphismIntoDirectSumWithGivenDirectSum, 2 ],
[ UniversalMorphismFromDirectSumWithGivenDirectSum, 1 ] ],
function( cat, S, diagram_S, morphism_matrix, diagram_T, T )
local test_diagram_product, test_diagram_coproduct;
if morphism_matrix = [ ] or morphism_matrix[1] = [ ] then
return ZeroMorphism( cat, S, T );
fi;
test_diagram_coproduct := ListN( diagram_S, morphism_matrix,
{ source, row } -> UniversalMorphismIntoDirectSumWithGivenDirectSum( cat, diagram_T, source, row, T )
);
return UniversalMorphismFromDirectSumWithGivenDirectSum( cat, diagram_S, T, test_diagram_coproduct, S );
end : CategoryFilter := cat -> not ( IsBound( cat!.supports_empty_limits ) and cat!.supports_empty_limits = true ) );
##
AddDerivationToCAP( MorphismBetweenDirectSumsWithGivenDirectSums,
"MorphismBetweenDirectSumsWithGivenDirectSums using universal morphisms of direct sums (with support for empty limits)",
[ [ UniversalMorphismIntoDirectSumWithGivenDirectSum, 2 ],
[ UniversalMorphismFromDirectSumWithGivenDirectSum, 1 ] ],
function( cat, S, diagram_S, morphism_matrix, diagram_T, T )
local test_diagram_product, test_diagram_coproduct;
test_diagram_coproduct := ListN( diagram_S, morphism_matrix,
{ source, row } -> UniversalMorphismIntoDirectSumWithGivenDirectSum( cat, diagram_T, source, row, T )
);
return UniversalMorphismFromDirectSumWithGivenDirectSum( cat, diagram_S, T, test_diagram_coproduct, S );
end : CategoryFilter := cat -> IsBound( cat!.supports_empty_limits ) and cat!.supports_empty_limits = true );
##
AddDerivationToCAP( HomologyObjectFunctorialWithGivenHomologyObjects,
"HomologyObjectFunctorialWithGivenHomologyObjects using functoriality of (co)kernels and images in abelian categories",
[ [ ImageEmbedding, 2 ],
[ PreCompose, 3 ],
[ KernelEmbedding, 2 ],
[ CokernelProjection, 2 ],
[ CokernelObjectFunctorial, 1 ],
[ LiftAlongMonomorphism, 1 ],
[ PreComposeList, 1 ],
[ IsomorphismFromHomologyObjectToItsConstructionAsAnImageObject, 1 ],
[ IsomorphismFromItsConstructionAsAnImageObjectToHomologyObject, 1 ] ],
function( cat, homology_source, mor_list, homology_range )
local alpha, beta, epsilon, gamma, delta, image_emb_source, image_emb_range, cok_functorial, functorial_mor;
alpha := mor_list[1];
beta := mor_list[2];
epsilon := mor_list[3];
gamma := mor_list[4];
delta := mor_list[5];
image_emb_source := ImageEmbedding( cat,
PreCompose( cat, KernelEmbedding( cat, beta ), CokernelProjection( cat, alpha ) )
);
image_emb_range := ImageEmbedding( cat,
PreCompose( cat, KernelEmbedding( cat, delta ), CokernelProjection( cat, gamma ) )
);
cok_functorial := CokernelObjectFunctorial( cat, alpha, epsilon, gamma );
functorial_mor :=
LiftAlongMonomorphism( cat,
image_emb_range, PreCompose( cat, image_emb_source, cok_functorial )
);
return PreComposeList( cat,
homology_source,
[
IsomorphismFromHomologyObjectToItsConstructionAsAnImageObject( cat, alpha, beta ),
functorial_mor,
IsomorphismFromItsConstructionAsAnImageObjectToHomologyObject( cat, gamma, delta ),
],
homology_range
);
end : CategoryFilter := IsAbelianCategory );
###########################
##
## Methods returning a morphism with source or range constructed within the method!
## If there is a method available which only constructs this source or range,
## one has to be sure that this source is equal to that construction (by IsEqualForObjects)
##
###########################
##
AddDerivationToCAP( ZeroObjectFunctorial,
"ZeroObjectFunctorial using ZeroMorphism",
[ [ ZeroObject, 1 ],
[ ZeroMorphism, 1 ] ],
function( cat )
local zero_object;
zero_object := ZeroObject( cat );
return ZeroMorphism( cat, zero_object, zero_object );
end );
##
AddDerivationToCAP( JointPairwiseDifferencesOfMorphismsIntoDirectProduct,
"JointPairwiseDifferencesOfMorphismsIntoDirectProduct using the operations defining this morphism (without support for empty limits)",
[ [ UniversalMorphismIntoTerminalObject, 1 ],
[ UniversalMorphismIntoDirectProduct, 2 ],
[ SubtractionForMorphisms, 1 ] ],
function( cat, A, diagram )
local number_of_morphisms, ranges, mor1, mor2;
number_of_morphisms := Length( diagram );
if number_of_morphisms = 1 then
return UniversalMorphismIntoTerminalObject( cat, A );
fi;
ranges := List( diagram, Range );
mor1 := UniversalMorphismIntoDirectProduct( cat, ranges{[ 1 .. number_of_morphisms - 1 ]}, A, diagram{[ 1 .. number_of_morphisms - 1 ]} );
mor2 := UniversalMorphismIntoDirectProduct( cat, ranges{[ 2 .. number_of_morphisms ]}, A, diagram{[ 2 .. number_of_morphisms ]} );
return SubtractionForMorphisms( cat, mor1, mor2 );
end : CategoryFilter := cat -> not ( IsBound( cat!.supports_empty_limits ) and cat!.supports_empty_limits = true ) );
##
AddDerivationToCAP( JointPairwiseDifferencesOfMorphismsIntoDirectProduct,
"JointPairwiseDifferencesOfMorphismsIntoDirectProduct using the operations defining this morphism (with support for empty limits)",
[ [ UniversalMorphismIntoDirectProduct, 2 ],
[ SubtractionForMorphisms, 1 ] ],
function( cat, A, diagram )
local number_of_morphisms, ranges, mor1, mor2;
number_of_morphisms := Length( diagram );
ranges := List( diagram, Range );
mor1 := UniversalMorphismIntoDirectProduct( cat, ranges{[ 1 .. number_of_morphisms - 1 ]}, A, diagram{[ 1 .. number_of_morphisms - 1 ]} );
mor2 := UniversalMorphismIntoDirectProduct( cat, ranges{[ 2 .. number_of_morphisms ]}, A, diagram{[ 2 .. number_of_morphisms ]} );
return SubtractionForMorphisms( cat, mor1, mor2 );
end : CategoryFilter := cat -> IsBound( cat!.supports_empty_limits ) and cat!.supports_empty_limits = true );
##
--> --------------------
--> maximum size reached
--> --------------------
[ zur Elbe Produktseite wechseln0.73Quellennavigators
Analyse erneut starten
]
|
