1#############################################################################
2##
3##                  GeneralizedMorphismsForCAP package
4##
5##  Copyright 2015, Sebastian Gutsche, TU Kaiserslautern
6##                  Sebastian Posur,   RWTH Aachen
7##
8#############################################################################
9
10####################################
11##
12## Installer
13##
14####################################
15
16##
17InstallGlobalFunction( INSTALL_FUNCTIONS_FOR_GENERALIZED_MORPHISM_CATEGORY_BY_COSPANS,
18
19  function( category )
20    local entry, underlying_honest_category;
21
22    underlying_honest_category := UnderlyingHonestCategory( category );
23
24    ##
25    AddIsEqualForCacheForObjects( category, IsIdenticalObj );
26
27    ##
28    AddIsEqualForCacheForMorphisms( category, IsIdenticalObj );
29
30    AddIsEqualForObjects( category,
31
32      function( object_1, object_2 )
33
34          return IsEqualForObjects( UnderlyingHonestObject( object_1 ), UnderlyingHonestObject( object_2 ) );
35
36    end );
37
38    AddIsCongruentForMorphisms( category,
39
40      function( morphism1, morphism2 )
41        local arrow_tuple, pullback_diagram1, pullback_diagram2, subobject1, subobject2;
42
43        arrow_tuple := [ Arrow( morphism1 ), ReversedArrow( morphism1 ) ];
44
45        pullback_diagram1 := [ ProjectionInFactorOfFiberProduct( arrow_tuple, 1 ), ProjectionInFactorOfFiberProduct( arrow_tuple, 2 ) ];
46
47        arrow_tuple := [ Arrow( morphism2 ), ReversedArrow( morphism2 ) ];
48
49        pullback_diagram2 := [ ProjectionInFactorOfFiberProduct( arrow_tuple, 1 ), ProjectionInFactorOfFiberProduct( arrow_tuple, 2 ) ];
50
51        subobject1 := UniversalMorphismIntoDirectSum( pullback_diagram1 );
52
53        subobject2 := UniversalMorphismIntoDirectSum( pullback_diagram2 );
54
55        ## TODO: added more logic to make the following line obsolete
56        Assert( 4, IsMonomorphism( subobject1 ) );
57        SetIsMonomorphism( subobject1, true );
58
59        Assert( 4, IsMonomorphism( subobject2 ) );
60        SetIsMonomorphism( subobject2, true );
61
62        return IsEqualAsSubobjects( subobject1, subobject2 );
63
64    end );
65
66    ## PreCompose
67
68
69    AddPreCompose( category, [
70
71      [ function( morphism1, morphism2 )
72          local pushout_diagram, injection_left, injection_right;
73
74          pushout_diagram := [ ReversedArrow( morphism1 ), Arrow( morphism2 ) ];
75
76          injection_left := InjectionOfCofactorOfPushout( pushout_diagram, 1 );
77
78          injection_right := InjectionOfCofactorOfPushout( pushout_diagram, 2 );
79
80          return GeneralizedMorphismByCospan( PreCompose( Arrow( morphism1 ), injection_left ), PreCompose( ReversedArrow( morphism2 ), injection_right ) );
81
82      end, [ ] ],
83
84      [ function( morphism1, morphism2 )
85          local arrow, reversed_arrow;
86
87          arrow := PreCompose( Arrow( morphism1 ), Arrow( morphism2 ) );
88
89          return AsGeneralizedMorphismByCospan( arrow );
90
91      end, [ HasIdentityAsReversedArrow, HasIdentityAsReversedArrow ] ],
92
93      [ function( morphism1, morphism2 )
94          local arrow;
95
96          arrow := PreCompose( Arrow( morphism1 ), Arrow( morphism2 ) );
97
98          return GeneralizedMorphismByCospan( arrow, ReversedArrow( morphism2 ) );
99
100      end, [ HasIdentityAsReversedArrow, ] ] ] );
101
102
103    ## AdditionForMorphisms
104
105    AddAdditionForMorphisms( category, [
106
107      [ function( morphism1, morphism2 )
108          local pushout_diagram, pushout_left, pushout_right, arrow, reversed_arrow;
109
110          pushout_diagram := [ ReversedArrow( morphism1 ), ReversedArrow( morphism2 ) ];
111
112          pushout_left := InjectionOfCofactorOfPushout( pushout_diagram, 1 );
113
114          pushout_right := InjectionOfCofactorOfPushout( pushout_diagram, 2 );
115
116          arrow := AdditionForMorphisms( PreCompose( Arrow( morphism1 ), pushout_left ), PreCompose( Arrow( morphism2 ), pushout_right ) );
117
118          reversed_arrow := PreCompose( pushout_diagram[ 1 ], pushout_left );
119
120          return GeneralizedMorphismByCospan( arrow, reversed_arrow );
121
122      end, [ ] ],
123
124      [ function( morphism1, morphism2 )
125
126          return AsGeneralizedMorphismByCospan( AdditionForMorphisms( Arrow( morphism1 ),  Arrow( morphism2 ) ) );
127
128      end, [ HasIdentityAsReversedArrow, HasIdentityAsReversedArrow ] ] ] );
129
130    AddAdditiveInverseForMorphisms( category, [
131
132      [ function( morphism )
133
134         return GeneralizedMorphismByCospan( AdditiveInverseForMorphisms( Arrow( morphism ) ), ReversedArrow( morphism ) );
135
136      end, [ ] ],
137
138      [ function( morphism )
139
140          return AsGeneralizedMorphismByCospan( AdditiveInverseForMorphisms( Arrow( morphism ) ) );
141
142      end, [ HasIdentityAsReversedArrow ] ] ] );
143
144    AddZeroMorphism( category,
145
146      function( obj1, obj2 )
147        local morphism;
148
149        morphism := ZeroMorphism( UnderlyingHonestObject( obj1 ), UnderlyingHonestObject( obj2 ) );
150
151        return AsGeneralizedMorphismByCospan( morphism );
152
153    end );
154
155
156    ## identity
157
158    AddIdentityMorphism( category,
159
160      function( generalized_object )
161        local identity_morphism;
162
163        identity_morphism := IdentityMorphism( UnderlyingHonestObject( generalized_object ) );
164
165        return AsGeneralizedMorphismByCospan( identity_morphism );
166
167    end );
168
169    if CurrentOperationWeight( underlying_honest_category!.derivations_weight_list, "IsWellDefinedForObjects" ) < infinity then
170
171        AddIsWellDefinedForObjects( category,
172
173          function( object )
174
175              return IsWellDefined( UnderlyingHonestObject( object ) );
176
177          end );
178
179    fi;
180
181    if CurrentOperationWeight( underlying_honest_category!.derivations_weight_list, "IsWellDefinedForMorphisms" ) < infinity then
182
183        AddIsWellDefinedForMorphisms( category,
184
185          function( generalized_morphism )
186            local category;
187
188            category := CapCategory( Arrow( generalized_morphism ) );
189
190            if not ForAll( [ Arrow( generalized_morphism ), ReversedArrow( generalized_morphism ) ],
191                        x -> IsIdenticalObj( CapCategory( x ), category ) ) then
192
193              return false;
194
195            fi;
196
197            if not ( ForAll( [ Arrow( generalized_morphism ), ReversedArrow( generalized_morphism ) ],
198                    IsWellDefined ) ) then
199
200              return false;
201
202            fi;
203
204            return true;
205
206        end );
207
208    fi;
209
210    return;
211
212end );
213
214####################################
215##
216## Constructors
217##
218####################################
219
220##
221InstallMethod( GeneralizedMorphismCategoryByCospans,
222               [ IsCapCategory ],
223
224  function( category )
225    local name, generalized_morphism_category, category_weight_list, i, preconditions;
226
227    if not IsFinalized( category ) then
228
229        Error( "category must be finalized" );
230
231        return;
232
233    elif not ( HasIsAbelianCategory( category ) and IsAbelianCategory( category ) ) then
234
235        Error( "the category must be abelian" );
236
237        return;
238
239    fi;
240
241    preconditions := [ "IsEqualAsSubobjects",
242                       "IsEqualAsFactorobjects",
243                       "LiftAlongMonomorphism",
244                       "ColiftAlongEpimorphism",
245                       "PreCompose",
246                       "IdentityMorphism",
247                       "FiberProduct",
248                       "Pushout",
249                       "ProjectionInFactorOfFiberProduct",
250                       "InjectionOfCofactorOfPushout",
251                       "AdditionForMorphisms",
252                       "CoastrictionToImage",
253                       "ImageEmbedding" ];
254
255    category_weight_list := category!.derivations_weight_list;
256
257    for i in preconditions do
258
259        if CurrentOperationWeight( category_weight_list, i ) = infinity then
260
261            Error( Concatenation( "category must be able to compute ", i ) );
262            return;
263
264        fi;
265
266    od;
267
268    name := Name( category );
269
270    name := Concatenation( "Generalized morphism category of ", name, " by cospan" );
271
272    generalized_morphism_category := CreateCapCategory( name );
273
274    AddObjectRepresentation( generalized_morphism_category, IsGeneralizedMorphismCategoryByCospansObject );
275
276    AddMorphismRepresentation( generalized_morphism_category, IsGeneralizedMorphismByCospan );
277
278    generalized_morphism_category!.predicate_logic := category!.predicate_logic;
279
280    SetUnderlyingHonestCategory( generalized_morphism_category, category );
281
282    INSTALL_FUNCTIONS_FOR_GENERALIZED_MORPHISM_CATEGORY_BY_COSPANS( generalized_morphism_category );
283
284    SetIsEnrichedOverCommutativeRegularSemigroup( generalized_morphism_category, true );
285
286    SetFilterObj( generalized_morphism_category, WasCreatedAsGeneralizedMorphismCategoryByCospans );
287
288    AddPredicateImplicationFileToCategory( generalized_morphism_category,
289      Filename(
290        DirectoriesPackageLibrary( "GeneralizedMorphismsForCAP", "LogicForGeneralizedMorphismCategory" ),
291        "PredicateImplicationsForGeneralizedMorphismCategory.tex" )
292    );
293
294    Finalize( generalized_morphism_category );
295
296    return generalized_morphism_category;
297
298end );
299
300InstallMethod( GeneralizedMorphismByCospansObject,
301               [ IsCapCategoryObject ],
302
303  function( object )
304    local gen_object, generalized_category;
305
306    generalized_category := GeneralizedMorphismCategoryByCospans( CapCategory( object ) );
307
308    gen_object := rec( );
309
310    ObjectifyObjectForCAPWithAttributes( gen_object, generalized_category,
311                             UnderlyingHonestObject, object );
312
313    return gen_object;
314
315end );
316
317##
318InstallMethodWithCacheFromObject( GeneralizedMorphismByCospan,
319                                  [ IsCapCategoryMorphism, IsCapCategoryMorphism ],
320
321  function( arrow, reversed_arrow )
322    local generalized_morphism, generalized_category;
323
324    if not IsEqualForObjects( Range( arrow ), Range( reversed_arrow ) ) then
325
326        Error( "Ranges of morphisms must coincide" );
327
328    fi;
329
330    generalized_category := GeneralizedMorphismCategoryByCospans( CapCategory( arrow ) );
331
332    generalized_morphism := rec( );
333
334    ObjectifyMorphismForCAPWithAttributes( generalized_morphism, generalized_category,
335                             Source, GeneralizedMorphismByCospansObject( Source( arrow ) ),
336                             Range, GeneralizedMorphismByCospansObject( Source( reversed_arrow ) ),
337                             Arrow, arrow,
338                             ReversedArrow, reversed_arrow );
339
340    return generalized_morphism;
341
342end );
343
344##
345InstallMethod( AsGeneralizedMorphismByCospan,
346               [ IsCapCategoryMorphism ],
347
348  function( arrow )
349    local generalized_morphism;
350
351    generalized_morphism := GeneralizedMorphismByCospan( arrow, IdentityMorphism( Range( arrow ) ) );
352
353    SetIsHonest( generalized_morphism, true );
354
355    SetHasIdentityAsReversedArrow( generalized_morphism, true );
356
357    return generalized_morphism;
358
359end );
360
361####################################
362##
363## Constructors of lifts of exact functors
364##
365####################################
366
367##
368InstallMethod( AsGeneralizedMorphismByCospan,
369        [ IsCapFunctor, IsString ],
370
371  function( F, name )
372    local A, B, gmcF;
373
374    A := GeneralizedMorphismCategoryByCospans( AsCapCategory( Source( F ) ) );
375    B := GeneralizedMorphismCategoryByCospans( AsCapCategory( Range( F ) ) );
376
377    gmcF := CapFunctor( name, A, B );
378
379    AddObjectFunction( gmcF,
380            function( obj )
381              return GeneralizedMorphismByCospansObject( ApplyFunctor( F, UnderlyingHonestObject( obj ) ) );
382            end );
383
384    AddMorphismFunction( gmcF,
385            function( new_source, mor, new_range )
386              return GeneralizedMorphismByCospan( ApplyFunctor( F, Arrow( mor ) ), ApplyFunctor( F, ReversedArrow( mor ) ) );
387            end );
388
389    return gmcF;
390
391end );
392
393##
394InstallMethod( AsGeneralizedMorphismByCospan,
395        [ IsCapFunctor ],
396
397  function( F )
398    local name;
399
400    name := "GeneralizedMorphismByCospan version of ";
401    name := Concatenation( name, Name( F ) );
402
403    return AsGeneralizedMorphismByCospan( F, name );
404
405end );
406
407#################################
408##
409## Additional methods
410##
411#################################
412
413InstallMethod( HasIdentityAsReversedArrow,
414               [ IsGeneralizedMorphismByCospan ],
415
416  function( morphism )
417    local reversed_arrow;
418
419    reversed_arrow := ReversedArrow( morphism );
420
421    if not IsEqualForObjects( Source( reversed_arrow ), Range( reversed_arrow ) ) then
422
423        return false;
424
425    fi;
426
427    return IsCongruentForMorphisms( reversed_arrow, IdentityMorphism( Source( reversed_arrow ) ) );
428
429end );
430
431InstallMethod( NormalizedCospanTuple,
432               [ IsGeneralizedMorphismByCospan ],
433
434  function( morphism )
435    local arrow_tuple, pullback_diagram;
436
437    arrow_tuple := [ Arrow( morphism ), ReversedArrow( morphism ) ];
438
439    pullback_diagram := [ ProjectionInFactorOfFiberProduct( arrow_tuple, 1 ), ProjectionInFactorOfFiberProduct( arrow_tuple, 2 ) ];
440
441    return [ InjectionOfCofactorOfPushout( pullback_diagram, 1 ), InjectionOfCofactorOfPushout( pullback_diagram, 2 ) ];
442
443end );
444
445InstallMethod( NormalizedCospan,
446               [ IsGeneralizedMorphismByCospan ],
447
448  function( morphism )
449
450    return CallFuncList( GeneralizedMorphismByCospan, NormalizedCospanTuple( morphism ) );
451
452end );
453
454InstallMethod( PseudoInverse,
455               [ IsGeneralizedMorphismByCospan ],
456
457  function( morphism )
458
459    return GeneralizedMorphismByCospan( ReversedArrow( morphism ), Arrow( morphism ) );
460
461end );
462
463InstallMethod( GeneralizedInverseByCospan,
464               [ IsCapCategoryMorphism ],
465
466  function( morphism )
467
468    return GeneralizedMorphismByCospan( IdentityMorphism( Range( morphism ) ), morphism );
469
470end );
471
472InstallMethod( HonestRepresentative,
473               [ IsGeneralizedMorphismByCospan ],
474
475  function( generalized_morphism )
476    local normalization;
477
478    normalization := NormalizedCospanTuple( generalized_morphism );
479
480    return PreCompose( normalization[ 1 ], Inverse( normalization[ 2 ] ) );
481
482end );
483
484##
485InstallMethod( HasFullCodomain,
486               [ IsGeneralizedMorphismByCospan ],
487
488  function( generalized_morphism )
489
490    return IsMonomorphism( ReversedArrow( generalized_morphism ) );
491
492end );
493
494##
495InstallMethod( HasFullDomain,
496               [ IsGeneralizedMorphismByCospan ],
497
498  function( generalized_morphism )
499    local cokernel_projection;
500
501    cokernel_projection := CokernelProjection( ReversedArrow( generalized_morphism ) );
502
503    return IsZeroForMorphisms( PreCompose( Arrow( generalized_morphism ), cokernel_projection ) );
504
505end );
506
507InstallMethodWithCacheFromObject( GeneralizedMorphismFromFactorToSubobjectByCospan,
508                              [ IsCapCategoryMorphism, IsCapCategoryMorphism ],
509
510  function( factor, subobject )
511    local pushout_diagram;
512
513    factor := AsGeneralizedMorphismByCospan( factor );
514
515    subobject := AsGeneralizedMorphismByCospan( subobject );
516
517    return PreCompose( PseudoInverse( factor ), PseudoInverse( subobject ) );
518
519end );
520
521InstallMethod( IdempotentDefinedBySubobjectByCospan,
522              [ IsCapCategoryMorphism ],
523
524  function( subobject )
525    local generalized;
526
527    generalized := AsGeneralizedMorphismByCospan( subobject );
528
529    return PreCompose( PseudoInverse( generalized ), generalized );
530
531end );
532
533InstallMethod( IdempotentDefinedByFactorobjectByCospan,
534              [ IsCapCategoryMorphism ],
535
536  function( factorobject )
537
538    return GeneralizedMorphismByCospan( factorobject, factorobject );
539
540end );
541
542InstallMethod( GeneralizedInverseByCospan,
543              [ IsCapCategoryMorphism ],
544
545  function( morphism )
546
547    return PseudoInverse( AsGeneralizedMorphismByCospan( morphism ) );
548
549end );
550
551##
552InstallMethodWithCacheFromObject( CommonCoastrictionOp,
553                                  [ IsList, IsGeneralizedMorphismByCospan ],
554
555  function( morphism_list, method_selection_object )
556    local arrow_list, reversedarrow_list, i, j, current_pushout_left, current_pushout_right, test_source;
557
558    if not ForAll( morphism_list, IsGeneralizedMorphismByCospan ) then
559        TryNextMethod();
560    fi;
561
562    if Length( morphism_list ) = 1 then
563        return morphism_list;
564    fi;
565
566    test_source := Range( morphism_list[ 1 ] );
567
568    if not ForAll( [ 2 .. Length( morphism_list ) ], i -> IsEqualForObjects( test_source, Range( morphism_list[ i ] ) ) ) then
569        Error( "not all ranges are equal" );
570    fi;
571
572    arrow_list := List( morphism_list, Arrow );
573    reversedarrow_list := List( morphism_list, ReversedArrow );
574
575    for i in [ 2  .. Length( morphism_list ) ] do
576        current_pushout_left := InjectionOfCofactorOfPushout( [ reversedarrow_list[ i - 1 ], reversedarrow_list[ i ] ], 1 );
577        current_pushout_right := InjectionOfCofactorOfPushout( [ reversedarrow_list[ i - 1 ], reversedarrow_list[ i ] ], 2 );
578
579        for j in [ 1 .. i - 1 ] do
580
581            arrow_list[ j ] := PreCompose( arrow_list[ j ], current_pushout_left );
582            reversedarrow_list[ j ] := PreCompose( reversedarrow_list[ j ], current_pushout_left );
583
584        od;
585
586        arrow_list[ i ] := PreCompose( arrow_list[ i ], current_pushout_right );
587        reversedarrow_list[ i ] := PreCompose( reversedarrow_list[ i ], current_pushout_right );
588
589    od;
590
591    return List( [ 1 .. Length( morphism_list ) ], i -> GeneralizedMorphismByCospan( arrow_list[ i ], reversedarrow_list[ i ] ) );
592
593end : ArgumentNumber := 2 );
594
595##
596InstallMethodWithCacheFromObject( ConcatenationProductOp,
597                                  [ IsList, IsGeneralizedMorphismByCospan ],
598
599  function( generalized_morphism_list, method_selection_object )
600
601    return GeneralizedMorphismByCospan( DirectSumFunctorial( List( generalized_morphism_list, Arrow ) ),
602                                        DirectSumFunctorial( List( generalized_morphism_list, ReversedArrow ) ) );
603
604end : ArgumentNumber := 2 );
605
606######################################
607##
608## Compatibility
609##
610######################################
611
612InstallMethod( GeneralizedMorphismByCospan,
613               [ IsCapCategoryMorphism, IsCapCategoryMorphism, IsCapCategoryMorphism ],
614
615  function( source_aid, morphism_aid, range_aid )
616    local morphism1, morphism2;
617
618    morphism1 := PseudoInverse( AsGeneralizedMorphismByCospan( source_aid ) );
619
620    morphism2 := GeneralizedMorphismByCospan( morphism_aid, range_aid );
621
622    return PreCompose( morphism1, morphism2 );
623
624end );
625
626InstallMethodWithCacheFromObject( DomainAssociatedMorphismCodomainTriple,
627                                  [ IsGeneralizedMorphismByCospan ],
628
629  function( morphism )
630    local three_arrow;
631
632    three_arrow := GeneralizedMorphismByThreeArrowsWithRangeAid( Arrow( morphism ), ReversedArrow( morphism ) );
633
634    return DomainAssociatedMorphismCodomainTriple( three_arrow );
635
636end );
637
638InstallMethod( GeneralizedMorphismByCospanWithSourceAid,
639               [ IsCapCategoryMorphism, IsCapCategoryMorphism ],
640
641  function( source_aid, morphism_aid )
642    local morphism1, morphism2;
643
644    morphism1 := GeneralizedInverseByCospan( source_aid );
645
646    morphism2 := AsGeneralizedMorphismByCospan( morphism_aid );
647
648    return PreCompose( morphism1, morphism2 );
649
650end );
651
652