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