1#############################################################################
2##
3##                                               CAP package
4##
5##  Copyright 2014, Sebastian Gutsche, TU Kaiserslautern
6##                  Sebastian Posur,   RWTH Aachen
7##
8#############################################################################
9
10#############################################
11##
12## Installation method
13##
14#############################################
15
16BindGlobal( "CAP_INTERNAL_INSTALL_OPERATIONS_FOR_SERRE_QUOTIENT_BY_SPANS",
17
18  function( category )
19    local membership_function;
20
21    membership_function := SubcategoryMembershipTestFunctionForSerreQuotient( category );
22
23    ## Equalities
24
25    AddIsCongruentForMorphisms( category,
26
27      function( morphism1, morphism2 )
28        local underlying_general, new_general, sum_general,
29              sum_associated, sum_image;
30
31        underlying_general := UnderlyingGeneralizedMorphism( morphism2 );
32
33        new_general := AdditiveInverse( underlying_general );
34
35        sum_general := AdditionForMorphisms( UnderlyingGeneralizedMorphism( morphism1 ), new_general );
36
37        sum_associated := AssociatedMorphism( sum_general );
38
39        sum_image := ImageObject( sum_associated );
40
41        return membership_function( sum_image );
42
43    end );
44
45    AddIsEqualForObjects( category,
46
47      function( obj1, obj2 )
48
49        return IsEqualForObjects( UnderlyingHonestObject( obj1 ), UnderlyingHonestObject( obj2 ) );
50
51    end );
52
53    AddIsEqualForCacheForObjects( category, IsIdenticalObj );
54    AddIsEqualForCacheForMorphisms( category, IsIdenticalObj );
55
56    ## Is Zero
57
58    AddIsZeroForObjects( category,
59
60      function( obj )
61
62        return membership_function( UnderlyingHonestObject( obj ) );
63
64    end );
65
66    ## PreCompose
67
68    AddPreCompose( category,
69
70      function( morphism1, morphism2 )
71        local composition;
72
73        composition := PreCompose( UnderlyingGeneralizedMorphism( morphism1 ),
74                                   UnderlyingGeneralizedMorphism( morphism2 ) );
75
76        return SerreQuotientCategoryBySpansMorphism( category, composition );
77
78    end );
79
80    ## IdentityMorphism
81
82    AddIdentityMorphism( category,
83
84      function( object )
85
86        return AsSerreQuotientCategoryBySpansMorphism( category, IdentityMorphism( UnderlyingHonestObject( object ) ) );
87
88    end );
89
90    ## Addition for morphisms
91
92    AddAdditionForMorphisms( category,
93
94      function( morphism1, morphism2 )
95        local underlying_generalized, common_restriction, new_arrow;
96
97        underlying_generalized := List( [ morphism1, morphism2 ], UnderlyingGeneralizedMorphism );
98
99        common_restriction := CommonRestriction( underlying_generalized );
100
101        new_arrow := AdditionForMorphisms( Arrow( common_restriction[ 1 ] ), Arrow( common_restriction[ 2 ] ) );
102
103        return SerreQuotientCategoryBySpansMorphism( category, ReversedArrow( common_restriction[ 1 ] ), new_arrow );
104
105    end );
106
107    ## IsZeroForMorphisms
108    ## Can be derived, but there might be a faster solution
109#     AddIsZeroForMorphisms( category,
110#
111#       function( morphism )
112#         local associated, image;
113#
114#         associated := AssociatedMorphism( UnderlyingGeneralizedMorphism( morphism ) );
115#
116#         image := ImageObject( associated );
117#
118#         return membership_function( image );
119#
120#     end );
121
122    ## Additive inverse for morphisms (works without normalization)
123
124    AddAdditiveInverseForMorphisms( category,
125
126      function( morphism )
127        local general;
128
129        general := UnderlyingGeneralizedMorphism( morphism );
130
131        return SerreQuotientCategoryBySpansMorphism( category, ReversedArrow( general ), AdditiveInverseForMorphisms( Arrow( general ) ) );
132
133    end );
134
135    ## Zero morphism
136
137    AddZeroMorphism( category,
138
139      function( source, range )
140        local new_general;
141
142        new_general := ZeroMorphism( UnderlyingHonestObject( source ), UnderlyingHonestObject( range ) );
143
144        return AsSerreQuotientCategoryBySpansMorphism( category, new_general );
145
146    end );
147
148    ## Zero object
149
150    AddZeroObject( category,
151
152      function( )
153        local generalized_zero;
154
155        generalized_zero := ZeroObject( UnderlyingHonestCategory( category ) );
156
157        return AsSerreQuotientCategoryBySpansObject( category, generalized_zero );
158
159    end );
160
161    ## direct sum
162
163    AddDirectSum( category,
164
165      function( obj_list )
166        local honest_list, honest_sum;
167
168        honest_list := List( obj_list, UnderlyingHonestObject );
169
170        honest_sum := DirectSum( honest_list );
171
172        return AsSerreQuotientCategoryBySpansObject( category, honest_sum );
173
174    end );
175
176    AddProjectionInFactorOfDirectSumWithGivenDirectSum( category,
177
178      function( product_object, component_number, direct_sum_object )
179        local underlying_objects, honest_projection;
180
181        underlying_objects := List( product_object, UnderlyingHonestObject );
182
183        honest_projection := ProjectionInFactorOfDirectSum( underlying_objects, component_number );
184
185        return AsSerreQuotientCategoryBySpansMorphism( category, honest_projection );
186
187    end );
188
189    AddInjectionOfCofactorOfDirectSumWithGivenDirectSum( category,
190
191      function( object_product_list, injection_number, direct_sum_object )
192        local underlying_objects, honest_injection;
193
194        underlying_objects := List( object_product_list, UnderlyingHonestObject );
195
196        honest_injection := InjectionOfCofactorOfDirectSum( underlying_objects, injection_number );
197
198        return AsSerreQuotientCategoryBySpansMorphism( category, honest_injection );
199
200    end );
201
202    AddUniversalMorphismIntoDirectSum( category,
203
204      function( diagram, morphism_list )
205        local generalized_list, arrow_list, reversedarrow_list, new_arrow, new_reversed_arrow, object_list;
206
207        generalized_list := List( morphism_list, UnderlyingGeneralizedMorphism );
208
209        generalized_list := CommonRestriction( generalized_list );
210
211        new_reversed_arrow := ReversedArrow( generalized_list[ 1 ] );
212
213        arrow_list := List( generalized_list, Arrow );
214
215        new_arrow := UniversalMorphismIntoDirectSum( List( diagram, UnderlyingHonestObject ), arrow_list );
216
217        return SerreQuotientCategoryBySpansMorphism( category, new_reversed_arrow, new_arrow );
218
219    end );
220
221    AddUniversalMorphismFromDirectSum( category,
222
223      function( diagram, morphism_list )
224        local generalized_list, arrow_list, reversedarrow_list, new_arrow, new_reversed_arrow, object_list;
225
226        generalized_list := List( morphism_list, UnderlyingGeneralizedMorphism );
227
228        arrow_list := List( generalized_list, Arrow );
229
230        reversedarrow_list := List( generalized_list, ReversedArrow );
231
232        new_arrow := UniversalMorphismFromDirectSum( List( arrow_list, Source ), arrow_list );
233
234        new_reversed_arrow := DirectSumFunctorial( reversedarrow_list );
235
236        return SerreQuotientCategoryBySpansMorphism( category, new_reversed_arrow, new_arrow );
237
238    end );
239
240    ## Kernel
241
242    AddKernelEmbedding( category,
243
244      function( morphism )
245        local underlying_general, kernel_mor;
246
247        underlying_general := UnderlyingGeneralizedMorphism( morphism );
248
249#         underlying_general := NormalizedSpan( underlying_general );
250
251        kernel_mor := KernelEmbedding( Arrow( underlying_general ) );
252
253        return AsSerreQuotientCategoryBySpansMorphism( category, PreCompose( kernel_mor, ReversedArrow( underlying_general ) ) );
254
255    end );
256
257    AddLiftAlongMonomorphism( category,
258
259      function( monomorphism, test_morphism )
260        local inverse_of_mono, composition;
261
262        inverse_of_mono := PseudoInverse( UnderlyingGeneralizedMorphism( monomorphism ) );
263
264        composition := PreCompose( UnderlyingGeneralizedMorphism( test_morphism ), inverse_of_mono );
265
266        return SerreQuotientCategoryBySpansMorphism( category, composition );
267
268    end );
269
270    ## Cokernel
271
272    AddCokernelProjection( category,
273
274      function( morphism )
275        local underlying_general, cokernel_mor;
276
277        underlying_general := UnderlyingGeneralizedMorphism( morphism );
278
279#         underlying_general := NormalizedSpan( underlying_general );
280
281        cokernel_mor := CokernelProjection( Arrow( underlying_general ) );
282
283        return AsSerreQuotientCategoryBySpansMorphism( category, cokernel_mor );
284
285    end );
286
287    AddColiftAlongEpimorphism( category,
288
289      function( epimorphism, test_morphism )
290        local inverse_of_epi, composition;
291
292        inverse_of_epi := PseudoInverse( UnderlyingGeneralizedMorphism( epimorphism ) );
293
294        composition := PreCompose( inverse_of_epi, UnderlyingGeneralizedMorphism( test_morphism ) );
295
296        return SerreQuotientCategoryBySpansMorphism( category, composition );
297
298    end );
299
300    AddLift( category,
301
302      function( test_morphism, monomorphism )
303        local inverse_of_mono, composition;
304
305        test_morphism := UnderlyingGeneralizedMorphism( test_morphism );
306        monomorphism := UnderlyingGeneralizedMorphism( monomorphism );
307
308        if not IsHonest( test_morphism ) or not IsHonest( monomorphism ) then
309            return fail;
310        fi;
311
312        test_morphism := HonestRepresentative( test_morphism );
313        monomorphism := HonestRepresentative( monomorphism );
314
315        composition := Lift( test_morphism, monomorphism );
316
317        if composition = fail then
318            return fail;
319        fi;
320
321        return AsSerreQuotientCategoryBySpansMorphism( category, composition );
322
323    end );
324
325    AddDualOnObjects( category,
326
327      function( object )
328
329        return AsSerreQuotientCategoryBySpansObject( category, DualOnObjects( UnderlyingHonestObject( object ) ) );
330
331    end );
332
333    AddDualOnMorphismsWithGivenDuals( category,
334
335      function( new_source, morphism, new_range )
336        local arrow, reversed_arrow, new_arrow, new_reversed_arrow;
337
338        arrow := Arrow( UnderlyingGeneralizedMorphism( morphism ) );
339        reversed_arrow := ReversedArrow( UnderlyingGeneralizedMorphism( morphism ) );
340
341        arrow := DualOnMorphisms( arrow );
342        reversed_arrow := DualOnMorphisms( reversed_arrow );
343
344        new_reversed_arrow := ProjectionInFactorOfFiberProduct( [ reversed_arrow, arrow ], 2 );
345        new_arrow := ProjectionInFactorOfFiberProduct( [ reversed_arrow, arrow ], 1 );
346
347        return SerreQuotientCategoryBySpansMorphism( category, new_reversed_arrow, new_arrow );
348
349    end );
350
351    AddInverse( category,
352
353      function( morphism )
354        local underlying_general, inverse;
355
356        underlying_general := UnderlyingGeneralizedMorphism( morphism );
357
358        inverse := PseudoInverse( underlying_general );
359
360        return SerreQuotientCategoryBySpansMorphism( category, inverse );
361
362    end );
363
364end );
365
366#############################################
367##
368## Constructor
369##
370#############################################
371
372InstallMethod( SerreQuotientCategoryBySpans,
373               [ IsCapCategory, IsFunction ],
374
375  function( category, test_function )
376    local name;
377
378    name := NameFunction( test_function );
379
380    return SerreQuotientCategoryBySpans( category, test_function, Concatenation( "test function with name: ", name ) );
381
382end );
383
384InstallMethodWithCacheFromObject( SerreQuotientCategoryBySpans,
385                                  [ IsCapCategory, IsFunction, IsString ],
386
387  function( category, test_function, function_name )
388    local serre_category, gen_category, name, preconditions, category_weight_list, i;
389
390    if not HasIsFinalized( category ) or not IsFinalized( category ) then
391
392        Error( "category must be finalized" );
393        return;
394
395    fi;
396
397    preconditions := [ "IsEqualForObjects",
398                       "ImageObject",
399                       "AdditiveInverseForMorphisms",
400                       "IdentityMorphism",
401                       "ZeroMorphism",
402                       "DirectSum",
403                       "ProjectionInFactorOfDirectSumWithGivenDirectSum",
404                       "InjectionOfCofactorOfDirectSumWithGivenDirectSum",
405                       "UniversalMorphismFromDirectSum",
406                       "UniversalMorphismIntoDirectSum",
407                       "DirectSumFunctorialWithGivenDirectSums",
408                       "KernelEmbedding",
409                       "CokernelProjection" ];
410
411    category_weight_list := category!.derivations_weight_list;
412
413    for i in preconditions do
414
415        if CurrentOperationWeight( category_weight_list, i ) = infinity then
416
417            Error( Concatenation( "category must be able to compute ", i ) );
418            return;
419
420        fi;
421
422    od;
423
424    name := Name( category );
425
426    name := Concatenation( "The Serre quotient category of ", name, " by ", function_name );
427
428    serre_category := CreateCapCategory( name );
429
430    AddObjectRepresentation( serre_category, IsSerreQuotientCategoryBySpansObject );
431
432    AddMorphismRepresentation( serre_category, IsSerreQuotientCategoryBySpansMorphism );
433
434    serre_category!.predicate_logic := category!.predicate_logic;
435
436    SetFilterObj( serre_category, WasCreatedAsSerreQuotientCategoryBySpans );
437
438    SetUnderlyingHonestCategory( serre_category, category );
439
440    SetUnderlyingGeneralizedMorphismCategory( serre_category, GeneralizedMorphismCategoryBySpans( category ) );
441
442    SetSubcategoryMembershipTestFunctionForSerreQuotient( serre_category, test_function );
443
444    SetIsAbelianCategory( serre_category, true );
445
446    CAP_INTERNAL_INSTALL_OPERATIONS_FOR_SERRE_QUOTIENT_BY_SPANS( serre_category );
447
448    CAP_INTERNAL_INSTALL_OPERATIONS_FOR_SERRE_QUOTIENT( serre_category );
449
450    Finalize( serre_category );
451
452    return serre_category;
453
454end );
455
456InstallMethodWithCacheFromObject( AsSerreQuotientCategoryBySpansObject,
457                                  [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans, IsCapCategoryObject ],
458
459  function( serre_category, object )
460    local honest_category, serre_object;
461
462    honest_category := UnderlyingHonestCategory( serre_category );
463
464    if not IsIdenticalObj( honest_category, CapCategory( object ) ) then
465
466        Error( "object does not belong to underlying honest category of serre quotient" );
467
468    fi;
469
470    serre_object := rec( );
471
472    ObjectifyObjectForCAPWithAttributes( serre_object, serre_category,
473                             UnderlyingHonestObject, object,
474                             UnderlyingGeneralizedObject, GeneralizedMorphismBySpansObject( object ) );
475
476    if HasSpecializedObjectFilterForSerreQuotients( serre_category ) then
477
478        SetFilterObj( serre_object, SpecializedObjectFilterForSerreQuotients( serre_category ) );
479
480    fi;
481
482    return serre_object;
483
484end );
485
486InstallMethodWithCacheFromObject( SerreQuotientCategoryBySpansMorphism,
487                                  [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans, IsGeneralizedMorphismBySpan ],
488
489  function( serre_category, gen_morphism )
490    local honest_category, serre_morphism;
491
492    if not IsIdenticalObj( UnderlyingGeneralizedMorphismCategory( serre_category ), CapCategory( gen_morphism ) ) then
493
494        Error( "generalized morphism has wrong category" );
495
496    fi;
497
498    serre_morphism := rec( );
499
500    ObjectifyMorphismForCAPWithAttributes( serre_morphism, serre_category,
501                             Source, AsSerreQuotientCategoryBySpansObject( serre_category, UnderlyingHonestObject( Source( gen_morphism ) ) ),
502                             Range, AsSerreQuotientCategoryBySpansObject( serre_category, UnderlyingHonestObject( Range( gen_morphism ) ) ),
503                             UnderlyingGeneralizedMorphism, gen_morphism );
504
505    if HasSpecializedMorphismFilterForSerreQuotients( serre_category ) then
506
507        SetFilterObj( serre_morphism, SpecializedMorphismFilterForSerreQuotients( serre_category ) );
508
509    fi;
510
511    return serre_morphism;
512
513end );
514
515InstallMethod( SerreQuotientCategoryMorphism,
516               [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans, IsGeneralizedMorphismBySpan ],
517
518  SerreQuotientCategoryBySpansMorphism );
519
520InstallMethod( SerreQuotientCategoryBySpansMorphism,
521               [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans, IsCapCategoryMorphism, IsCapCategoryMorphism, IsCapCategoryMorphism ],
522
523  function( serre_category, source_aid, associated, range_aid )
524
525    return SerreQuotientCategoryBySpansMorphism( serre_category, GeneralizedMorphismBySpan( source_aid, associated, range_aid ) );
526
527end );
528
529InstallMethod( SerreQuotientCategoryBySpansMorphism,
530               [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans, IsCapCategoryMorphism, IsCapCategoryMorphism ],
531
532  function( serre_category, reversed_arrow, arrow )
533
534    return SerreQuotientCategoryBySpansMorphism( serre_category, GeneralizedMorphismBySpan( reversed_arrow, arrow ) );
535
536end );
537
538InstallMethod( SerreQuotientCategoryBySpansMorphismWithRangeAid,
539               [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans, IsCapCategoryMorphism, IsCapCategoryMorphism ],
540
541  function( serre_category, associated, range_aid )
542
543    return SerreQuotientCategoryBySpansMorphism( serre_category, GeneralizedMorphismBySpanWithRangeAid( associated, range_aid ) );
544
545end );
546
547InstallMethodWithCacheFromObject( AsSerreQuotientCategoryBySpansMorphism,
548                                  [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans, IsCapCategoryMorphism ],
549
550  function( serre_category, arrow )
551
552    return SerreQuotientCategoryBySpansMorphism( serre_category, AsGeneralizedMorphismBySpan( arrow ) );
553
554end );
555
556#############################################
557##
558## Compatibility layer
559##
560#############################################
561
562InstallMethod( AsSerreQuotientCategoryObject,
563               [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans, IsCapCategoryObject ],
564
565  AsSerreQuotientCategoryBySpansObject );
566
567InstallMethod( AsSerreQuotientCategoryMorphism,
568               [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans, IsCapCategoryMorphism ],
569
570  AsSerreQuotientCategoryBySpansMorphism );
571
572InstallMethod( SerreQuotientCategoryMorphism,
573               [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans, IsGeneralizedMorphismBySpan ],
574
575  SerreQuotientCategoryBySpansMorphism );
576
577InstallMethod( SerreQuotientCategoryMorphism,
578               [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans, IsCapCategoryMorphism, IsCapCategoryMorphism, IsCapCategoryMorphism ],
579
580  SerreQuotientCategoryBySpansMorphism );
581
582InstallMethod( SerreQuotientCategoryMorphism,
583               [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans, IsCapCategoryMorphism, IsCapCategoryMorphism ],
584
585  SerreQuotientCategoryBySpansMorphism );
586
587InstallMethod( SerreQuotientCategoryMorphismWithRangeAid,
588               [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans, IsCapCategoryMorphism, IsCapCategoryMorphism ],
589
590  SerreQuotientCategoryBySpansMorphismWithRangeAid );
591
592InstallMethod( SerreQuotientCategoryMorphismWithSourceAid,
593               [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans, IsCapCategoryMorphism, IsCapCategoryMorphism ],
594
595  SerreQuotientCategoryBySpansMorphism );
596
597#############################################
598##
599## Functor
600##
601#############################################
602
603InstallMethod( CanonicalProjection,
604               [ IsCapCategory and WasCreatedAsSerreQuotientCategoryBySpans ],
605
606  function( category )
607    local underlying_honest, functor;
608
609    underlying_honest := UnderlyingHonestCategory( category );
610
611    functor := CapFunctor( Concatenation( "Embedding in ", Name( category ) ), underlying_honest, category );
612
613    AddObjectFunction( functor,
614
615        i -> AsSerreQuotientCategoryBySpansObject( category, i ) );
616
617    AddMorphismFunction( functor,
618
619      function( new_source, morphism, new_range )
620
621        return AsSerreQuotientCategoryBySpansMorphism( category, morphism );
622
623    end );
624
625    return functor;
626
627end );
628