Quelle DerivedMethods.gi Sprache: unbekannt

# 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

--> --------------------

Quelle DerivedMethods.gi Sprache: unbekannt

[ Dauer der Verarbeitung: 0.54 Sekunden (vorverarbeitet) ]