From 2b662bc27381c1a64bb5056afa14b444ee34edbd Mon Sep 17 00:00:00 2001 From: Mohamed Barakat Date: Mon, 15 May 2023 14:57:56 +0200 Subject: [PATCH] installed ExactCoverWithGlobalElements primitively and used it to "derive" MorphismsOfExternalHom --- PackageInfo.g | 2 +- gap/SkeletalFinSetsForCAP.gi | 55 ++++++++++--------- .../CategoryOfSkeletalFinSetsPrecompiled.gi | 19 +++---- 3 files changed, 38 insertions(+), 38 deletions(-) diff --git a/PackageInfo.g b/PackageInfo.g index 7f115fcc..17a11cb5 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.05-05", +Version := "2023.05-06", 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", diff --git a/gap/SkeletalFinSetsForCAP.gi b/gap/SkeletalFinSetsForCAP.gi index 1eb96fad..0d5886ff 100644 --- a/gap/SkeletalFinSetsForCAP.gi +++ b/gap/SkeletalFinSetsForCAP.gi @@ -857,25 +857,34 @@ AddCartesianLambdaIntroduction( SkeletalFinSets, end ); +## +AddExactCoverWithGlobalElements( SkeletalFinSets, + function ( cat, A ) + local T; + + T := TerminalObject( cat ); + + return List( [ 0 .. Length( A ) - 1 ], i -> MapOfFinSets( cat, T, [ i ], A ) ); + +end ); + ## AddExponentialOnMorphismsWithGivenExponentials( SkeletalFinSets, function ( cat, S, alpha, beta, T ) - local M, m, N, n, D, MN; + local M, N, MN, mors; M := Range( alpha ); - m := Length( M ); N := Source( beta ); - n := Length( N ); - - D := TerminalObject( cat ); MN := ExponentialOnObjects( cat, M, N ); + + mors := ExactCoverWithGlobalElements( cat, MN ); return MapOfFinSets( cat, S, - List( [ 0 .. n ^ m - 1 ], - function ( i ) + List( mors, + function ( mor ) return AsList( CartesianLambdaIntroduction( cat, PreComposeList( @@ -884,17 +893,14 @@ AddExponentialOnMorphismsWithGivenExponentials( SkeletalFinSets, CartesianLambdaElimination( cat, M, N, - MapOfFinSets( cat, - D, - [ i ], - MN ) ), + mor ), beta ] ) ) )[1 + 0]; end ), T ); -end, 1 + Sum( [ [ "TerminalObject", 1 ], - [ "ExponentialOnObjects", 1 ], +end, 1 + Sum( [ [ "ExponentialOnObjects", 1 ], + [ "ExactCoverWithGlobalElements", 1 ], [ "PreComposeList", 2 ], [ "CartesianLambdaElimination", 2 ], [ "CartesianLambdaIntroduction", 2 ] ], @@ -965,27 +971,22 @@ end ); ## AddMorphismsOfExternalHom( SkeletalFinSets, function ( cat, A, B ) - local hom_A_B, T; + local hom_A_B, mors; hom_A_B := ExponentialOnObjects( cat, A, B ); - T := TerminalObject( cat ); + mors := ExactCoverWithGlobalElements( cat, hom_A_B ); - return List( hom_A_B, - i -> CartesianLambdaElimination( cat, + return List( mors, + mor -> CartesianLambdaElimination( cat, A, B, - MapOfFinSets( cat, T, [ i ], hom_A_B ) ) ); + mor ) ); -end ); - -## -AddExactCoverWithGlobalElements( SkeletalFinSets, - function ( cat, A ) - - return MorphismsOfExternalHom( cat, TerminalObject( cat ), A ); - -end ); +end, 1 + Sum( [ [ "ExponentialOnObjects", 1 ], + [ "ExactCoverWithGlobalElements", 1 ], + [ "CartesianLambdaElimination", 2 ] ], + e -> e[2] * CurrentOperationWeight( SkeletalFinSets!.derivations_weight_list, e[1] ) ) ); end ); diff --git a/gap/precompiled_categories/CategoryOfSkeletalFinSetsPrecompiled.gi b/gap/precompiled_categories/CategoryOfSkeletalFinSetsPrecompiled.gi index df1c7ffa..b7813d9c 100644 --- a/gap/precompiled_categories/CategoryOfSkeletalFinSetsPrecompiled.gi +++ b/gap/precompiled_categories/CategoryOfSkeletalFinSetsPrecompiled.gi @@ -285,11 +285,10 @@ end ######## function ( cat_1, arg2_1 ) - local hoisted_2_1, deduped_3_1; - deduped_3_1 := Length( arg2_1 ); - hoisted_2_1 := CreateCapCategoryObjectWithAttributes( cat_1, Length, BigInt( 1 ) ); - return List( [ 0 .. deduped_3_1 - 1 ], function ( i_2 ) - return CreateCapCategoryMorphismWithAttributes( cat_1, hoisted_2_1, arg2_1, AsList, [ REM_INT( i_2, deduped_3_1 ) ] ); + local hoisted_1_1; + hoisted_1_1 := CreateCapCategoryObjectWithAttributes( cat_1, Length, BigInt( 1 ) ); + return List( [ 0 .. Length( arg2_1 ) - 1 ], function ( i_2 ) + return CreateCapCategoryMorphismWithAttributes( cat_1, hoisted_1_1, arg2_1, AsList, [ i_2 ] ); end ); end ######## @@ -309,10 +308,10 @@ function ( cat_1, s_1, alpha_1, beta_1, r_1 ) hoisted_4_1 := AsList( beta_1 ); hoisted_3_1 := AsList( alpha_1 ); hoisted_2_1 := [ 0 .. deduped_8_1 - 1 ]; - return CreateCapCategoryMorphismWithAttributes( cat_1, s_1, r_1, AsList, List( [ 0 .. deduped_7_1 ^ deduped_8_1 - 1 ], function ( i_2 ) + return CreateCapCategoryMorphismWithAttributes( cat_1, s_1, r_1, AsList, List( [ 0 .. deduped_7_1 ^ deduped_8_1 - 1 ], function ( logic_new_func_x_2 ) local hoisted_1_2; hoisted_1_2 := List( hoisted_2_1, function ( i_3 ) - return REM_INT( QUO_INT( i_2, deduped_7_1 ^ i_3 ), deduped_7_1 ); + return REM_INT( QUO_INT( logic_new_func_x_2, deduped_7_1 ^ i_3 ), deduped_7_1 ); end ); return Sum( List( hoisted_6_1, function ( k_3 ) return hoisted_4_1[(1 + hoisted_1_2[(1 + hoisted_3_1[(1 + CAP_JIT_INCOMPLETE_LOGIC( k_3 ))])])] * hoisted_5_1 ^ k_3; @@ -651,15 +650,15 @@ function ( cat_1, arg2_1, arg3_1 ) deduped_4_1 := Length( arg2_1 ); deduped_3_1 := Length( arg3_1 ); hoisted_2_1 := [ 0 .. deduped_4_1 - 1 ]; - return List( [ 0 .. deduped_3_1 ^ deduped_4_1 - 1 ], function ( i_2 ) + return List( [ 0 .. deduped_3_1 ^ deduped_4_1 - 1 ], function ( logic_new_func_x_2 ) return CreateCapCategoryMorphismWithAttributes( cat_1, arg2_1, arg3_1, AsList, List( hoisted_2_1, function ( i_3 ) - return REM_INT( QUO_INT( i_2, deduped_3_1 ^ i_3 ), deduped_3_1 ); + return REM_INT( QUO_INT( logic_new_func_x_2, deduped_3_1 ^ i_3 ), deduped_3_1 ); end ) ); end ); end ######## - , 100 ); + , 401 ); ## AddObjectConstructor( cat,