Skip to content

Commit

Permalink
AddAstrictionToCoimage
Browse files Browse the repository at this point in the history
ImageEmbedding( phi )      ⤳ Set
AstrictionToCoimage( phi ) ⤳ DuplicateFreeList

and compiled CoimageProjection

needs CAP v2023.10-07
  • Loading branch information
mohamed-barakat committed Oct 17, 2023
1 parent dfa939e commit e9a1437
Show file tree
Hide file tree
Showing 4 changed files with 50 additions and 3 deletions.
4 changes: 2 additions & 2 deletions PackageInfo.g
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ SetPackageInfo( rec(

PackageName := "FinSetsForCAP",
Subtitle := "The elementary topos of (skeletal) finite sets",
Version := "2023.10-01",
Version := "2023.10-02",

Date := (function ( ) if IsBound( GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE ) then return GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE; else return Concatenation( ~.Version{[ 1 .. 4 ]}, "-", ~.Version{[ 6, 7 ]}, "-01" ); fi; end)( ),
License := "GPL-2.0-or-later",
Expand Down Expand Up @@ -98,7 +98,7 @@ PackageDoc := rec(
Dependencies := rec(
GAP := ">= 4.12.1",
NeededOtherPackages := [
[ "CAP", ">= 2023.09-11" ],
[ "CAP", ">= 2023.10-07" ],
[ "CartesianCategories", ">= 2023.08-13" ],
[ "Toposes", ">= 2023.10-01" ],
],
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@

LoadPackage( "FinSetsForCAP", false );
#! true
LoadPackage( "CompilerForCAP", false );
LoadPackage( "CompilerForCAP", ">= 2023.10-03", false );
#! true

ReadPackage( "FinSetsForCAP", "gap/CompilerLogic.gi" );
Expand All @@ -25,6 +25,7 @@ primitive_operations :=
list_of_operations :=
SortedList( Concatenation( primitive_operations, [
"CoastrictionToImage",
"CoimageProjection",
"IsHomSetInhabited",
"TruthMorphismOfImplies",
#"HasPushoutComplement",
Expand Down
16 changes: 16 additions & 0 deletions gap/SkeletalFinSets.gi
Original file line number Diff line number Diff line change
Expand Up @@ -481,6 +481,22 @@ AddImageEmbedding( SkeletalFinSets,

end );

##
AddAstrictionToCoimage( SkeletalFinSets,
function ( cat, phi )
local L, map;

L := AsList( phi );

## unlike ImageObject which is a subobject of the range,
## the CoimageObject is a factor object of the source,
## and we want to retain the sorting of the source:
map := DuplicateFreeList( L );

return MorphismConstructor( cat, ObjectConstructor( cat, BigInt( Length( map ) ) ), map, Range( phi ) );

end );

## Limits

##
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,19 @@
#
BindGlobal( "ADD_FUNCTIONS_FOR_SkeletalCategoryOfFiniteSetsWithMorphismsGivenByListsPrecompiled", function ( cat )

##
AddAstrictionToCoimage( cat,

########
function ( cat_1, alpha_1 )
local deduped_1_1;
deduped_1_1 := DuplicateFreeList( AsList( alpha_1 ) );
return CreateCapCategoryMorphismWithAttributes( cat_1, CreateCapCategoryObjectWithAttributes( cat_1, Length, BigInt( Length( deduped_1_1 ) ) ), Range( alpha_1 ), AsList, deduped_1_1 );
end
########

, 100 );

##
AddCartesianBraidingInverseWithGivenDirectProducts( cat,

Expand Down Expand Up @@ -184,6 +197,23 @@ end

, 100 );

##
AddCoimageProjection( cat,

########
function ( cat_1, alpha_1 )
local deduped_3_1, deduped_4_1, deduped_5_1;
deduped_5_1 := AsList( alpha_1 );
deduped_4_1 := Source( alpha_1 );
deduped_3_1 := DuplicateFreeList( deduped_5_1 );
return CreateCapCategoryMorphismWithAttributes( cat_1, deduped_4_1, CreateCapCategoryObjectWithAttributes( cat_1, Length, BigInt( Length( deduped_3_1 ) ) ), AsList, List( [ 0 .. Length( deduped_4_1 ) - 1 ], function ( x_2 )
return -1 + BigInt( SafePosition( deduped_3_1, deduped_5_1[(1 + x_2)] ) );
end ) );
end
########

, 202 : IsPrecompiledDerivation := true );

##
AddColift( cat,

Expand Down

0 comments on commit e9a1437

Please sign in to comment.