Merge pull request #211 from mohamed-barakat/IsHomSetInhabited

outsourced a derivation of IsHomSetInhabited from Toposes to FinSetsForCAP
homalg-project · Jul 3, 2023 · 15c3eda · 15c3eda
2 parents 519f2e5 + 09746cd
commit 15c3eda
Show file tree

Hide file tree

Showing 5 changed files with 33 additions and 10 deletions.
diff --git a/PackageInfo.g b/PackageInfo.g
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "FinSetsForCAP",
 Subtitle := "The elementary topos of (skeletal) finite sets",
-Version := "2023.06-05",
+Version := "2023.06-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/examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g b/examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g
@@ -24,6 +24,7 @@ primitive_operations :=
           category_constructor( : no_precompiled_code := true ) );;
 list_of_operations :=
   SortedList( Concatenation( primitive_operations, [
+          "IsHomSetInhabited",
           "TruthMorphismOfImplies",
           #"HasPushoutComplement",
           "PushoutComplement",

diff --git a/gap/CompilerLogic.gi b/gap/CompilerLogic.gi
@@ -431,6 +431,15 @@ CapJitAddLogicTemplate(
     )
 );
 
+CapJitAddLogicTemplate(
+    rec(
+        variable_names := [ "number1", "number2" ],
+        variable_filters := [ IsBigInt, IsBigInt ],
+        src_template := "not number2 ^ number1 = 0",
+        dst_template := "number1 = 0 or not number2 = 0",
+    )
+);
+
 CapJitAddLogicTemplate(
     rec(
         variable_names := [ "entry", "func" ],

diff --git a/gap/SkeletalFinSets.gi b/gap/SkeletalFinSets.gi
@@ -331,14 +331,6 @@ AddIsEqualForMorphisms( SkeletalFinSets,
 
 end );
 
-##
-AddIsHomSetInhabited( SkeletalFinSets,
-  function ( cat, A, B )
-
-    return IsInitial( cat, A ) or not IsInitial( cat, B );
-
-end );
-
 ##
 AddIdentityMorphism( SkeletalFinSets,
   function ( cat, n )
@@ -985,6 +977,27 @@ end, 1 + Sum( [ [ "ExponentialOnObjects", 1 ],
 
 end );
 
+##
+AddDerivationToCAP( IsHomSetInhabited,
+        "IsHomSetInhabited using IsInitial when the range category of the homomorphism structure is the skeletal category of finite sets",
+        [ [ HomomorphismStructureOnObjects, 1 ],
+          [ IsInitial, 1, RangeCategoryOfHomomorphismStructure ] ],
+
+  function ( cat, a, b )
+    local range_cat;
+
+    range_cat := RangeCategoryOfHomomorphismStructure( cat );
+
+    return not IsInitial( range_cat,
+                   HomomorphismStructureOnObjects( cat, a, b ) );
+
+end : CategoryGetters := rec( range_cat := RangeCategoryOfHomomorphismStructure ),
+CategoryFilter :=
+  function ( cat )
+    return HasRangeCategoryOfHomomorphismStructure( cat ) and
+           IsCategoryOfSkeletalFinSets( RangeCategoryOfHomomorphismStructure( cat ) );
+end );
+
 ##
 InstallMethod( String,
         "for a CAP skeletal finite set",

diff --git a/gap/precompiled_categories/CategoryOfSkeletalFinSetsWithMorphismsGivenByListsPrecompiled.gi b/gap/precompiled_categories/CategoryOfSkeletalFinSetsWithMorphismsGivenByListsPrecompiled.gi
@@ -449,7 +449,7 @@ function ( cat_1, arg2_1, arg3_1 )
 end
 ########
 
-    , 100 );
+    , 202 : IsPrecompiledDerivation := true );
 
     ##
     AddIsInitial( cat,