| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/GAP/pkg/cap/gap/ (Algebra von RWTH Aachen Version 4.15.1©) Datei vom 22.8.2025 mit Größe 148 kB |
|
Quelle MethodRecord.gi Sprache: unbekannt |
|
|
# 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, Ran return [ false, "some of the morphisms are not compatible with the provided source and range obj 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_linea input_arguments_names := [ "cat", "source", "list_of_ring_elements", "list_of_morphism 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, Ran return [ false, "some of the morphisms are not compatible with the provided source and range obj 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 com 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[ 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 com 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_morphism 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 ) t 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 regar 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", "morp 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 ) return [ false, Concatenation( "in diagram position ", String( current_morphism_position ) fi; od; return [ true ]; end, compatible_with_congruence_of_morphisms := false, ), UniversalMorphismIntoEqualizerWithGivenEqualizer := rec( filter_list := [ "category", "object", "list_of_morphisms", "object", "morphism", "objec 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, ), IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectP filter_list := [ "category", "object", "list_of_morphisms" ], input_arguments_names := [ "cat", "A", "D" ], return_type := "morphism", dual_operation := "IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFro ), IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqu filter_list := [ "category", "object", "list_of_morphisms" ], input_arguments_names := [ "cat", "A", "D" ], return_type := "morphism", dual_operation := "IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesO ), 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 pro 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 pro 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 obje fi; od; for current_morphism_position in [ 1 .. Length( diagram ) ] do if not IsEqualForObjects( cat, Source( diagram[ current_morphism_position ] ), Range( sour return [ false, Concatenation( "in diagram position ", String( current_morphism_position ) 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", "objec 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 obje fi; od; for current_morphism_position in [ 1 .. Length( diagram ) ] do if not IsEqualForObjects( cat, Source( diagram[ current_morphism_position ] ), Range( sour return [ false, Concatenation( "in diagram position ", String( current_morphism_position ) 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 --> -------------------- [ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ] |
2026-03-28