diff --git a/PackageInfo.g b/PackageInfo.g index acbd6b6..90d6c85 100644 --- a/PackageInfo.g +++ b/PackageInfo.g @@ -10,7 +10,7 @@ SetPackageInfo( rec( PackageName := "FinSetsForCAP", Subtitle := "The elementary topos of (skeletal) finite sets", -Version := "2024.03-01", +Version := "2024.03-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", @@ -100,7 +100,7 @@ Dependencies := rec( NeededOtherPackages := [ [ "CAP", ">= 2023.12-05" ], [ "CartesianCategories", ">= 2024.02-02" ], - [ "Toposes", ">= 2024.02-02" ], + [ "Toposes", ">= 2024.03-04" ], ], SuggestedOtherPackages := [ ], ExternalConditions := [ ], diff --git a/doc/Doc.autodoc b/doc/Doc.autodoc index b72ebf1..a2f1774 100644 --- a/doc/Doc.autodoc +++ b/doc/Doc.autodoc @@ -58,6 +58,9 @@ @Subsection Lift @InsertChunk Lift +@Subsection Singleton morphism +@InsertChunk SingletonMorphism + @Subsection Topos properties @InsertChunk Topos @@ -133,6 +136,9 @@ @Subsection Skeletal Colift @InsertChunk SkeletalColift +@Subsection Skeletal singleton morphism +@InsertChunk SkeletalSingletonMorphism + @Subsection Skeletal topos properties @InsertChunk SkeletalTopos diff --git a/examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g b/examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g index 5d326b3..677d466 100644 --- a/examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g +++ b/examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g @@ -32,6 +32,7 @@ list_of_operations := "CoimageProjection", "IsHomSetInhabited", "TruthMorphismOfImplies", + "SingletonMorphismWithGivenPowerObject", #"HasPushoutComplement", "PushoutComplement", ] ) );; diff --git a/examples/SingletonMorphism.g b/examples/SingletonMorphism.g new file mode 100644 index 0000000..66d884d --- /dev/null +++ b/examples/SingletonMorphism.g @@ -0,0 +1,14 @@ +#! @Chunk SingletonMorphism + +#! @Example +LoadPackage( "FinSetsForCAP" ); +#! true +a := FinSet( [ 1, 2, 3 ] ); +#! +sa := SingletonMorphism( a ); +#! +sa = LowerSegmentOfRelation( a, a, CartesianDiagonal( a, 2 ) ); +#! true +sa = UpperSegmentOfRelation( a, a, CartesianDiagonal( a, 2 ) ); +#! true +#! @EndExample diff --git a/examples/SkeletalSingletonMorphism.g b/examples/SkeletalSingletonMorphism.g new file mode 100644 index 0000000..08c8147 --- /dev/null +++ b/examples/SkeletalSingletonMorphism.g @@ -0,0 +1,15 @@ +#! @Chunk SkeletalSingletonMorphism + +#! @Example +LoadPackage( "FinSetsForCAP" ); +#! true +a := FinSet( 3 ); +#! |3| +sa := SingletonMorphism( a );; +Display( sa ); +#! { 0, 1, 2 } ⱶ[ 1, 2, 4 ]→ { 0,..., 7 } +sa = LowerSegmentOfRelation( a, a, CartesianDiagonal( a, 2 ) ); +#! true +sa = UpperSegmentOfRelation( a, a, CartesianDiagonal( a, 2 ) ); +#! true +#! @EndExample diff --git a/gap/CompilerLogic.gi b/gap/CompilerLogic.gi index 95f9cd1..021949a 100644 --- a/gap/CompilerLogic.gi +++ b/gap/CompilerLogic.gi @@ -506,3 +506,37 @@ CapJitAddLogicTemplate( dst_template := "q * GeometricSumDiff1( q, a ) + a * i * GeometricSum( q, a )", ) ); + +CapJitAddLogicTemplate( + rec( + variable_names := [ "length", "value", "func" ], + src_template := "List( ListWithIdenticalEntries( length, value ), func )", + dst_template := "ListWithIdenticalEntries( length, func( value ) )", + ) +); + +CapJitAddLogicTemplate( + rec( + variable_names := [ "length", "value" ], + src_template := "Length( ListWithIdenticalEntries( length, value ) )", + dst_template := "length", + ) +); + +CapJitAddLogicTemplate( + rec( + variable_names := [ "length", "number" ], + variable_filters := [ IsBigInt, IsBigInt ], + src_template := "Product( ListWithIdenticalEntries( length, number ) )", + dst_template := "number ^ length", + ) +); + +CapJitAddLogicTemplate( + rec( + variable_names := [ "j", "a", "b" ], + variable_filters := [ IsBigInt, IsBigInt, IsBigInt ], + src_template := "Sum( List( [ 0 .. a - 1 ], k -> List( [ 0 .. a ^ 2 - 1 ], function( x ) if x in List( [ 0 .. a - 1 ], i -> i + i * a ) then return BigInt( 1 ); else return BigInt( 0 ); fi; end )[1 + k + j * a] * b ^ k ) )", + dst_template := "b ^ j", + ) +); diff --git a/gap/precompiled_categories/SkeletalCategoryOfFiniteSetsWithMorphismsGivenByListsPrecompiled.gi b/gap/precompiled_categories/SkeletalCategoryOfFiniteSetsWithMorphismsGivenByListsPrecompiled.gi index 695ec54..1184ed5 100644 --- a/gap/precompiled_categories/SkeletalCategoryOfFiniteSetsWithMorphismsGivenByListsPrecompiled.gi +++ b/gap/precompiled_categories/SkeletalCategoryOfFiniteSetsWithMorphismsGivenByListsPrecompiled.gi @@ -943,6 +943,21 @@ end , 19464 : IsPrecompiledDerivation := true ); + ## + AddSingletonMorphismWithGivenPowerObject( cat, + +######## +function ( cat_1, a_1, Pa_1 ) + local hoisted_1_1; + hoisted_1_1 := BigInt( 2 ); + return CreateCapCategoryMorphismWithAttributes( cat_1, a_1, Pa_1, AsList, List( [ 0 .. Length( a_1 ) - 1 ], function ( i_2 ) + return hoisted_1_1 ^ i_2; + end ) ); +end +######## + + , 605 : IsPrecompiledDerivation := true ); + ## AddSomeInjectiveObject( cat,