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