|
# SPDX-License-Identifier: GPL-2.0-or-later
# CAP: Categories, Algorithms, Programming
#
# Implementations
#
# THIS FILE IS AUTOMATICALLY GENERATED, SEE LimitConvenience.gi
##
InstallMethod( UniversalMorphismIntoDirectProduct,
[ IsList ],
function( list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectProduct( CapCategory( list[1] ), list );
end );
##
InstallOtherMethod( UniversalMorphismIntoDirectProduct,
[ IsCapCategory, IsList ],
function( cat, list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectProduct( cat, List( list, Range ), list );
end );
##
InstallOtherMethod( UniversalMorphismIntoDirectProduct,
[ IsCapCategoryObject, IsList ],
function( test_object, list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectProduct( CapCategory( test_object ), test_object, list );
end );
##
InstallOtherMethod( UniversalMorphismIntoDirectProduct,
[ IsCapCategory, IsCapCategoryObject, IsList ],
function( cat, test_object, list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectProduct( cat, List( list, Range ), test_object, list );
end );
InstallOtherMethod( UniversalMorphismIntoDirectProduct,
[ IsList, IsList ],
function( objects, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectProduct( objects, Source( tau[1] ), tau );
end );
InstallOtherMethod( UniversalMorphismIntoDirectProduct,
[ IsCapCategory, IsList, IsList ],
function( cat, objects, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectProduct( cat, objects, Source( tau[1] ), tau );
end );
InstallOtherMethod( UniversalMorphismIntoDirectProductWithGivenDirectProduct,
[ IsList, IsList, IsCapCategoryObject ],
function( objects, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectProductWithGivenDirectProduct( objects, Source( tau[1] ), tau, P );
end );
InstallOtherMethod( UniversalMorphismIntoDirectProductWithGivenDirectProduct,
[ IsCapCategory, IsList, IsList, IsCapCategoryObject ],
function( cat, objects, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectProductWithGivenDirectProduct( cat, objects, Source( tau[1] ), tau, P );
end );
##
InstallMethod( UniversalMorphismFromCoproduct,
[ IsList ],
function( list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromCoproduct( CapCategory( list[1] ), list );
end );
##
InstallOtherMethod( UniversalMorphismFromCoproduct,
[ IsCapCategory, IsList ],
function( cat, list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromCoproduct( cat, List( list, Source ), list );
end );
##
InstallOtherMethod( UniversalMorphismFromCoproduct,
[ IsCapCategoryObject, IsList ],
function( test_object, list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromCoproduct( CapCategory( test_object ), test_object, list );
end );
##
InstallOtherMethod( UniversalMorphismFromCoproduct,
[ IsCapCategory, IsCapCategoryObject, IsList ],
function( cat, test_object, list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromCoproduct( cat, List( list, Source ), test_object, list );
end );
InstallOtherMethod( UniversalMorphismFromCoproduct,
[ IsList, IsList ],
function( objects, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromCoproduct( objects, Range( tau[1] ), tau );
end );
InstallOtherMethod( UniversalMorphismFromCoproduct,
[ IsCapCategory, IsList, IsList ],
function( cat, objects, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromCoproduct( cat, objects, Range( tau[1] ), tau );
end );
InstallOtherMethod( UniversalMorphismFromCoproductWithGivenCoproduct,
[ IsList, IsList, IsCapCategoryObject ],
function( objects, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromCoproductWithGivenCoproduct( objects, Range( tau[1] ), tau, P );
end );
InstallOtherMethod( UniversalMorphismFromCoproductWithGivenCoproduct,
[ IsCapCategory, IsList, IsList, IsCapCategoryObject ],
function( cat, objects, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromCoproductWithGivenCoproduct( cat, objects, Range( tau[1] ), tau, P );
end );
##
InstallOtherMethod( DirectProductFunctorial,
[ IsList ],
function( L )
return DirectProductFunctorial( List( L, Source ), L, List( L, Range ) );
end );
##
InstallOtherMethodForCompilerForCAP( DirectProductFunctorial,
[ IsCapCategory, IsList ],
function( cat, L )
return DirectProductFunctorial( cat, List( L, Source ), L, List( L, Range ) );
end );
##
InstallOtherMethod( DirectProductFunctorialWithGivenDirectProducts,
[ IsCapCategoryObject, IsList, IsCapCategoryObject ],
function( source, L, range )
return DirectProductFunctorialWithGivenDirectProducts( source, List( L, Source ), L, List( L, Range ), range );
end );
##
InstallOtherMethodForCompilerForCAP( DirectProductFunctorialWithGivenDirectProducts,
[ IsCapCategory, IsCapCategoryObject, IsList, IsCapCategoryObject ],
function( cat, source, L, range )
return DirectProductFunctorialWithGivenDirectProducts( cat, source, List( L, Source ), L, List( L, Range ), range );
end );
##
AddDerivationToCAP( DirectProductFunctorialWithGivenDirectProducts,
"DirectProductFunctorialWithGivenDirectProducts using the universality of the limit",
[ [UniversalMorphismIntoDirectProductWithGivenDirectProduct, 1 ], [ PreCompose, 2 ], [ ProjectionInFactorOfDirectProductWithGivenDirectProduct, 2 ] ],
function( cat, P, objects, L, objectsp, Pp )
return UniversalMorphismIntoDirectProductWithGivenDirectProduct( cat, objectsp, P, List( [ 1 .. Length( L ) ], i -> PreCompose( cat, ProjectionInFactorOfDirectProductWithGivenDirectProduct( cat, objects, i, P ), L[i] ) ), Pp );
end );
##
InstallOtherMethod( CoproductFunctorial,
[ IsList ],
function( L )
return CoproductFunctorial( List( L, Source ), L, List( L, Range ) );
end );
##
InstallOtherMethodForCompilerForCAP( CoproductFunctorial,
[ IsCapCategory, IsList ],
function( cat, L )
return CoproductFunctorial( cat, List( L, Source ), L, List( L, Range ) );
end );
##
InstallOtherMethod( CoproductFunctorialWithGivenCoproducts,
[ IsCapCategoryObject, IsList, IsCapCategoryObject ],
function( source, L, range )
return CoproductFunctorialWithGivenCoproducts( source, List( L, Source ), L, List( L, Range ), range );
end );
##
InstallOtherMethodForCompilerForCAP( CoproductFunctorialWithGivenCoproducts,
[ IsCapCategory, IsCapCategoryObject, IsList, IsCapCategoryObject ],
function( cat, source, L, range )
return CoproductFunctorialWithGivenCoproducts( cat, source, List( L, Source ), L, List( L, Range ), range );
end );
##
InstallMethod( UniversalMorphismIntoDirectSum,
[ IsList ],
function( list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectSum( CapCategory( list[1] ), list );
end );
##
InstallOtherMethod( UniversalMorphismIntoDirectSum,
[ IsCapCategory, IsList ],
function( cat, list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectSum( cat, List( list, Range ), list );
end );
##
InstallOtherMethod( UniversalMorphismIntoDirectSum,
[ IsCapCategoryObject, IsList ],
function( test_object, list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectSum( CapCategory( test_object ), test_object, list );
end );
##
InstallOtherMethod( UniversalMorphismIntoDirectSum,
[ IsCapCategory, IsCapCategoryObject, IsList ],
function( cat, test_object, list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectSum( cat, List( list, Range ), test_object, list );
end );
InstallOtherMethod( UniversalMorphismIntoDirectSum,
[ IsList, IsList ],
function( objects, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectSum( objects, Source( tau[1] ), tau );
end );
InstallOtherMethod( UniversalMorphismIntoDirectSum,
[ IsCapCategory, IsList, IsList ],
function( cat, objects, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectSum( cat, objects, Source( tau[1] ), tau );
end );
InstallOtherMethod( UniversalMorphismIntoDirectSumWithGivenDirectSum,
[ IsList, IsList, IsCapCategoryObject ],
function( objects, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectSumWithGivenDirectSum( objects, Source( tau[1] ), tau, P );
end );
InstallOtherMethod( UniversalMorphismIntoDirectSumWithGivenDirectSum,
[ IsCapCategory, IsList, IsList, IsCapCategoryObject ],
function( cat, objects, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoDirectSumWithGivenDirectSum( cat, objects, Source( tau[1] ), tau, P );
end );
##
InstallMethod( UniversalMorphismFromDirectSum,
[ IsList ],
function( list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromDirectSum( CapCategory( list[1] ), list );
end );
##
InstallOtherMethod( UniversalMorphismFromDirectSum,
[ IsCapCategory, IsList ],
function( cat, list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromDirectSum( cat, List( list, Source ), list );
end );
##
InstallOtherMethod( UniversalMorphismFromDirectSum,
[ IsCapCategoryObject, IsList ],
function( test_object, list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromDirectSum( CapCategory( test_object ), test_object, list );
end );
##
InstallOtherMethod( UniversalMorphismFromDirectSum,
[ IsCapCategory, IsCapCategoryObject, IsList ],
function( cat, test_object, list )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromDirectSum( cat, List( list, Source ), test_object, list );
end );
InstallOtherMethod( UniversalMorphismFromDirectSum,
[ IsList, IsList ],
function( objects, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromDirectSum( objects, Range( tau[1] ), tau );
end );
InstallOtherMethod( UniversalMorphismFromDirectSum,
[ IsCapCategory, IsList, IsList ],
function( cat, objects, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromDirectSum( cat, objects, Range( tau[1] ), tau );
end );
InstallOtherMethod( UniversalMorphismFromDirectSumWithGivenDirectSum,
[ IsList, IsList, IsCapCategoryObject ],
function( objects, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromDirectSumWithGivenDirectSum( objects, Range( tau[1] ), tau, P );
end );
InstallOtherMethod( UniversalMorphismFromDirectSumWithGivenDirectSum,
[ IsCapCategory, IsList, IsList, IsCapCategoryObject ],
function( cat, objects, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromDirectSumWithGivenDirectSum( cat, objects, Range( tau[1] ), tau, P );
end );
##
InstallOtherMethod( DirectSumFunctorial,
[ IsList ],
function( L )
return DirectSumFunctorial( List( L, Source ), L, List( L, Range ) );
end );
##
InstallOtherMethodForCompilerForCAP( DirectSumFunctorial,
[ IsCapCategory, IsList ],
function( cat, L )
return DirectSumFunctorial( cat, List( L, Source ), L, List( L, Range ) );
end );
##
InstallOtherMethod( DirectSumFunctorialWithGivenDirectSums,
[ IsCapCategoryObject, IsList, IsCapCategoryObject ],
function( source, L, range )
return DirectSumFunctorialWithGivenDirectSums( source, List( L, Source ), L, List( L, Range ), range );
end );
##
InstallOtherMethodForCompilerForCAP( DirectSumFunctorialWithGivenDirectSums,
[ IsCapCategory, IsCapCategoryObject, IsList, IsCapCategoryObject ],
function( cat, source, L, range )
return DirectSumFunctorialWithGivenDirectSums( cat, source, List( L, Source ), L, List( L, Range ), range );
end );
##
AddDerivationToCAP( DirectSumFunctorialWithGivenDirectSums,
"DirectSumFunctorialWithGivenDirectSums using the universality of the limit",
[ [UniversalMorphismIntoDirectSumWithGivenDirectSum, 1 ], [ PreCompose, 2 ], [ ProjectionInFactorOfDirectSumWithGivenDirectSum, 2 ] ],
function( cat, P, objects, L, objectsp, Pp )
return UniversalMorphismIntoDirectSumWithGivenDirectSum( cat, objectsp, P, List( [ 1 .. Length( L ) ], i -> PreCompose( cat, ProjectionInFactorOfDirectSumWithGivenDirectSum( cat, objects, i, P ), L[i] ) ), Pp );
end );
InstallOtherMethod( UniversalMorphismIntoFiberProduct,
[ IsList, IsList ],
function( morphisms, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoFiberProduct( morphisms, Source( tau[1] ), tau );
end );
InstallOtherMethod( UniversalMorphismIntoFiberProduct,
[ IsCapCategory, IsList, IsList ],
function( cat, morphisms, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoFiberProduct( cat, morphisms, Source( tau[1] ), tau );
end );
InstallOtherMethod( UniversalMorphismIntoFiberProductWithGivenFiberProduct,
[ IsList, IsList, IsCapCategoryObject ],
function( morphisms, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoFiberProductWithGivenFiberProduct( morphisms, Source( tau[1] ), tau, P );
end );
InstallOtherMethod( UniversalMorphismIntoFiberProductWithGivenFiberProduct,
[ IsCapCategory, IsList, IsList, IsCapCategoryObject ],
function( cat, morphisms, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoFiberProductWithGivenFiberProduct( cat, morphisms, Source( tau[1] ), tau, P );
end );
InstallOtherMethod( UniversalMorphismFromPushout,
[ IsList, IsList ],
function( morphisms, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromPushout( morphisms, Range( tau[1] ), tau );
end );
InstallOtherMethod( UniversalMorphismFromPushout,
[ IsCapCategory, IsList, IsList ],
function( cat, morphisms, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromPushout( cat, morphisms, Range( tau[1] ), tau );
end );
InstallOtherMethod( UniversalMorphismFromPushoutWithGivenPushout,
[ IsList, IsList, IsCapCategoryObject ],
function( morphisms, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromPushoutWithGivenPushout( morphisms, Range( tau[1] ), tau, P );
end );
InstallOtherMethod( UniversalMorphismFromPushoutWithGivenPushout,
[ IsCapCategory, IsList, IsList, IsCapCategoryObject ],
function( cat, morphisms, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromPushoutWithGivenPushout( cat, morphisms, Range( tau[1] ), tau, P );
end );
##
AddDerivationToCAP( FiberProductFunctorialWithGivenFiberProducts,
"FiberProductFunctorialWithGivenFiberProducts using the universality of the limit",
[ [UniversalMorphismIntoFiberProductWithGivenFiberProduct, 1 ], [ PreCompose, 2 ], [ ProjectionInFactorOfFiberProductWithGivenFiberProduct, 2 ] ],
function( cat, P, morphisms, L, morphismsp, Pp )
return UniversalMorphismIntoFiberProductWithGivenFiberProduct( cat, morphismsp, P, List( [ 1 .. Length( L ) ], i -> PreCompose( cat, ProjectionInFactorOfFiberProductWithGivenFiberProduct( cat, morphisms, i, P ), L[i] ) ), Pp );
end );
InstallOtherMethod( UniversalMorphismIntoEqualizer,
[ IsCapCategoryObject, IsList, IsCapCategoryMorphism ],
function( Y, morphisms, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoEqualizer( Y, morphisms, Source( tau ), tau );
end );
InstallOtherMethod( UniversalMorphismIntoEqualizer,
[ IsCapCategory, IsCapCategoryObject, IsList, IsCapCategoryMorphism ],
function( cat, Y, morphisms, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoEqualizer( cat, Y, morphisms, Source( tau ), tau );
end );
InstallOtherMethod( UniversalMorphismIntoEqualizerWithGivenEqualizer,
[ IsCapCategoryObject, IsList, IsCapCategoryMorphism, IsCapCategoryObject ],
function( Y, morphisms, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoEqualizerWithGivenEqualizer( Y, morphisms, Source( tau ), tau, P );
end );
InstallOtherMethod( UniversalMorphismIntoEqualizerWithGivenEqualizer,
[ IsCapCategory, IsCapCategoryObject, IsList, IsCapCategoryMorphism, IsCapCategoryObject ],
function( cat, Y, morphisms, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismIntoEqualizerWithGivenEqualizer( cat, Y, morphisms, Source( tau ), tau, P );
end );
InstallOtherMethod( UniversalMorphismFromCoequalizer,
[ IsCapCategoryObject, IsList, IsCapCategoryMorphism ],
function( Y, morphisms, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromCoequalizer( Y, morphisms, Range( tau ), tau );
end );
InstallOtherMethod( UniversalMorphismFromCoequalizer,
[ IsCapCategory, IsCapCategoryObject, IsList, IsCapCategoryMorphism ],
function( cat, Y, morphisms, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromCoequalizer( cat, Y, morphisms, Range( tau ), tau );
end );
InstallOtherMethod( UniversalMorphismFromCoequalizerWithGivenCoequalizer,
[ IsCapCategoryObject, IsList, IsCapCategoryMorphism, IsCapCategoryObject ],
function( Y, morphisms, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromCoequalizerWithGivenCoequalizer( Y, morphisms, Range( tau ), tau, P );
end );
InstallOtherMethod( UniversalMorphismFromCoequalizerWithGivenCoequalizer,
[ IsCapCategory, IsCapCategoryObject, IsList, IsCapCategoryMorphism, IsCapCategoryObject ],
function( cat, Y, morphisms, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return UniversalMorphismFromCoequalizerWithGivenCoequalizer( cat, Y, morphisms, Range( tau ), tau, P );
end );
##
AddDerivationToCAP( EqualizerFunctorialWithGivenEqualizers,
"EqualizerFunctorialWithGivenEqualizers using the universality of the limit",
[ [UniversalMorphismIntoEqualizerWithGivenEqualizer, 1 ], [ PreCompose, 1 ], [ EmbeddingOfEqualizerWithGivenEqualizer, 1 ] ],
function( cat, P, morphisms, mu, morphismsp, Pp )
local Y, Yp;
Y := Source( mu );
Yp := Range( mu );
return UniversalMorphismIntoEqualizerWithGivenEqualizer( cat, Yp, morphismsp, P, PreCompose( cat, EmbeddingOfEqualizerWithGivenEqualizer( cat, Y, morphisms, P ), mu ), Pp );
end );
InstallOtherMethod( KernelLift,
[ IsCapCategoryMorphism, IsCapCategoryMorphism ],
function( alpha, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return KernelLift( alpha, Source( tau ), tau );
end );
InstallOtherMethod( KernelLift,
[ IsCapCategory, IsCapCategoryMorphism, IsCapCategoryMorphism ],
function( cat, alpha, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return KernelLift( cat, alpha, Source( tau ), tau );
end );
InstallOtherMethod( KernelLiftWithGivenKernelObject,
[ IsCapCategoryMorphism, IsCapCategoryMorphism, IsCapCategoryObject ],
function( alpha, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return KernelLiftWithGivenKernelObject( alpha, Source( tau ), tau, P );
end );
InstallOtherMethod( KernelLiftWithGivenKernelObject,
[ IsCapCategory, IsCapCategoryMorphism, IsCapCategoryMorphism, IsCapCategoryObject ],
function( cat, alpha, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return KernelLiftWithGivenKernelObject( cat, alpha, Source( tau ), tau, P );
end );
InstallOtherMethod( CokernelColift,
[ IsCapCategoryMorphism, IsCapCategoryMorphism ],
function( alpha, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return CokernelColift( alpha, Range( tau ), tau );
end );
InstallOtherMethod( CokernelColift,
[ IsCapCategory, IsCapCategoryMorphism, IsCapCategoryMorphism ],
function( cat, alpha, tau )
#% CAP_JIT_RESOLVE_FUNCTION
return CokernelColift( cat, alpha, Range( tau ), tau );
end );
InstallOtherMethod( CokernelColiftWithGivenCokernelObject,
[ IsCapCategoryMorphism, IsCapCategoryMorphism, IsCapCategoryObject ],
function( alpha, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return CokernelColiftWithGivenCokernelObject( alpha, Range( tau ), tau, P );
end );
InstallOtherMethod( CokernelColiftWithGivenCokernelObject,
[ IsCapCategory, IsCapCategoryMorphism, IsCapCategoryMorphism, IsCapCategoryObject ],
function( cat, alpha, tau, P )
#% CAP_JIT_RESOLVE_FUNCTION
return CokernelColiftWithGivenCokernelObject( cat, alpha, Range( tau ), tau, P );
end );
##
AddDerivationToCAP( KernelObjectFunctorialWithGivenKernelObjects,
"KernelObjectFunctorialWithGivenKernelObjects using the universality of the limit",
[ [KernelLiftWithGivenKernelObject, 1 ], [ PreCompose, 1 ], [ KernelEmbeddingWithGivenKernelObject, 1 ] ],
function( cat, P, alpha, mu, alphap, Pp )
return KernelLiftWithGivenKernelObject( cat, alphap, P, PreCompose( cat, KernelEmbeddingWithGivenKernelObject( cat, alpha, P ), mu ), Pp );
end );
##
AddDerivationToCAP( TerminalObjectFunctorialWithGivenTerminalObjects,
"TerminalObjectFunctorialWithGivenTerminalObjects using the universality of the limit",
[ [UniversalMorphismIntoTerminalObjectWithGivenTerminalObject, 1 ] ],
function( cat, P, Pp )
return UniversalMorphismIntoTerminalObjectWithGivenTerminalObject( cat, P, Pp );
end );
##
AddDerivationToCAP( TerminalObjectFunctorial,
"TerminalObjectFunctorial by taking the identity morphism of TerminalObject",
[ [ TerminalObject, 1 ],
[ IdentityMorphism, 1 ] ],
function( cat )
return IdentityMorphism( cat, TerminalObject( cat ) );
end );
##
AddDerivationToCAP( ZeroObjectFunctorialWithGivenZeroObjects,
"ZeroObjectFunctorialWithGivenZeroObjects using the universality of the limit",
[ [UniversalMorphismIntoZeroObjectWithGivenZeroObject, 1 ] ],
function( cat, P, Pp )
return UniversalMorphismIntoZeroObjectWithGivenZeroObject( cat, P, Pp );
end );
##
AddDerivationToCAP( ZeroObjectFunctorial,
"ZeroObjectFunctorial by taking the identity morphism of ZeroObject",
[ [ ZeroObject, 1 ],
[ IdentityMorphism, 1 ] ],
function( cat )
return IdentityMorphism( cat, ZeroObject( cat ) );
end );
[ Dauer der Verarbeitung: 0.7 Sekunden
(vorverarbeitet)
]
|
