|
# SPDX-License-Identifier: GPL-2.0-or-later
# CAP: Categories, Algorithms, Programming
#
# Implementations
#
BindGlobal( "CAP_INTERNAL_CORE_METHOD_NAME_RECORD", rec(
ObjectConstructor := rec(
filter_list := [ "category", "object_datum" ],
return_type := "object",
compatible_with_congruence_of_morphisms := false,
),
ObjectDatum := rec(
filter_list := [ "category", "object" ],
return_type := "object_datum",
),
MorphismConstructor := rec(
filter_list := [ "category", "object", "morphism_datum", "object" ],
return_type := "morphism",
compatible_with_congruence_of_morphisms := false,
),
MorphismDatum := rec(
filter_list := [ "category", "morphism" ],
return_type := "morphism_datum",
compatible_with_congruence_of_morphisms := false,
),
SetOfObjectsOfCategory := rec(
filter_list := [ "category" ],
return_type := "list_of_objects",
dual_operation := "SetOfObjectsOfCategory",
),
SetOfMorphismsOfFiniteCategory := rec(
filter_list := [ "category" ],
return_type := "list_of_morphisms",
dual_operation := "SetOfMorphismsOfFiniteCategory",
),
LiftAlongMonomorphism := rec(
filter_list := [ "category", "morphism", "morphism" ],
input_arguments_names := [ "cat", "iota", "tau" ],
output_source_getter_string := "Source( tau )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Source( iota )",
output_range_getter_preconditions := [ ],
pre_function := function( cat, iota, tau )
if not IsEqualForObjects( cat, Range( iota ), Range( tau ) ) then
return [ false, "the two morphisms must have equal ranges" ];
fi;
return [ true ];
end,
return_type := "morphism",
dual_operation := "ColiftAlongEpimorphism",
compatible_with_congruence_of_morphisms := true,
),
IsLiftableAlongMonomorphism := rec(
filter_list := [ "category", "morphism", "morphism" ],
pre_function := function( cat, iota, tau )
if not IsEqualForObjects( cat, Range( iota ), Range( tau ) ) then
return [ false, "the two morphisms must have equal ranges" ];
fi;
return [ true ];
end,
return_type := "bool",
dual_operation := "IsColiftableAlongEpimorphism",
compatible_with_congruence_of_morphisms := true,
),
ColiftAlongEpimorphism := rec(
filter_list := [ "category", "morphism", "morphism" ],
input_arguments_names := [ "cat", "epsilon", "tau" ],
output_source_getter_string := "Range( epsilon )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Range( tau )",
output_range_getter_preconditions := [ ],
pre_function := function( cat, epsilon, tau )
if not IsEqualForObjects( cat, Source( epsilon ), Source( tau ) ) then
return [ false, "the two morphisms must have equal sources" ];
fi;
return [ true ];
end,
return_type := "morphism",
dual_operation := "LiftAlongMonomorphism",
compatible_with_congruence_of_morphisms := true,
),
IsColiftableAlongEpimorphism := rec(
filter_list := [ "category", "morphism", "morphism" ],
pre_function := function( cat, epsilon, tau )
if not IsEqualForObjects( cat, Source( epsilon ), Source( tau ) ) then
return [ false, "the two morphisms must have equal sources" ];
fi;
return [ true ];
end,
return_type := "bool",
dual_operation := "IsLiftableAlongMonomorphism",
compatible_with_congruence_of_morphisms := true,
),
Lift := rec(
filter_list := [ "category", "morphism", "morphism" ],
input_arguments_names := [ "cat", "alpha", "beta" ],
output_source_getter_string := "Source( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Source( beta )",
output_range_getter_preconditions := [ ],
pre_function := function( cat, iota, tau )
if not IsEqualForObjects( cat, Range( iota ), Range( tau ) ) then
return [ false, "the two morphisms must have equal ranges" ];
fi;
return [ true ];
end,
return_type := "morphism",
dual_operation := "Colift",
dual_arguments_reversed := true,
is_merely_set_theoretic := true,
compatible_with_congruence_of_morphisms := false,
),
IsLiftable := rec(
filter_list := [ "category", "morphism", "morphism" ],
pre_function := "Lift",
return_type := "bool",
dual_operation := "IsColiftable",
dual_arguments_reversed := true,
compatible_with_congruence_of_morphisms := false,
),
Colift := rec(
filter_list := [ "category", "morphism", "morphism" ],
input_arguments_names := [ "cat", "alpha", "beta" ],
output_source_getter_string := "Range( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Range( beta )",
output_range_getter_preconditions := [ ],
pre_function := function( cat, epsilon, tau )
if not IsEqualForObjects( cat, Source( epsilon ), Source( tau ) ) then
return [ false, "the two morphisms must have equal sources" ];
fi;
return [ true ];
end,
return_type := "morphism",
dual_operation := "Lift",
dual_arguments_reversed := true,
is_merely_set_theoretic := true,
compatible_with_congruence_of_morphisms := false,
),
IsColiftable := rec(
filter_list := [ "category", "morphism", "morphism" ],
pre_function := "Colift",
return_type := "bool",
dual_operation := "IsLiftable",
dual_arguments_reversed := true,
compatible_with_congruence_of_morphisms := false,
),
ProjectiveLift := rec(
filter_list := [ "category", "morphism", "morphism" ],
input_arguments_names := [ "cat", "alpha", "beta" ],
output_source_getter_string := "Source( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Source( beta )",
output_range_getter_preconditions := [ ],
pre_function := function( cat, iota, tau )
if not IsEqualForObjects( cat, Range( iota ), Range( tau ) ) then
return [ false, "the two morphisms must have equal ranges" ];
fi;
return [ true ];
end,
return_type := "morphism",
dual_arguments_reversed := true,
dual_operation := "InjectiveColift",
compatible_with_congruence_of_morphisms := false,
),
InjectiveColift := rec(
filter_list := [ "category", "morphism", "morphism" ],
input_arguments_names := [ "cat", "alpha", "beta" ],
output_source_getter_string := "Range( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Range( beta )",
output_range_getter_preconditions := [ ],
pre_function := function( cat, epsilon, tau )
if not IsEqualForObjects( cat, Source( epsilon ), Source( tau ) ) then
return [ false, "the two morphisms must have equal sources" ];
fi;
return [ true ];
end,
return_type := "morphism",
dual_arguments_reversed := true,
dual_operation := "ProjectiveLift",
compatible_with_congruence_of_morphisms := false,
),
IdentityMorphism := rec(
filter_list := [ "category", "object" ],
input_arguments_names := [ "cat", "a" ],
output_source_getter_string := "a",
output_source_getter_preconditions := [ ],
output_range_getter_string := "a",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "IdentityMorphism" ),
InverseForMorphisms := rec(
# Type check for IsIsomorphism
filter_list := [ "category", "morphism" ],
input_arguments_names := [ "cat", "alpha" ],
output_source_getter_string := "Range( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Source( alpha )",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "InverseForMorphisms",
compatible_with_congruence_of_morphisms := true,
),
PreInverseForMorphisms := rec(
filter_list := [ "category", "morphism" ],
input_arguments_names := [ "cat", "alpha" ],
output_source_getter_string := "Range( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Source( alpha )",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "PostInverseForMorphisms",
is_merely_set_theoretic := true
),
PostInverseForMorphisms := rec(
filter_list := [ "category", "morphism" ],
input_arguments_names := [ "cat", "alpha" ],
output_source_getter_string := "Range( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Source( alpha )",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "PreInverseForMorphisms",
is_merely_set_theoretic := true
),
KernelObject := rec(
filter_list := [ "category", "morphism" ],
input_arguments_names := [ "cat", "alpha" ],
return_type := "object",
dual_operation := "CokernelObject",
compatible_with_congruence_of_morphisms := false,
functorial := "KernelObjectFunctorial",
),
KernelEmbedding := rec(
filter_list := [ "category", "morphism" ],
input_arguments_names := [ "cat", "alpha" ],
output_range_getter_string := "Source( alpha )",
output_range_getter_preconditions := [ ],
with_given_object_position := "Source",
return_type := "morphism",
dual_operation := "CokernelProjection",
compatible_with_congruence_of_morphisms := false,
),
KernelEmbeddingWithGivenKernelObject := rec(
filter_list := [ "category", "morphism", "object" ],
input_arguments_names := [ "cat", "alpha", "P" ],
output_source_getter_string := "P",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Source( alpha )",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "CokernelProjectionWithGivenCokernelObject",
compatible_with_congruence_of_morphisms := false,
),
MorphismFromKernelObjectToSink := rec(
filter_list := [ "category", "morphism" ],
input_arguments_names := [ "cat", "alpha" ],
output_range_getter_string := "Range( alpha )",
output_range_getter_preconditions := [ ],
with_given_object_position := "Source",
dual_operation := "MorphismFromSourceToCokernelObject",
return_type := "morphism",
compatible_with_congruence_of_morphisms := false,
),
MorphismFromKernelObjectToSinkWithGivenKernelObject := rec(
filter_list := [ "category", "morphism", "object" ],
input_arguments_names := [ "cat", "alpha", "P" ],
output_source_getter_string := "P",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Range( alpha )",
output_range_getter_preconditions := [ ],
dual_operation := "MorphismFromSourceToCokernelObjectWithGivenCokernelObject",
return_type := "morphism",
compatible_with_congruence_of_morphisms := false,
),
KernelLift := rec(
filter_list := [ "category", "morphism", "object", "morphism" ],
input_arguments_names := [ "cat", "alpha", "T", "tau" ],
output_source_getter_string := "T",
output_source_getter_preconditions := [ ],
with_given_object_position := "Range",
return_type := "morphism",
dual_operation := "CokernelColift",
compatible_with_congruence_of_morphisms := false,
),
KernelLiftWithGivenKernelObject := rec(
filter_list := [ "category", "morphism", "object", "morphism", "object" ],
input_arguments_names := [ "cat", "alpha", "T", "tau", "P" ],
output_source_getter_string := "T",
output_source_getter_preconditions := [ ],
output_range_getter_string := "P",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "CokernelColiftWithGivenCokernelObject",
compatible_with_congruence_of_morphisms := false,
),
CokernelObject := rec(
filter_list := [ "category", "morphism" ],
input_arguments_names := [ "cat", "alpha" ],
return_type := "object",
dual_operation := "KernelObject",
compatible_with_congruence_of_morphisms := false,
functorial := "CokernelObjectFunctorial",
),
CokernelProjection := rec(
filter_list := [ "category", "morphism" ],
input_arguments_names := [ "cat", "alpha" ],
output_source_getter_string := "Range( alpha )",
output_source_getter_preconditions := [ ],
with_given_object_position := "Range",
return_type := "morphism",
dual_operation := "KernelEmbedding",
compatible_with_congruence_of_morphisms := false,
),
CokernelProjectionWithGivenCokernelObject := rec(
filter_list := [ "category", "morphism", "object" ],
input_arguments_names := [ "cat", "alpha", "P" ],
output_source_getter_string := "Range( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "P",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "KernelEmbeddingWithGivenKernelObject",
compatible_with_congruence_of_morphisms := false,
),
MorphismFromSourceToCokernelObject := rec(
filter_list := [ "category", "morphism" ],
input_arguments_names := [ "cat", "alpha" ],
output_source_getter_string := "Source( alpha )",
output_source_getter_preconditions := [ ],
with_given_object_position := "Range",
dual_operation := "MorphismFromKernelObjectToSink",
return_type := "morphism",
compatible_with_congruence_of_morphisms := false,
),
MorphismFromSourceToCokernelObjectWithGivenCokernelObject := rec(
filter_list := [ "category", "morphism", "object" ],
input_arguments_names := [ "cat", "alpha", "P" ],
output_source_getter_string := "Source( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "P",
output_range_getter_preconditions := [ ],
dual_operation := "MorphismFromKernelObjectToSinkWithGivenKernelObject",
return_type := "morphism",
compatible_with_congruence_of_morphisms := false,
),
CokernelColift := rec(
filter_list := [ "category", "morphism", "object", "morphism" ],
input_arguments_names := [ "cat", "alpha", "T", "tau" ],
output_range_getter_string := "T",
output_range_getter_preconditions := [ ],
with_given_object_position := "Source",
return_type := "morphism",
dual_operation := "KernelLift",
compatible_with_congruence_of_morphisms := false,
),
CokernelColiftWithGivenCokernelObject := rec(
filter_list := [ "category", "morphism", "object", "morphism", "object" ],
input_arguments_names := [ "cat", "alpha", "T", "tau", "P" ],
output_source_getter_string := "P",
output_source_getter_preconditions := [ ],
output_range_getter_string := "T",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "KernelLiftWithGivenKernelObject",
compatible_with_congruence_of_morphisms := false,
),
PreCompose := rec(
filter_list := [ "category", "morphism", "morphism" ],
input_arguments_names := [ "cat", "alpha", "beta" ],
output_source_getter_string := "Source( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Range( beta )",
output_range_getter_preconditions := [ ],
pre_function := function( cat, mor_left, mor_right )
if not IsEqualForObjects( cat, Range( mor_left ), Source( mor_right ) ) then
return [ false, "morphisms not composable" ];
fi;
return [ true ];
end,
return_type := "morphism",
dual_operation := "PostCompose",
compatible_with_congruence_of_morphisms := true,
),
SumOfMorphisms := rec(
filter_list := [ "category", "object", "list_of_morphisms", "object" ],
input_arguments_names := [ "cat", "source", "list_of_morphisms", "range" ],
pre_function := function( cat, source, list_of_morphisms, range )
local m;
for m in list_of_morphisms do
if not IsEqualForObjects( cat, source, Source( m ) ) or not IsEqualForObjects( cat, range, Range( m ) ) then
return [ false, "some of the morphisms are not compatible with the provided source and range objects" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
output_source_getter_string := "source",
output_range_getter_string := "range",
dual_operation := "SumOfMorphisms",
dual_arguments_reversed := true,
compatible_with_congruence_of_morphisms := true,
),
LinearCombinationOfMorphisms := rec(
filter_list := [ "category", "object", "list_of_elements_of_commutative_ring_of_linear_structure", "list_of_morphisms", "object" ],
input_arguments_names := [ "cat", "source", "list_of_ring_elements", "list_of_morphisms", "range" ],
pre_function := function( cat, source, list_of_ring_elements, list_of_morphisms, range )
local m;
if not Length( list_of_ring_elements ) = Length( list_of_morphisms ) then
return [ false, "the length of the lists of coefficients and morphisms must be the same" ];
fi;
for m in list_of_morphisms do
if not IsEqualForObjects( cat, source, Source( m ) ) or not IsEqualForObjects( cat, range, Range( m ) ) then
return [ false, "some of the morphisms are not compatible with the provided source and range objects" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
output_source_getter_string := "source",
output_range_getter_string := "range",
dual_operation := "LinearCombinationOfMorphisms",
dual_preprocessor_func := function( arg )
local list;
list := CAP_INTERNAL_OPPOSITE_RECURSIVE( arg );
return NTuple( 5, list[1], list[5], list[3], list[4], list[2] );
end,
compatible_with_congruence_of_morphisms := true,
),
PreComposeList := rec(
filter_list := [ "category", "object", "list_of_morphisms", "object" ],
input_arguments_names := [ "cat", "source", "list_of_morphisms", "range" ],
pre_function := function( cat, source, list_of_morphisms, range )
local i;
if IsEmpty( list_of_morphisms ) then
if not IsEqualForObjects( cat, source, range ) then
return [ false, "the given source and range are not equal while the given list of morphisms to compose is empty" ];
fi;
else
if not IsEqualForObjects( cat, source, Source( First( list_of_morphisms ) ) ) then
return [ false, "the given source is not equal to the source of the first morphism" ];
elif not IsEqualForObjects( cat, range, Range( Last( list_of_morphisms ) ) ) then
return [ false, "the given range is not equal to the range of the last morphism" ];
fi;
fi;
for i in [ 1 .. Length( list_of_morphisms ) - 1 ] do
if not IsEqualForObjects( cat, Range( list_of_morphisms[i] ), Source( list_of_morphisms[i + 1] ) ) then
return [ false, "morphisms not composable" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
output_source_getter_string := "source",
output_range_getter_string := "range",
dual_operation := "PostComposeList",
dual_arguments_reversed := true,
compatible_with_congruence_of_morphisms := true,
),
PostCompose := rec(
filter_list := [ "category", "morphism", "morphism" ],
input_arguments_names := [ "cat", "beta", "alpha" ],
output_source_getter_string := "Source( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Range( beta )",
output_range_getter_preconditions := [ ],
pre_function := function( cat, mor_right, mor_left )
if not IsEqualForObjects( cat, Range( mor_left ), Source( mor_right ) ) then
return [ false, "morphisms not composable" ];
fi;
return [ true ];
end,
return_type := "morphism",
dual_operation := "PreCompose",
compatible_with_congruence_of_morphisms := true,
),
PostComposeList := rec(
filter_list := [ "category", "object", "list_of_morphisms", "object" ],
input_arguments_names := [ "cat", "source", "list_of_morphisms", "range" ],
pre_function := function( cat, source, list_of_morphisms, range )
local i;
if IsEmpty( list_of_morphisms ) then
if not IsEqualForObjects( cat, source, range ) then
return [ false, "the given source and range are not equal while the given list of morphisms to compose is empty" ];
fi;
else
if not IsEqualForObjects( cat, source, Source( Last( list_of_morphisms ) ) ) then
return [ false, "the given source is not equal to the source of the last morphism" ];
elif not IsEqualForObjects( cat, range, Range( First( list_of_morphisms ) ) ) then
return [ false, "the given range is not equal to the range of the first morphism" ];
fi;
fi;
for i in [ 1 .. Length( list_of_morphisms ) - 1 ] do
if not IsEqualForObjects( cat, Range( list_of_morphisms[i + 1] ), Source( list_of_morphisms[i] ) ) then
return [ false, "morphisms not composable" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
output_source_getter_string := "source",
output_range_getter_string := "range",
dual_operation := "PreComposeList",
dual_arguments_reversed := true,
compatible_with_congruence_of_morphisms := true,
),
ZeroObject := rec(
filter_list := [ "category" ],
input_arguments_names := [ "cat" ],
return_type := "object",
dual_operation := "ZeroObject",
functorial := "ZeroObjectFunctorial",
),
ZeroObjectFunctorial := rec(
filter_list := [ "category" ],
input_arguments_names := [ "cat" ],
return_type := "morphism",
output_source_getter_string := "ZeroObject( cat )",
output_source_getter_preconditions := [ [ "ZeroObject", 1 ] ],
output_range_getter_string := "ZeroObject( cat )",
output_range_getter_preconditions := [ [ "ZeroObject", 1 ] ],
with_given_object_position := "both",
dual_operation := "ZeroObjectFunctorial",
dual_arguments_reversed := true
),
ZeroObjectFunctorialWithGivenZeroObjects := rec(
filter_list := [ "category", "object", "object" ],
input_arguments_names := [ "cat", "P", "Pp" ],
output_source_getter_string := "P",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Pp",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "ZeroObjectFunctorialWithGivenZeroObjects",
dual_arguments_reversed := true
),
UniversalMorphismFromZeroObject := rec(
filter_list := [ "category", "object" ],
input_arguments_names := [ "cat", "T" ],
output_range_getter_string := "T",
output_range_getter_preconditions := [ ],
with_given_object_position := "Source",
return_type := "morphism",
dual_operation := "UniversalMorphismIntoZeroObject" ),
UniversalMorphismFromZeroObjectWithGivenZeroObject := rec(
filter_list := [ "category", "object", "object" ],
input_arguments_names := [ "cat", "T", "P" ],
output_source_getter_string := "P",
output_source_getter_preconditions := [ ],
output_range_getter_string := "T",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "UniversalMorphismIntoZeroObjectWithGivenZeroObject" ),
UniversalMorphismIntoZeroObject := rec(
filter_list := [ "category", "object" ],
input_arguments_names := [ "cat", "T" ],
output_source_getter_string := "T",
output_source_getter_preconditions := [ ],
with_given_object_position := "Range",
return_type := "morphism",
dual_operation := "UniversalMorphismFromZeroObject" ),
UniversalMorphismIntoZeroObjectWithGivenZeroObject := rec(
filter_list := [ "category", "object", "object" ],
input_arguments_names := [ "cat", "T", "P" ],
output_source_getter_string := "T",
output_source_getter_preconditions := [ ],
output_range_getter_string := "P",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "UniversalMorphismFromZeroObjectWithGivenZeroObject" ),
IsomorphismFromZeroObjectToInitialObject := rec(
filter_list := [ "category" ],
return_type := "morphism",
dual_operation := "IsomorphismFromTerminalObjectToZeroObject",
),
IsomorphismFromInitialObjectToZeroObject := rec(
filter_list := [ "category" ],
return_type := "morphism",
dual_operation := "IsomorphismFromZeroObjectToTerminalObject",
),
IsomorphismFromZeroObjectToTerminalObject := rec(
filter_list := [ "category" ],
return_type := "morphism",
dual_operation := "IsomorphismFromInitialObjectToZeroObject",
),
IsomorphismFromTerminalObjectToZeroObject := rec(
filter_list := [ "category" ],
return_type := "morphism",
dual_operation := "IsomorphismFromZeroObjectToInitialObject",
),
ZeroMorphism := rec(
filter_list := [ "category", "object", "object" ],
input_arguments_names := [ "cat", "a", "b" ],
output_source_getter_string := "a",
output_source_getter_preconditions := [ ],
output_range_getter_string := "b",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_arguments_reversed := true,
dual_operation := "ZeroMorphism" ),
DirectSum := rec(
filter_list := [ "category", "list_of_objects" ],
input_arguments_names := [ "cat", "objects" ],
return_type := "object",
dual_operation := "DirectSum",
functorial := "DirectSumFunctorial",
),
ProjectionInFactorOfDirectSum := rec(
filter_list := [ "category", "list_of_objects", "integer" ],
input_arguments_names := [ "cat", "objects", "k" ],
output_range_getter_string := "objects[k]",
output_range_getter_preconditions := [ ],
with_given_object_position := "Source",
return_type := "morphism",
dual_operation := "InjectionOfCofactorOfDirectSum" ),
ProjectionInFactorOfDirectSumWithGivenDirectSum := rec(
filter_list := [ "category", "list_of_objects", "integer", "object" ],
input_arguments_names := [ "cat", "objects", "k", "P" ],
output_source_getter_string := "P",
output_source_getter_preconditions := [ ],
output_range_getter_string := "objects[k]",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "InjectionOfCofactorOfDirectSumWithGivenDirectSum" ),
UniversalMorphismIntoDirectSum := rec(
filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms" ],
input_arguments_names := [ "cat", "objects", "T", "tau" ],
output_source_getter_string := "T",
output_source_getter_preconditions := [ ],
with_given_object_position := "Range",
dual_operation := "UniversalMorphismFromDirectSum",
pre_function := function( cat, diagram, test_object, source )
local current_morphism;
for current_morphism in source do
if not IsEqualForObjects( cat, Source( current_morphism ), test_object ) then
return [ false, "sources of morphisms must be equal to the test object in given source diagram" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := true,
),
UniversalMorphismIntoDirectSumWithGivenDirectSum := rec(
filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms", "object" ],
input_arguments_names := [ "cat", "objects", "T", "tau", "P" ],
output_source_getter_string := "T",
output_source_getter_preconditions := [ ],
output_range_getter_string := "P",
output_range_getter_preconditions := [ ],
dual_operation := "UniversalMorphismFromDirectSumWithGivenDirectSum",
pre_function := function( cat, diagram, test_object, source, direct_sum )
local current_morphism;
for current_morphism in source do
if not IsEqualForObjects( cat, Source( current_morphism ), test_object ) then
return [ false, "sources of morphisms must be equal to the test object in given source diagram" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := true,
),
InjectionOfCofactorOfDirectSum := rec(
filter_list := [ "category", "list_of_objects", "integer" ],
input_arguments_names := [ "cat", "objects", "k" ],
output_source_getter_string := "objects[k]",
output_source_getter_preconditions := [ ],
with_given_object_position := "Range",
return_type := "morphism",
dual_operation := "ProjectionInFactorOfDirectSum" ),
InjectionOfCofactorOfDirectSumWithGivenDirectSum := rec(
filter_list := [ "category", "list_of_objects", "integer", "object" ],
input_arguments_names := [ "cat", "objects", "k", "P" ],
output_source_getter_string := "objects[k]",
output_source_getter_preconditions := [ ],
output_range_getter_string := "P",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "ProjectionInFactorOfDirectSumWithGivenDirectSum" ),
UniversalMorphismFromDirectSum := rec(
filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms" ],
input_arguments_names := [ "cat", "objects", "T", "tau" ],
output_range_getter_string := "T",
output_range_getter_preconditions := [ ],
with_given_object_position := "Source",
dual_operation := "UniversalMorphismIntoDirectSum",
pre_function := function( cat, diagram, test_object, sink )
local current_morphism;
for current_morphism in sink do
if not IsEqualForObjects( cat, Range( current_morphism ), test_object ) then
return [ false, "ranges of morphisms must be equal to the test object in given sink diagram" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := true,
),
UniversalMorphismFromDirectSumWithGivenDirectSum := rec(
filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms", "object" ],
input_arguments_names := [ "cat", "objects", "T", "tau", "P" ],
output_source_getter_string := "P",
output_source_getter_preconditions := [ ],
output_range_getter_string := "T",
output_range_getter_preconditions := [ ],
dual_operation := "UniversalMorphismIntoDirectSumWithGivenDirectSum",
pre_function := function( cat, diagram, test_object, sink, direct_sum )
local current_morphism;
for current_morphism in sink do
if not IsEqualForObjects( cat, Range( current_morphism ), test_object ) then
return [ false, "ranges of morphisms must be equal to the test object in given sink diagram" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := true,
),
TerminalObject := rec(
filter_list := [ "category" ],
input_arguments_names := [ "cat" ],
return_type := "object",
dual_operation := "InitialObject",
functorial := "TerminalObjectFunctorial",
),
UniversalMorphismIntoTerminalObject := rec(
filter_list := [ "category", "object" ],
input_arguments_names := [ "cat", "T" ],
output_source_getter_string := "T",
output_source_getter_preconditions := [ ],
with_given_object_position := "Range",
return_type := "morphism",
dual_operation := "UniversalMorphismFromInitialObject" ),
UniversalMorphismIntoTerminalObjectWithGivenTerminalObject := rec(
filter_list := [ "category", "object", "object" ],
input_arguments_names := [ "cat", "T", "P" ],
output_source_getter_string := "T",
output_source_getter_preconditions := [ ],
output_range_getter_string := "P",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "UniversalMorphismFromInitialObjectWithGivenInitialObject" ),
InitialObject := rec(
filter_list := [ "category" ],
input_arguments_names := [ "cat" ],
return_type := "object",
dual_operation := "TerminalObject",
functorial := "InitialObjectFunctorial",
),
UniversalMorphismFromInitialObject := rec(
filter_list := [ "category", "object" ],
input_arguments_names := [ "cat", "T" ],
output_range_getter_string := "T",
output_range_getter_preconditions := [ ],
with_given_object_position := "Source",
return_type := "morphism",
dual_operation := "UniversalMorphismIntoTerminalObject" ),
UniversalMorphismFromInitialObjectWithGivenInitialObject := rec(
filter_list := [ "category", "object", "object" ],
input_arguments_names := [ "cat", "T", "P" ],
output_source_getter_string := "P",
output_source_getter_preconditions := [ ],
output_range_getter_string := "T",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "UniversalMorphismIntoTerminalObjectWithGivenTerminalObject" ),
DirectProduct := rec(
filter_list := [ "category", "list_of_objects" ],
input_arguments_names := [ "cat", "objects" ],
return_type := "object",
dual_operation := "Coproduct",
functorial := "DirectProductFunctorial",
),
ProjectionInFactorOfDirectProduct := rec(
filter_list := [ "category", "list_of_objects", "integer" ],
input_arguments_names := [ "cat", "objects", "k" ],
output_range_getter_string := "objects[k]",
output_range_getter_preconditions := [ ],
with_given_object_position := "Source",
return_type := "morphism",
dual_operation := "InjectionOfCofactorOfCoproduct" ),
ProjectionInFactorOfDirectProductWithGivenDirectProduct := rec(
filter_list := [ "category", "list_of_objects", "integer", "object" ],
input_arguments_names := [ "cat", "objects", "k", "P" ],
output_source_getter_string := "P",
output_source_getter_preconditions := [ ],
output_range_getter_string := "objects[k]",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "InjectionOfCofactorOfCoproductWithGivenCoproduct" ),
UniversalMorphismIntoDirectProduct := rec(
filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms" ],
input_arguments_names := [ "cat", "objects", "T", "tau" ],
output_source_getter_string := "T",
output_source_getter_preconditions := [ ],
with_given_object_position := "Range",
dual_operation := "UniversalMorphismFromCoproduct",
pre_function := function( cat, diagram, test_object, source )
local current_morphism;
for current_morphism in source do
if not IsEqualForObjects( cat, Source( current_morphism ), test_object ) then
return [ false, "sources of morphisms must be equal to the test object in given source diagram" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := true,
),
UniversalMorphismIntoDirectProductWithGivenDirectProduct := rec(
filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms", "object" ],
input_arguments_names := [ "cat", "objects", "T", "tau", "P" ],
output_source_getter_string := "T",
output_source_getter_preconditions := [ ],
output_range_getter_string := "P",
output_range_getter_preconditions := [ ],
dual_operation := "UniversalMorphismFromCoproductWithGivenCoproduct",
pre_function := function( cat, diagram, test_object, source, direct_product )
local current_morphism;
for current_morphism in source do
if not IsEqualForObjects( cat, Source( current_morphism ), test_object ) then
return [ false, "sources of morphisms must be equal to the test object in given source diagram" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := true,
),
ComponentOfMorphismIntoDirectProduct := rec(
filter_list := [ "category", "morphism", "list_of_objects", "integer" ],
input_arguments_names := [ "cat", "alpha", "P", "i" ],
output_source_getter_string := "Source( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "P[i]",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "ComponentOfMorphismFromCoproduct" ),
IsCongruentForMorphisms := rec(
filter_list := [ "category", "morphism", "morphism" ],
dual_operation := "IsCongruentForMorphisms",
pre_function := function( cat, morphism_1, morphism_2 )
if not IsEqualForObjects( cat, Source( morphism_1 ), Source( morphism_2 ) ) then
return [ false, "sources are not equal" ];
fi;
if not IsEqualForObjects( cat, Range( morphism_1 ), Range( morphism_2 ) ) then
return [ false, "ranges are not equal" ];
fi;
return [ true ];
end,
redirect_function := function( cat, morphism_1, morphism_2 )
if IsIdenticalObj( morphism_1, morphism_2 ) then
return [ true, true ];
else
return [ false ];
fi;
end,
post_function := function( cat, morphism_1, morphism_2, return_value )
if cat!.predicate_logic_propagation_for_morphisms and
cat!.predicate_logic and return_value = true then
INSTALL_TODO_LIST_FOR_EQUAL_MORPHISMS( morphism_1, morphism_2 );
fi;
end,
return_type := "bool",
compatible_with_congruence_of_morphisms := true,
),
IsEqualForMorphisms := rec(
filter_list := [ "category", "morphism", "morphism" ],
dual_operation := "IsEqualForMorphisms",
pre_function := function( cat, morphism_1, morphism_2 )
if not IsEqualForObjects( cat, Source( morphism_1 ), Source( morphism_2 ) ) then
return [ false, "sources are not equal" ];
fi;
if not IsEqualForObjects( cat, Range( morphism_1 ), Range( morphism_2 ) ) then
return [ false, "ranges are not equal" ];
fi;
return [ true ];
end,
redirect_function := function( cat, morphism_1, morphism_2 )
if IsIdenticalObj( morphism_1, morphism_2 ) then
return [ true, true ];
else
return [ false ];
fi;
end,
return_type := "bool",
compatible_with_congruence_of_morphisms := false,
),
IsEqualForMorphismsOnMor := rec(
filter_list := [ "category", "morphism", "morphism" ],
dual_operation := "IsEqualForMorphismsOnMor",
redirect_function := function( cat, morphism_1, morphism_2 )
if IsIdenticalObj( morphism_1, morphism_2 ) then
return [ true, true ];
else
return [ false ];
fi;
end,
return_type := "bool",
compatible_with_congruence_of_morphisms := false,
),
IsEqualForObjects := rec(
filter_list := [ "category", "object", "object" ],
dual_operation := "IsEqualForObjects",
redirect_function := function( cat, object_1, object_2 )
if IsIdenticalObj( object_1, object_2 ) then
return [ true, true ];
else
return [ false ];
fi;
end,
post_function := function( cat, object_1, object_2, return_value )
if cat!.predicate_logic_propagation_for_objects and
cat!.predicate_logic and return_value = true and not IsIdenticalObj( object_1, object_2 ) then
INSTALL_TODO_LIST_FOR_EQUAL_OBJECTS( object_1, object_2 );
fi;
end,
return_type := "bool" ),
IsEqualForCacheForObjects := rec(
filter_list := [ "category", "object", "object" ],
dual_operation := "IsEqualForCacheForObjects",
return_type := "bool" ),
IsEqualForCacheForMorphisms := rec(
filter_list := [ "category", "morphism", "morphism" ],
dual_operation := "IsEqualForCacheForMorphisms",
return_type := "bool",
compatible_with_congruence_of_morphisms := false,
),
IsIsomorphicForObjects := rec(
filter_list := [ "category", "object", "object" ],
input_arguments_names := [ "cat", "object_1", "object_2" ],
return_type := "bool",
dual_operation := "IsIsomorphicForObjects",
# The witness SomeIsomorphismBetweenObjects needs reversed arguments.
# This shows that reversing the arguments is the correct dualization,
# even if the relation is symmetric.
dual_arguments_reversed := true,
redirect_function := function( cat, object_1, object_2 )
# As any CAP operation, IsIsomorphicForObjects must be compatible with IsEqualForObjects.
# This implies that IsIsomorphicForObjects must be coarser than IsEqualForObjects:
# One can see this by first choosing object_2 := object_1 and the varying one argument with regard to IsEqualForObjects.
if IsEqualForObjects( object_1, object_2 ) then
return [ true, true ];
else
return [ false ];
fi;
end,
),
SomeIsomorphismBetweenObjects := rec(
filter_list := [ "category", "object", "object" ],
input_arguments_names := [ "cat", "object_1", "object_2" ],
return_type := "morphism",
output_source_getter_string := "object_1",
output_source_getter_preconditions := [ ],
output_range_getter_string := "object_2",
output_range_getter_preconditions := [ ],
dual_operation := "SomeIsomorphismBetweenObjects",
dual_arguments_reversed := true,
),
IsZeroForMorphisms := rec(
filter_list := [ "category", "morphism" ],
return_type := "bool",
dual_operation := "IsZeroForMorphisms",
is_reflected_by_faithful_functor := true,
compatible_with_congruence_of_morphisms := true,
),
AdditionForMorphisms := rec(
filter_list := [ "category", "morphism", "morphism" ],
input_arguments_names := [ "cat", "alpha", "beta" ],
output_source_getter_string := "Source( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Range( alpha )",
output_range_getter_preconditions := [ ],
dual_operation := "AdditionForMorphisms",
pre_function := function( cat, morphism_1, morphism_2 )
if not IsEqualForObjects( cat, Source( morphism_1 ), Source( morphism_2 ) ) then
return [ false, "sources are not equal" ];
fi;
if not IsEqualForObjects( cat, Range( morphism_1 ), Range( morphism_2 ) ) then
return [ false, "ranges are not equal" ];
fi;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := true,
),
SubtractionForMorphisms := rec(
filter_list := [ "category", "morphism", "morphism" ],
input_arguments_names := [ "cat", "alpha", "beta" ],
output_source_getter_string := "Source( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Range( alpha )",
output_range_getter_preconditions := [ ],
dual_operation := "SubtractionForMorphisms",
pre_function := function( cat, morphism_1, morphism_2 )
if not IsEqualForObjects( cat, Source( morphism_1 ), Source( morphism_2 ) ) then
return [ false, "sources are not equal" ];
fi;
if not IsEqualForObjects( cat, Range( morphism_1 ), Range( morphism_2 ) ) then
return [ false, "ranges are not equal" ];
fi;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := true,
),
MultiplyWithElementOfCommutativeRingForMorphisms := rec(
filter_list := [ "category", "element_of_commutative_ring_of_linear_structure", "morphism" ],
input_arguments_names := [ "cat", "r", "alpha" ],
output_source_getter_string := "Source( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Range( alpha )",
output_range_getter_preconditions := [ ],
pre_function := function( cat, r, morphism )
if not r in CommutativeRingOfLinearCategory( cat ) then
return [ false, "the first argument is not an element of the ring of the category of the morphism" ];
fi;
return [ true ];
end,
dual_operation := "MultiplyWithElementOfCommutativeRingForMorphisms",
return_type := "morphism",
compatible_with_congruence_of_morphisms := true,
),
AdditiveInverseForMorphisms := rec(
filter_list := [ "category", "morphism" ],
input_arguments_names := [ "cat", "alpha" ],
output_source_getter_string := "Source( alpha )",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Range( alpha )",
output_range_getter_preconditions := [ ],
dual_operation := "AdditiveInverseForMorphisms",
return_type := "morphism",
compatible_with_congruence_of_morphisms := true,
),
Coproduct := rec(
filter_list := [ "category", "list_of_objects" ],
input_arguments_names := [ "cat", "objects" ],
return_type := "object",
dual_operation := "DirectProduct",
functorial := "CoproductFunctorial",
),
InjectionOfCofactorOfCoproduct := rec(
filter_list := [ "category", "list_of_objects", "integer" ],
input_arguments_names := [ "cat", "objects", "k" ],
output_source_getter_string := "objects[k]",
output_source_getter_preconditions := [ ],
with_given_object_position := "Range",
return_type := "morphism",
dual_operation := "ProjectionInFactorOfDirectProduct" ),
InjectionOfCofactorOfCoproductWithGivenCoproduct := rec(
filter_list := [ "category", "list_of_objects", "integer", "object" ],
input_arguments_names := [ "cat", "objects", "k", "P" ],
output_source_getter_string := "objects[k]",
output_source_getter_preconditions := [ ],
output_range_getter_string := "P",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "ProjectionInFactorOfDirectProductWithGivenDirectProduct" ),
UniversalMorphismFromCoproduct := rec(
filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms" ],
input_arguments_names := [ "cat", "objects", "T", "tau" ],
output_range_getter_string := "T",
output_range_getter_preconditions := [ ],
with_given_object_position := "Source",
dual_operation := "UniversalMorphismIntoDirectProduct",
pre_function := function( cat, diagram, test_object, sink )
local current_morphism;
for current_morphism in sink do
if not IsEqualForObjects( cat, Range( current_morphism ), test_object ) then
return [ false, "ranges of morphisms must be equal to the test object in given sink diagram" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := true,
),
UniversalMorphismFromCoproductWithGivenCoproduct := rec(
filter_list := [ "category", "list_of_objects", "object", "list_of_morphisms", "object" ],
input_arguments_names := [ "cat", "objects", "T", "tau", "P" ],
output_source_getter_string := "P",
output_source_getter_preconditions := [ ],
output_range_getter_string := "T",
output_range_getter_preconditions := [ ],
dual_operation := "UniversalMorphismIntoDirectProductWithGivenDirectProduct",
pre_function := function( cat, diagram, test_object, sink, coproduct )
local current_morphism;
for current_morphism in sink do
if not IsEqualForObjects( cat, Range( current_morphism ), test_object ) then
return [ false, "ranges of morphisms must be equal to the test object in given sink diagram" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := true,
),
ComponentOfMorphismFromCoproduct := rec(
filter_list := [ "category", "morphism", "list_of_objects", "integer" ],
input_arguments_names := [ "cat", "alpha", "I", "i" ],
output_source_getter_string := "I[i]",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Range( alpha )",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "ComponentOfMorphismIntoDirectProduct" ),
IsEqualAsSubobjects := rec(
filter_list := [ "category", "morphism", "morphism" ],
return_type := "bool",
dual_operation := "IsEqualAsFactorobjects",
compatible_with_congruence_of_morphisms := true,
),
IsEqualAsFactorobjects := rec(
filter_list := [ "category", "morphism", "morphism" ],
return_type := "bool",
dual_operation := "IsEqualAsSubobjects",
compatible_with_congruence_of_morphisms := true,
),
IsDominating := rec(
filter_list := [ "category", "morphism", "morphism" ],
dual_operation := "IsCodominating",
pre_function := function( cat, sub1, sub2 )
if not IsEqualForObjects( cat, Range( sub1 ), Range( sub2 ) ) then
return [ false, "subobjects of different objects are not comparable by dominates" ];
fi;
return [ true ];
end,
return_type := "bool",
compatible_with_congruence_of_morphisms := true,
),
IsCodominating := rec(
filter_list := [ "category", "morphism", "morphism" ],
dual_operation := "IsDominating",
pre_function := function( cat, factor1, factor2 )
if not IsEqualForObjects( cat, Source( factor1 ), Source( factor2 ) ) then
return [ false, "factors of different objects are not comparable by codominates" ];
fi;
return [ true ];
end,
return_type := "bool",
compatible_with_congruence_of_morphisms := true,
),
Equalizer := rec(
filter_list := [ "category", "object", "list_of_morphisms" ],
input_arguments_names := [ "cat", "Y", "morphisms" ],
return_type := "object",
dual_operation := "Coequalizer",
pre_function := function( cat, cobase, diagram )
local base, current_morphism;
if IsEmpty( diagram ) then
return [ true ];
fi;
for current_morphism in diagram{[ 1 .. Length( diagram ) ]} do
if not IsEqualForObjects( cat, Source( current_morphism ), cobase ) then
return [ false, "the given morphisms of the equalizer diagram must have equal sources" ];
fi;
od;
base := Range( diagram[1] );
for current_morphism in diagram{[ 2 .. Length( diagram ) ]} do
if not IsEqualForObjects( cat, Range( current_morphism ), base ) then
return [ false, "the given morphisms of the equalizer diagram must have equal ranges" ];
fi;
od;
return [ true ];
end,
compatible_with_congruence_of_morphisms := false,
functorial := "EqualizerFunctorial",
),
EmbeddingOfEqualizer := rec(
filter_list := [ "category", "object", "list_of_morphisms" ],
return_type := "morphism",
input_arguments_names := [ "cat", "Y", "morphisms" ],
output_range_getter_string := "Y",
output_range_getter_preconditions := [ ],
with_given_object_position := "Source",
dual_operation := "ProjectionOntoCoequalizer",
pre_function := "Equalizer",
compatible_with_congruence_of_morphisms := false,
),
EmbeddingOfEqualizerWithGivenEqualizer := rec(
filter_list := [ "category", "object", "list_of_morphisms", "object" ],
return_type := "morphism",
input_arguments_names := [ "cat", "Y", "morphisms", "P" ],
output_source_getter_string := "P",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Y",
output_range_getter_preconditions := [ ],
dual_operation := "ProjectionOntoCoequalizerWithGivenCoequalizer",
compatible_with_congruence_of_morphisms := false,
),
MorphismFromEqualizerToSink := rec(
filter_list := [ "category", "object", "list_of_morphisms" ],
input_arguments_names := [ "cat", "Y", "morphisms" ],
output_range_getter_string := "Range( morphisms[1] )",
output_range_getter_preconditions := [ ],
with_given_object_position := "Source",
dual_operation := "MorphismFromSourceToCoequalizer",
return_type := "morphism",
compatible_with_congruence_of_morphisms := false,
),
MorphismFromEqualizerToSinkWithGivenEqualizer := rec(
filter_list := [ "category", "object", "list_of_morphisms", "object" ],
input_arguments_names := [ "cat", "Y", "morphisms", "P" ],
output_source_getter_string := "P",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Range( morphisms[1] )",
output_range_getter_preconditions := [ ],
dual_operation := "MorphismFromSourceToCoequalizerWithGivenCoequalizer",
return_type := "morphism",
compatible_with_congruence_of_morphisms := false,
),
UniversalMorphismIntoEqualizer := rec(
filter_list := [ "category", "object", "list_of_morphisms", "object", "morphism" ],
input_arguments_names := [ "cat", "Y", "morphisms", "T", "tau" ],
output_source_getter_string := "T",
output_source_getter_preconditions := [ ],
with_given_object_position := "Range",
return_type := "morphism",
dual_operation := "UniversalMorphismFromCoequalizer",
pre_function := function( cat, cobase, diagram, test_object, tau )
local base, current_morphism, current_morphism_position;
if IsEmpty( diagram ) then
return [ true ];
fi;
for current_morphism in diagram{[ 1 .. Length( diagram ) ]} do
if not IsEqualForObjects( cat, Source( current_morphism ), cobase ) then
return [ false, "the given morphisms of the equalizer diagram must have equal sources" ];
fi;
od;
base := Range( diagram[1] );
for current_morphism in diagram{[ 2 .. Length( diagram ) ]} do
if not IsEqualForObjects( cat, Range( current_morphism ), base ) then
return [ false, "the given morphisms of the equalizer diagram must have equal ranges" ];
fi;
od;
for current_morphism_position in [ 1 .. Length( diagram ) ] do
if not IsEqualForObjects( cat, Source( diagram[ current_morphism_position ] ), Range( tau ) ) then
return [ false, Concatenation( "in diagram position ", String( current_morphism_position ), ": source and range are not equal" ) ];
fi;
od;
return [ true ];
end,
compatible_with_congruence_of_morphisms := false,
),
UniversalMorphismIntoEqualizerWithGivenEqualizer := rec(
filter_list := [ "category", "object", "list_of_morphisms", "object", "morphism", "object" ],
input_arguments_names := [ "cat", "Y", "morphisms", "T", "tau", "P" ],
output_source_getter_string := "T",
output_source_getter_preconditions := [ ],
output_range_getter_string := "P",
output_range_getter_preconditions := [ ],
return_type := "morphism",
dual_operation := "UniversalMorphismFromCoequalizerWithGivenCoequalizer",
compatible_with_congruence_of_morphisms := false,
),
IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct := rec(
filter_list := [ "category", "object", "list_of_morphisms" ],
input_arguments_names := [ "cat", "A", "D" ],
return_type := "morphism",
dual_operation := "IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer",
),
IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer := rec(
filter_list := [ "category", "object", "list_of_morphisms" ],
input_arguments_names := [ "cat", "A", "D" ],
return_type := "morphism",
dual_operation := "IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct",
),
FiberProduct := rec(
filter_list := [ "category", "list_of_morphisms" ],
input_arguments_names := [ "cat", "morphisms" ],
dual_operation := "Pushout",
pre_function := function( cat, diagram )
local base, current_morphism;
if IsEmpty( diagram ) then
return [ true ];
fi;
base := Range( diagram[1] );
for current_morphism in diagram{[ 2 .. Length( diagram ) ]} do
if not IsEqualForObjects( cat, Range( current_morphism ), base ) then
return [ false, "the given morphisms of the fiber product diagram must have equal ranges" ];
fi;
od;
return [ true ];
end,
return_type := "object",
compatible_with_congruence_of_morphisms := false,
functorial := "FiberProductFunctorial",
),
ProjectionInFactorOfFiberProduct := rec(
filter_list := [ "category", "list_of_morphisms", "integer" ],
input_arguments_names := [ "cat", "morphisms", "k" ],
output_range_getter_string := "Source( morphisms[k] )",
output_range_getter_preconditions := [ ],
with_given_object_position := "Source",
dual_operation := "InjectionOfCofactorOfPushout",
pre_function := function( cat, diagram, projection_number )
local base, current_morphism;
if projection_number < 1 or projection_number > Length( diagram ) then
return[ false, Concatenation( "there does not exist a ", String( projection_number ), "th projection" ) ];
fi;
base := Range( diagram[1] );
for current_morphism in diagram{[ 2 .. Length( diagram ) ]} do
if not IsEqualForObjects( cat, Range( current_morphism ), base ) then
return [ false, "the given morphisms of the fiber product diagram must have equal ranges" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := false,
),
ProjectionInFactorOfFiberProductWithGivenFiberProduct := rec(
filter_list := [ "category", "list_of_morphisms", "integer", "object" ],
input_arguments_names := [ "cat", "morphisms", "k", "P" ],
output_source_getter_string := "P",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Source( morphisms[k] )",
output_range_getter_preconditions := [ ],
dual_operation := "InjectionOfCofactorOfPushoutWithGivenPushout",
pre_function := function( cat, diagram, projection_number, pullback )
local base, current_morphism;
if projection_number < 1 or projection_number > Length( diagram ) then
return[ false, Concatenation( "there does not exist a ", String( projection_number ), "th projection" ) ];
fi;
base := Range( diagram[1] );
for current_morphism in diagram{[ 2 .. Length( diagram ) ]} do
if not IsEqualForObjects( cat, Range( current_morphism ), base ) then
return [ false, "the given morphisms of the fiber product diagram must have equal ranges" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := false,
),
MorphismFromFiberProductToSink := rec(
filter_list := [ "category", "list_of_morphisms" ],
input_arguments_names := [ "cat", "morphisms" ],
output_range_getter_string := "Range( morphisms[1] )",
output_range_getter_preconditions := [ ],
with_given_object_position := "Source",
dual_operation := "MorphismFromSourceToPushout",
pre_function := function( cat, diagram )
local base, current_morphism;
base := Range( diagram[1] );
for current_morphism in diagram{[ 2 .. Length( diagram ) ]} do
if not IsEqualForObjects( cat, Range( current_morphism ), base ) then
return [ false, "the given morphisms of the fiber product diagram must have equal ranges" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := false,
),
MorphismFromFiberProductToSinkWithGivenFiberProduct := rec(
filter_list := [ "category", "list_of_morphisms", "object" ],
input_arguments_names := [ "cat", "morphisms", "P" ],
output_source_getter_string := "P",
output_source_getter_preconditions := [ ],
output_range_getter_string := "Range( morphisms[1] )",
output_range_getter_preconditions := [ ],
dual_operation := "MorphismFromSourceToPushoutWithGivenPushout",
pre_function := function( cat, diagram, pullback )
local base, current_morphism;
base := Range( diagram[1] );
for current_morphism in diagram{[ 2 .. Length( diagram ) ]} do
if not IsEqualForObjects( cat, Range( current_morphism ), base ) then
return [ false, "the given morphisms of the fiber product diagram must have equal ranges" ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := false,
),
UniversalMorphismIntoFiberProduct := rec(
filter_list := [ "category", "list_of_morphisms", "object", "list_of_morphisms" ],
input_arguments_names := [ "cat", "morphisms", "T", "tau" ],
output_source_getter_string := "T",
output_source_getter_preconditions := [ ],
with_given_object_position := "Range",
dual_operation := "UniversalMorphismFromPushout",
pre_function := function( cat, diagram, test_object, source )
local base, current_morphism, current_morphism_position;
if Length( diagram ) <> Length( source ) then
return [ false, "fiber product diagram and test diagram must have equal length" ];
fi;
if IsEmpty( diagram ) then
return [ true ];
fi;
base := Range( diagram[1] );
for current_morphism in diagram{[ 2 .. Length( diagram ) ]} do
if not IsEqualForObjects( cat, Range( current_morphism ), base ) then
return [ false, "the given morphisms of the fiber product diagram must have equal ranges" ];
fi;
od;
for current_morphism in source do
if not IsEqualForObjects( cat, Source( current_morphism ), test_object ) then
return [ false, "the given morphisms of the test source do not have sources equal to the test object" ];
fi;
od;
for current_morphism_position in [ 1 .. Length( diagram ) ] do
if not IsEqualForObjects( cat, Source( diagram[ current_morphism_position ] ), Range( source[ current_morphism_position ] ) ) then
return [ false, Concatenation( "in diagram position ", String( current_morphism_position ), ": source and range are not equal" ) ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := false,
),
UniversalMorphismIntoFiberProductWithGivenFiberProduct := rec(
filter_list := [ "category", "list_of_morphisms", "object", "list_of_morphisms", "object" ],
input_arguments_names := [ "cat", "morphisms", "T", "tau", "P" ],
output_source_getter_string := "T",
output_source_getter_preconditions := [ ],
output_range_getter_string := "P",
output_range_getter_preconditions := [ ],
dual_operation := "UniversalMorphismFromPushoutWithGivenPushout",
pre_function := function( cat, diagram, test_object, source, pullback )
local base, current_morphism, current_morphism_position;
if Length( diagram ) <> Length( source ) then
return [ false, "fiber product diagram and test diagram must have equal length" ];
fi;
if IsEmpty( diagram ) then
return [ true ];
fi;
base := Range( diagram[1] );
for current_morphism in diagram{[ 2 .. Length( diagram ) ]} do
if not IsEqualForObjects( cat, Range( current_morphism ), base ) then
return [ false, "the given morphisms of the fiber product diagram must have equal ranges" ];
fi;
od;
for current_morphism in source do
if not IsEqualForObjects( cat, Source( current_morphism ), test_object ) then
return [ false, "the given morphisms of the test source do not have sources equal to the test object" ];
fi;
od;
for current_morphism_position in [ 1 .. Length( diagram ) ] do
if not IsEqualForObjects( cat, Source( diagram[ current_morphism_position ] ), Range( source[ current_morphism_position ] ) ) then
return [ false, Concatenation( "in diagram position ", String( current_morphism_position ), ": source and range are not equal" ) ];
fi;
od;
return [ true ];
end,
return_type := "morphism",
compatible_with_congruence_of_morphisms := false,
),
Coequalizer := rec(
filter_list := [ "category", "object", "list_of_morphisms" ],
input_arguments_names := [ "cat", "Y", "morphisms" ],
return_type := "object",
dual_operation := "Equalizer",
pre_function := function( cat, cobase, diagram )
local base, current_morphism;
if IsEmpty( diagram ) then
return [ true ];
fi;
base := Source( diagram[1] );
for current_morphism in diagram{[ 2 .. Length( diagram ) ]} do
if not IsEqualForObjects( cat, Source( current_morphism ), base ) then
return [ false, "the given morphisms of the coequalizer diagram must have equal sources" ];
fi;
od;
for current_morphism in diagram{[ 1 .. Length( diagram ) ]} do
if not IsEqualForObjects( cat, Range( current_morphism ), cobase ) then
return [ false, "the given morphisms of the coequalizer diagram must have equal ranges" ];
fi;
od;
return [ true ];
end,
compatible_with_congruence_of_morphisms := false,
functorial := "CoequalizerFunctorial",
),
ProjectionOntoCoequalizer := rec(
filter_list := [ "category", "object", "list_of_morphisms" ],
return_type := "morphism",
input_arguments_names := [ "cat", "Y", "morphisms" ],
output_source_getter_string := "Y",
output_source_getter_preconditions := [ ],
with_given_object_position := "Range",
--> --------------------
--> maximum size reached
--> --------------------
[ zur Elbe Produktseite wechseln0.73Quellennavigators
Analyse erneut starten
]
|
