1#############################################################################
2##
3##                                               CAP package
4##
5##  Copyright 2013, Sebastian Gutsche, TU Kaiserslautern
6##                  Sebastian Posur,   RWTH Aachen
7##
8#############################################################################
9
10######################################
11##
12## Reps, types, stuff.
13##
14######################################
15
16DeclareRepresentation( "IsCapCategoryMorphismRep",
17                       IsAttributeStoringRep and IsCapCategoryMorphism,
18                       [ ] );
19
20BindGlobal( "TheFamilyOfCapCategoryMorphisms",
21        NewFamily( "TheFamilyOfCapCategoryMorphisms" ) );
22
23BindGlobal( "TheTypeOfCapCategoryMorphisms",
24        NewType( TheFamilyOfCapCategoryMorphisms,
25                IsCapCategoryMorphismRep ) );
26
27######################################
28##
29## Properties logic
30##
31######################################
32#
33# InstallTrueMethod( IsSplitMonomorphism and IsSplitEpimorphism, IsCapCategoryMorphism and IsIsomorphism );
34#
35# InstallTrueMethod( IsAutomorphism, IsCapCategoryMorphism and IsOne );
36#
37# InstallTrueMethod( IsIsomorphism and IsEndomorphism, IsCapCategoryMorphism and IsAutomorphism );
38#
39# InstallTrueMethod( IsMonomorphism, IsCapCategoryMorphism and IsSplitMonomorphism );
40#
41# InstallTrueMethod( IsEpimorphism, IsCapCategoryMorphism and IsSplitEpimorphism );
42#
43# InstallTrueMethod( IsIsomorphism, IsMonomorphism and IsEpimorphism and IsAbelianCategory );#TODO: weaker?
44
45#######################################
46##
47## Technical implications
48##
49#######################################
50
51InstallValue( PROPAGATION_LIST_FOR_EQUAL_MORPHISMS,
52              [
53                 "IsMonomorphism",
54                 "IsEpimorphism",
55                 "IsIsomorphism",
56                 "IsEndomorphism",
57                 "IsAutomorphism",
58                 "IsSplitMonomorphism",
59                 "IsSplitEpimorphism",
60                 "IsOne",
61                 "IsIdempotent",
62                 "IsZero",
63                 # ..
64              ] );
65
66######################################
67##
68## Operations
69##
70######################################
71
72InstallMethod( Add,
73               [ IsCapCategory, IsCapCategoryMorphism ],
74
75  function( category, morphism )
76    local filter;
77
78    filter := MorphismFilter( category );
79
80    if not filter( morphism ) then
81
82        SetFilterObj( morphism, filter );
83
84    fi;
85
86    AddObject( category, Source( morphism ) );
87
88    AddObject( category, Range( morphism ) );
89
90    if category!.predicate_logic then
91
92        INSTALL_TODO_FOR_LOGICAL_THEOREMS( "Source", [ morphism ], Source( morphism ), category );
93
94        INSTALL_TODO_FOR_LOGICAL_THEOREMS( "Range", [ morphism ], Range( morphism ), category );
95
96    fi;
97
98    if HasCapCategory( morphism ) then
99
100        if IsIdenticalObj( CapCategory( morphism ), category ) then
101
102            return;
103
104        else
105
106            Error(
107                Concatenation(
108                    "a morphism that lies in the CAP-category with the name\n",
109                    Name( CapCategory( morphism ) ),
110                    "\n",
111                    "was tried to be added to a different CAP-category with the name\n",
112                    Name( category ), ".\n",
113                    "(Please note that it is possible for different CAP-categories to have the same name)"
114                )
115            );
116
117        fi;
118
119    fi;
120
121    SetCapCategory( morphism, category );
122
123end );
124
125InstallMethod( AddMorphism,
126               [ IsCapCategory, IsCapCategoryMorphism ],
127
128  function( category, morphism )
129
130    Add( category, morphism );
131
132end );
133
134InstallMethod( AddMorphism,
135               [ IsCapCategory, IsAttributeStoringRep ],
136
137  function( category, morphism )
138
139    SetFilterObj( morphism, IsCapCategoryMorphism );
140
141    Add( category, morphism );
142
143end );
144
145##
146InstallMethod( IsZero,
147               [ IsCapCategoryMorphism ],
148
149IsZeroForMorphisms );
150
151##
152InstallMethod( \+,
153               [ IsCapCategoryMorphism, IsCapCategoryMorphism ],
154
155AdditionForMorphisms );
156
157##
158InstallMethod( \-,
159               [ IsCapCategoryMorphism, IsCapCategoryMorphism ],
160
161SubtractionForMorphisms );
162
163##
164InstallMethod( AdditiveInverse,
165                  [ IsCapCategoryMorphism ],
166
167AdditiveInverseForMorphisms );
168
169##
170InstallMethod( \*,
171               [ IsRingElement, IsCapCategoryMorphism ],
172
173MultiplyWithElementOfCommutativeRingForMorphisms );
174
175##
176InstallMethod( \*,
177               [ IsCapCategoryMorphism, IsRingElement ],
178
179  function( mor, r )
180
181    return MultiplyWithElementOfCommutativeRingForMorphisms( r, mor );
182
183end );
184
185##
186InstallMethod( IsEqualForCacheForMorphisms,
187               [ IsCapCategoryMorphism, IsCapCategoryMorphism ],
188
189  IsEqualForCache );
190
191
192InstallMethod( AddMorphismRepresentation,
193               [ IsCapCategory, IsObject ],
194
195  function( category, representation )
196
197    category!.morphism_representation := representation;
198    category!.morphism_type := NewType( TheFamilyOfCapCategoryMorphisms, representation and MorphismFilter( category ) and IsCapCategoryMorphismRep );
199
200end );
201
202InstallMethod( RandomMorphismWithFixedSourceAndRange,
203    [ IsCapCategoryObject, IsCapCategoryObject, IsInt ], RandomMorphismWithFixedSourceAndRangeByInteger );
204InstallMethod( RandomMorphismWithFixedSourceAndRange,
205    [ IsCapCategoryObject, IsCapCategoryObject, IsList ], RandomMorphismWithFixedSourceAndRangeByList );
206
207InstallMethod( RandomMorphismWithFixedSource,
208    [ IsCapCategoryObject, IsInt ], RandomMorphismWithFixedSourceByInteger );
209InstallMethod( RandomMorphismWithFixedSource,
210    [ IsCapCategoryObject, IsList ], RandomMorphismWithFixedSourceByList );
211
212InstallMethod( RandomMorphismWithFixedRange,
213    [ IsCapCategoryObject, IsInt ], RandomMorphismWithFixedRangeByInteger );
214InstallMethod( RandomMorphismWithFixedRange,
215    [ IsCapCategoryObject, IsList ], RandomMorphismWithFixedRangeByList );
216
217InstallMethod( RandomMorphism,
218    [ IsCapCategory, IsInt ], RandomMorphismByInteger );
219InstallMethod( RandomMorphism,
220    [ IsCapCategory, IsList ], RandomMorphismByList );
221
222
223InstallGlobalFunction( ObjectifyMorphismForCAPWithAttributes,
224
225  function( arg_list... )
226    local category, morphism;
227
228    category := arg_list[ 2 ];
229    arg_list[ 2 ] := category!.morphism_type;
230    Append( arg_list, [ CapCategory, category ] );
231    CallFuncList( ObjectifyWithAttributes, arg_list );
232
233    if category!.predicate_logic then
234        morphism := arg_list[ 1 ];
235        INSTALL_TODO_FOR_LOGICAL_THEOREMS( "Source", [ morphism ], Source( morphism ), category );
236        INSTALL_TODO_FOR_LOGICAL_THEOREMS( "Range", [ morphism ], Range( morphism ), category );
237    fi;
238
239end );
240
241######################################
242##
243## Morphism equality functions
244##
245######################################
246
247# This method should usually not be selected when the two morphisms belong to the same category
248InstallMethod( IsEqualForMorphisms,
249                [ IsCapCategoryMorphism, IsCapCategoryMorphism ],
250
251  function( morphism_1, morphism_2 )
252
253    if not HasCapCategory( morphism_1 ) then
254        Error( Concatenation( "the morphism \"", String( morphism_1 ), "\" has no CAP category" ) );
255    fi;
256    if not HasCapCategory( morphism_2 ) then
257        Error( Concatenation( "the morphism \"", String( morphism_2 ), "\" has no CAP category" ) );
258    fi;
259
260    if not IsIdenticalObj( CapCategory( morphism_1 ), CapCategory( morphism_2 ) ) then
261        Error( Concatenation( "the morphism \"", String( morphism_1 ), "\" and the morphism \"", String( morphism_2 ), "\" do not belong to the same CAP category" ) );
262    else
263        Error( Concatenation( "the morphism \"", String( morphism_1 ), "\" and the morphism \"", String( morphism_2 ), "\" belong to the same CAP category, but no specific method IsEqualForMorphisms is installed. Maybe you forgot to finalize the category?" ) );
264    fi;
265
266end );
267
268# This method should usually not be selected when the two morphisms belong to the same category
269InstallMethod( IsCongruentForMorphisms,
270                [ IsCapCategoryMorphism, IsCapCategoryMorphism ],
271
272  function( morphism_1, morphism_2 )
273
274    if not HasCapCategory( morphism_1 ) then
275        Error( Concatenation( "the morphism \"", String( morphism_1 ), "\" has no CAP category" ) );
276    fi;
277    if not HasCapCategory( morphism_2 ) then
278        Error( Concatenation( "the morphism \"", String( morphism_2 ), "\" has no CAP category" ) );
279    fi;
280
281    if not IsIdenticalObj( CapCategory( morphism_1 ), CapCategory( morphism_2 ) ) then
282        Error( Concatenation( "the morphism \"", String( morphism_1 ), "\" and the morphism \"", String( morphism_2 ), "\" do not belong to the same CAP category" ) );
283    else
284        Error( Concatenation( "the morphism \"", String( morphism_1 ), "\" and the morphism \"", String( morphism_2 ), "\" belong to the same CAP category, but no specific method IsCongruentForMorphisms is installed. Maybe you forgot to finalize the category?" ) );
285    fi;
286
287end );
288
289##
290InstallMethod( \=,
291               [ IsCapCategoryMorphism, IsCapCategoryMorphism ],
292
293  function( morphism_1, morphism_2 )
294
295    if CapCategory( morphism_1 )!.input_sanity_check_level > 0 or CapCategory( morphism_2 )!.input_sanity_check_level > 0  then
296        if not IsIdenticalObj( CapCategory( morphism_1 ), CapCategory( morphism_2 ) ) then
297            Error( Concatenation( "the morphism \"", String( morphism_1 ), "\" and the morphism \"", String( morphism_2 ), "\" do not belong to the same CAP category" ) );
298        fi;
299    fi;
300    if not IsEqualForObjects( Source( morphism_1 ), Source( morphism_2 ) ) or not IsEqualForObjects( Range( morphism_1 ), Range( morphism_2 ) ) then
301
302        return false;
303
304    fi;
305
306    return IsCongruentForMorphisms( morphism_1, morphism_2 );
307
308end );
309
310##
311InstallGlobalFunction( INSTALL_TODO_LIST_FOR_EQUAL_MORPHISMS,
312
313  function( morphism_1, morphism_2 )
314    local category, i, entry;
315
316    category := CapCategory( morphism_1 );
317
318    for i in PROPAGATION_LIST_FOR_EQUAL_MORPHISMS do
319
320        AddToToDoList( ToDoListEntryForEqualAttributes( morphism_1, i, morphism_2, i ) );
321
322    od;
323
324    if IsBound( category!.PROPAGATION_LIST_FOR_EQUAL_MORPHISMS ) then
325
326        for i in category!.PROPAGATION_LIST_FOR_EQUAL_MORPHISMS do
327
328            AddToToDoList( ToDoListEntryForEqualAttributes( morphism_1, i, morphism_2, i ) );
329
330        od;
331
332    fi;
333
334end );
335
336##
337InstallMethod( AddPropertyToMatchAtIsCongruentForMorphisms,
338               [ IsCapCategory, IsString ],
339
340  function( category, name )
341
342    if not IsBound( category!.PROPAGATION_LIST_FOR_EQUAL_MORPHISMS ) then
343
344        category!.PROPAGATION_LIST_FOR_EQUAL_MORPHISMS := [ ];
345
346    fi;
347
348    if Position( category!.PROPAGATION_LIST_FOR_EQUAL_MORPHISMS, name ) = fail then
349
350        Add( category!.PROPAGATION_LIST_FOR_EQUAL_MORPHISMS, name );
351
352    fi;
353
354end );
355
356
357######################################
358##
359## Convenience method
360##
361######################################
362
363## FIXME: This might be dangerous
364##
365# InstallMethod( Zero,
366#                [ IsCapCategoryMorphism ],
367#
368#   function( mor )
369#
370#     return ZeroMorphism( Source( mor ), Range( mor ) );
371#
372# end );
373
374##
375InstallMethod( \-,
376               [ IsCapCategoryMorphism, IsCapCategoryMorphism ],
377
378  function( alpha, beta )
379
380    return alpha + AdditiveInverse( beta );
381
382end );
383
384##
385InstallMethod( PreCompose,
386               [ IsList ],
387
388  function( morphism_list )
389    local length, result_morphism, i;
390
391    length := Length( morphism_list );
392
393    if length = 0 then
394
395      Error( "non-empty list expected" );
396
397    fi;
398
399    result_morphism := morphism_list[1];
400
401    for i in [ 2 .. length ] do
402
403      result_morphism := PreCompose( result_morphism, morphism_list[i] );
404
405    od;
406
407    return result_morphism;
408
409end );
410
411##
412InstallMethod( PostCompose,
413               [ IsList ],
414
415  function( morphism_list )
416    local length, result_morphism, i;
417
418    length := Length( morphism_list );
419
420    if length = 0 then
421
422      Error( "non-empty list expected" );
423
424    fi;
425
426    result_morphism := morphism_list[1];
427
428    for i in [ 2 .. length ] do
429
430      result_morphism := PostCompose( result_morphism, morphism_list[i] );
431
432    od;
433
434    return result_morphism;
435
436end );
437
438##
439InstallMethod( HomomorphismStructureOnMorphisms,
440               [ IsCapCategoryMorphism, IsCapCategoryMorphism ],
441
442  function( alpha, beta )
443
444    return HomomorphismStructureOnMorphismsWithGivenObjects(
445             HomomorphismStructureOnObjects( Range( alpha ), Source( beta ) ),
446             alpha, beta,
447             HomomorphismStructureOnObjects( Source( alpha ), Range( beta ) )
448           );
449
450end );
451
452##
453InstallMethod( SolveLinearSystemInAbCategory,
454               [ IsList, IsList, IsList ],
455
456  function( left_coeffs, right_coeffs, right_side )
457
458    return SolveLinearSystemInAbCategoryOp( left_coeffs, right_coeffs, right_side, CapCategory( right_side[1] ) );
459
460end );
461
462######################################
463##
464## Morphism transport
465##
466######################################
467
468## mor: x -> y
469## equality_source: x -> x'
470## equality_range: y -> y'
471## TransportHom( mor, equality_source, equality_range ): x' -> y'
472##
473InstallMethodWithCacheFromObject( TransportHom,
474                                  [ IsCapCategoryMorphism, IsCapCategoryMorphism, IsCapCategoryMorphism ],
475
476  function( mor, equality_source, equality_range )
477
478    return PreCompose(
479             Inverse( equality_source ),
480             PreCompose( mor, equality_range )
481           );
482
483end );
484
485###########################
486##
487## IsWellDefined
488##
489###########################
490
491##
492InstallMethod( IsWellDefinedForMorphisms,
493               [ IsCapCategoryMorphism ],
494
495  IsWellDefined
496);
497
498###########################
499##
500## Print
501##
502###########################
503
504##
505InstallGlobalFunction( CAP_INTERNAL_CREATE_MORPHISM_PRINT,
506
507  function( )
508    local print_graph, morphism_function;
509
510    morphism_function := function( object )
511      local string;
512
513        string := "morphism in ";
514
515        Append( string, Name( CapCategory( object ) ) );
516
517        return string;
518
519    end;
520
521    print_graph := CreatePrintingGraph( IsCapCategoryMorphism and HasCapCategory, morphism_function );
522
523    AddRelationToGraph( print_graph,
524                        rec( Source := [ rec( Conditions := "IsIsomorphism",
525                                              PrintString := "iso",
526                                              Adjective := true,
527                                              NoSepString := true ) ],
528                             Range := [ rec( Conditions := "IsSplitMonomorphism",
529                                             PrintString := "split mono",
530                                             TypeOfView := "ViewObj",
531                                             ComputeLevel := "AllWithCompute",
532                                             Adjective := true,
533                                              NoSepString := true ),
534                                        rec( Conditions := "IsSplitEpimorphism",
535                                             PrintString := "split epi",
536                                             Adjective := true,
537                                              NoSepString := true ) ] ) );
538
539    AddRelationToGraph( print_graph,
540                        rec( Source := [ rec( Conditions := "IsOne",
541                                              PrintString := "identity",
542                                              Adjective := true ) ],
543                             Range := [ rec( Conditions := "IsAutomorphism",
544                                             PrintString := "auto",
545                                             Adjective := true,
546                                             NoSepString := true ),
547                                        "IsIsomorphism" ] ) );
548
549    AddRelationToGraph( print_graph,
550                        rec( Source := [ "IsAutomorphism" ],
551                             Range := [ "IsIsomorphism",
552                                        rec( Conditions := "IsEndomorphism",
553                                             PrintString := "endo",
554                                             Adjective := true,
555                                             NoSepString := true) ] ) );
556
557    AddRelationToGraph( print_graph,
558                        rec( Source := [ "IsSplitMonomorphism" ],
559                             Range := [ rec( Conditions := "IsMonomorphism",
560                                             PrintString := "mono",
561                                             Adjective := true,
562                                             NoSepString := true ) ] ) );
563
564    AddRelationToGraph( print_graph,
565                        rec( Source := [ "IsSplitEpimorphism" ],
566                             Range := [ rec( Conditions := "IsEpimorphism",
567                                             PrintString := "epi",
568                                             Adjective := true,
569                                             NoSepString := true ) ] ) );
570
571    AddNodeToGraph( print_graph,
572                    rec( Conditions := "IsZeroForMorphisms",
573                         PrintString := "zero",
574                         Adjective := true ) );
575
576    InstallPrintFunctionsOutOfPrintingGraph( print_graph, -1 );
577
578end );
579
580CAP_INTERNAL_CREATE_MORPHISM_PRINT( );
581
582InstallMethod( String,
583               [ IsCapCategoryMorphism and HasCapCategory ],
584
585  function( morphism )
586
587    return Concatenation( "A morphism in ", Name( CapCategory( morphism ) ) );
588
589end );
590