diff --git a/PackageInfo.g b/PackageInfo.g index 9f70ee55..b8562964 100644 --- a/PackageInfo.g +++ b/PackageInfo.g @@ -10,7 +10,7 @@ SetPackageInfo( rec( PackageName := "FinSetsForCAP", Subtitle := "The elementary topos of (skeletal) finite sets", -Version := "2023.10-02", +Version := "2023.10-03", 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", @@ -100,7 +100,7 @@ Dependencies := rec( NeededOtherPackages := [ [ "CAP", ">= 2023.09-11" ], [ "CartesianCategories", ">= 2023.08-13" ], - [ "Toposes", ">= 2023.10-01" ], + [ "Toposes", ">= 2023.10-13" ], ], SuggestedOtherPackages := [ ], ExternalConditions := [ ], diff --git a/doc/Doc.autodoc b/doc/Doc.autodoc index ecd98b6a..b72ebf13 100644 --- a/doc/Doc.autodoc +++ b/doc/Doc.autodoc @@ -106,6 +106,9 @@ @InsertChunk SkeletalImageEmbedding @InsertChunk SkeletalCoastrictionToImage +@Subsection Skeletal Coimage +@InsertChunk SkeletalCoimageObject + @Subsection Skeletal Preimage @InsertChunk SkeletalPreimage diff --git a/examples/CoimageObject.g b/examples/CoimageObject.g index c71a131c..6768915c 100644 --- a/examples/CoimageObject.g +++ b/examples/CoimageObject.g @@ -22,10 +22,11 @@ IsEpimorphism( phi ); #! false IsSplitEpimorphism( phi ); #! false -iota := AstrictionToCoimage( phi ); -#! pi := CoimageProjection( phi ); #! +iota := AstrictionToCoimage( phi ); +#! PreCompose( pi, iota ) = phi; #! true + #! @EndExample diff --git a/examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g b/examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g index f6539b33..9076c5a7 100644 --- a/examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g +++ b/examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g @@ -8,7 +8,7 @@ LoadPackage( "FinSetsForCAP", false ); #! true -LoadPackage( "CompilerForCAP", false ); +LoadPackage( "CompilerForCAP", ">= 2023.10-03", false ); #! true ReadPackage( "FinSetsForCAP", "gap/CompilerLogic.gi" ); @@ -24,6 +24,8 @@ primitive_operations := category_constructor( : no_precompiled_code := true ) );; list_of_operations := SortedList( Concatenation( primitive_operations, [ + "CoastrictionToImage", + "CoimageProjection", "IsHomSetInhabited", "TruthMorphismOfImplies", #"HasPushoutComplement", diff --git a/examples/SkeletalCoimageObject.g b/examples/SkeletalCoimageObject.g new file mode 100644 index 00000000..b1a2b1d4 --- /dev/null +++ b/examples/SkeletalCoimageObject.g @@ -0,0 +1,32 @@ +#! @Chunk SkeletalCoimageObject + +#! @Example +LoadPackage( "FinSetsForCAP", false ); +#! true +m := FinSet( 3 ); +#! |3| +n := FinSet( 3 ); +#! |3| +phi := MapOfFinSets( m, [ 1, 0, 1 ], n ); +#! |3| → |3| +I := CoimageObject( phi ); +#! |2| +IsMonomorphism( phi ); +#! false +IsSplitMonomorphism( phi ); +#! false +IsEpimorphism( phi ); +#! false +IsSplitEpimorphism( phi ); +#! false +pi := CoimageProjection( phi ); +#! |3| → |2| +iota := AstrictionToCoimage( phi ); +#! |2| → |3| +PreCompose( pi, iota ) = phi; +#! true +Display( iota ); +#! { 0, 1 } ⱶ[ 1, 0 ]→ { 0, 1, 2 } +Display( ImageEmbedding( phi ) ); +#! { 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1, 2 } +#! @EndExample diff --git a/gap/SkeletalFinSets.gi b/gap/SkeletalFinSets.gi index 4e6882c7..481de57f 100644 --- a/gap/SkeletalFinSets.gi +++ b/gap/SkeletalFinSets.gi @@ -356,14 +356,6 @@ AddPreCompose( SkeletalFinSets, end ); -## -AddImageObject( SkeletalFinSets, - function ( cat, phi ) - - return ObjectConstructor( cat, BigInt( Length( Set( AsList( phi ) ) ) ) ); - -end ); - ## the function SKELETAL_FIN_SETS_IsEpimorphism ## has linear runtime complexity AddIsEpimorphism( SkeletalFinSets, @@ -484,36 +476,32 @@ AddColift( SkeletalFinSets, end ); ## -AddImageEmbeddingWithGivenImageObject( SkeletalFinSets, - function ( cat, phi, image ) +AddImageEmbedding( SkeletalFinSets, + function ( cat, phi ) + local map; + + map := Set( AsList( phi ) ); + + return MorphismConstructor( cat, ObjectConstructor( cat, BigInt( Length( map ) ) ), map, Range( phi ) ); - return MorphismConstructor( cat, image, Set( AsList( phi ) ), Range( phi ) ); - end ); ## -AddCoastrictionToImageWithGivenImageObject( SkeletalFinSets, - function ( cat, phi, image_object ) - local G, images, s, L, l, pi; - - G := AsList( phi ); - - images := Set( G ); - - s := Source( phi ); - - L := List( s, i -> -1 + BigInt( SafePosition( images, G[1 + i] ) ) ); +AddAstrictionToCoimage( SkeletalFinSets, + function ( cat, phi ) + local L, map; - pi := MorphismConstructor( cat, s, L, image_object ); + L := AsList( phi ); - #% CAP_JIT_DROP_NEXT_STATEMENT - Assert( 3, IsEpimorphism( cat, pi ) ); + ## 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 pi; + return MorphismConstructor( cat, ObjectConstructor( cat, BigInt( Length( map ) ) ), map, Range( phi ) ); end ); - ## Limits ## diff --git a/gap/precompiled_categories/SkeletalCategoryOfFiniteSetsWithMorphismsGivenByListsPrecompiled.gi b/gap/precompiled_categories/SkeletalCategoryOfFiniteSetsWithMorphismsGivenByListsPrecompiled.gi index 00bd6787..1c36790d 100644 --- a/gap/precompiled_categories/SkeletalCategoryOfFiniteSetsWithMorphismsGivenByListsPrecompiled.gi +++ b/gap/precompiled_categories/SkeletalCategoryOfFiniteSetsWithMorphismsGivenByListsPrecompiled.gi @@ -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, @@ -157,21 +170,21 @@ end , 100 ); ## - AddCoastrictionToImageWithGivenImageObject( cat, + AddCoastrictionToImage( cat, ######## -function ( cat_1, alpha_1, I_1 ) - local hoisted_2_1, deduped_3_1, deduped_4_1; - deduped_4_1 := AsList( alpha_1 ); - deduped_3_1 := Source( alpha_1 ); - hoisted_2_1 := SSortedList( deduped_4_1 ); - return CreateCapCategoryMorphismWithAttributes( cat_1, deduped_3_1, I_1, AsList, List( [ 0 .. Length( deduped_3_1 ) - 1 ], function ( i_2 ) - return -1 + BigInt( SafePosition( hoisted_2_1, deduped_4_1[(1 + i_2)] ) ); +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 := SSortedList( 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 ######## - , 100 ); + , 202 : IsPrecompiledDerivation := true ); ## AddCoequalizer( cat, @@ -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, @@ -345,22 +375,13 @@ end , 100 ); ## - AddImageEmbeddingWithGivenImageObject( cat, + AddImageEmbedding( cat, ######## -function ( cat_1, alpha_1, I_1 ) - return CreateCapCategoryMorphismWithAttributes( cat_1, I_1, Range( alpha_1 ), AsList, SSortedList( AsList( alpha_1 ) ) ); -end -######## - - , 100 ); - - ## - AddImageObject( cat, - -######## -function ( cat_1, arg2_1 ) - return CreateCapCategoryObjectWithAttributes( cat_1, Length, BigInt( Length( SSortedList( AsList( arg2_1 ) ) ) ) ); +function ( cat_1, alpha_1 ) + local deduped_1_1; + deduped_1_1 := SSortedList( AsList( alpha_1 ) ); + return CreateCapCategoryMorphismWithAttributes( cat_1, CreateCapCategoryObjectWithAttributes( cat_1, Length, BigInt( Length( deduped_1_1 ) ) ), Range( alpha_1 ), AsList, deduped_1_1 ); end ######## @@ -816,7 +837,7 @@ function ( cat_1, l_1, m_1 ) end ######## - , 19767 : IsPrecompiledDerivation := true ); + , 19464 : IsPrecompiledDerivation := true ); ## AddSomeInjectiveObject( cat,