added example file HeytingAlgebraOfSubobjects.g

needs Toposes v2021.11-19

Author: mohamed-barakat

PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "FinSetsForCAP",
 Subtitle := "The elementary topos of (skeletal) finite sets",
-Version := "2021.11-15",
+Version := "2021.11-16",
 
 Date := Concatenation( "01/", ~.Version{[ 6, 7 ]}, "/", ~.Version{[ 1 .. 4 ]} ),
 License := "GPL-2.0-or-later",
@@ -100,7 +100,7 @@ Dependencies := rec(
   NeededOtherPackages := [
                    [ "GAPDoc", ">= 1.5" ],
                    [ "CAP", ">= 2021.05-02" ],
-                   [ "Toposes", ">= 2021.11-13" ],
+                   [ "Toposes", ">= 2021.11-19" ],
                    ],
   SuggestedOtherPackages := [ ],
   ExternalConditions := [ ],

doc/Doc.autodoc

@@ -57,6 +57,7 @@
 
 @Subsection Subobject Classifier
 @InsertChunk SubobjectClassifier
+@InsertChunk HeytingAlgebraOfSubobjects
 
 @Chapter The category of skeletal finite sets
 
@@ -122,3 +123,4 @@
 
 @Subsection Skeletal Subobject Classifier
 @InsertChunk SkeletalSubobjectClassifier
+@InsertChunk SkeletalHeytingAlgebraOfSubobjects

examples/HeytingAlgebraOfSubobjects.g

@@ -0,0 +1,59 @@
+#! @Chunk HeytingAlgebraOfSubobjects
+
+LoadPackage( "FinSetsForCAP" );
+
+# Below we see the Heyting algebra structure
+# on the set of subobjects (= monos up to mutual dominance)
+
+#! @Example
+M := FinSet( [ 1 .. 7 ] );
+#! <An object in FinSets>
+N := FinSet( [ 2, 3, 5 ] );
+#! <An object in FinSets>
+iotaN := EmbeddingOfFinSets( N, M );
+#! <A monomorphism in FinSets>
+NC := PseudoComplementSubobject( iotaN );
+#! <An object in FinSets>
+Display( NC );
+#! [ [ 1, "*" ], [ 4, "*" ], [ 6, "*" ], [ 7, "*" ] ]
+tauN := EmbeddingOfPseudoComplementSubobject( iotaN );
+#! <A monomorphism in FinSets>
+Nc := ImageObject( tauN );
+#! <An object in FinSets>
+Display( Nc );
+#! [ 1, 4, 6, 7 ]
+L := FinSet( [ 2, 4, 5, 7 ] );
+#! <An object in FinSets>
+iotaL := EmbeddingOfFinSets( L, M );
+#! <A monomorphism in FinSets>
+NIL := IntersectionSubobject( iotaN, iotaL );
+#! <An object in FinSets>
+Display( NIL );
+#! [ [ 2, 2 ], [ 5, 5 ] ]
+iotaNiL := EmbeddingOfIntersectionSubobject( iotaN, iotaL );
+#! <A monomorphism in FinSets>
+NiL := ImageObject( iotaNiL );
+#! <An object in FinSets>
+Display( NiL );
+#! [ 2, 5 ]
+NUL := UnionSubobject( iotaN, iotaL );
+#! <An object in FinSets>
+Display( NUL );
+#! [ 2, 3, 5, 4, 7 ]
+iotaNuL := EmbeddingOfUnionSubobject( iotaN, iotaL );
+#! <A monomorphism in FinSets>
+NuL := ImageObject( iotaNuL );
+#! <An object in FinSets>
+Display( NuL );
+#! [ 2, 3, 5, 4, 7 ]
+NPL := RelativePseudoComplementSuboject( iotaN, iotaL );
+#! <An object in FinSets>
+Display( NPL );
+#! [ [ 1, "*" ], [ 2, "*" ], [ 4, "*" ], [ 5, "*" ], [ 6, "*" ], [ 7, "*" ] ]
+iotaNpL := EmbeddingOfRelativePseudoComplementSuboject( iotaN, iotaL );
+#! <A monomorphism in FinSets>
+NpL := ImageObject( iotaNpL );
+#! <An object in FinSets>
+Display( NpL );
+#! [ 1, 2, 4, 5, 6, 7 ]
+#! @EndExample

examples/SkeletalHeytingAlgebraOfSubobjects.g

@@ -0,0 +1,51 @@
+#! @Chunk SkeletalHeytingAlgebraOfSubobjects
+
+LoadPackage( "FinSetsForCAP" );
+
+# Below we see the Heyting algebra structure
+# on the set of subobjects (= monos up to mutual dominance)
+
+#! @Example
+M := FinSet( 7 );
+#! <An object in SkeletalFinSets>
+N := FinSet( 3 );
+#! <An object in SkeletalFinSets>
+iotaN := MapOfFinSets( N, [ 2, 3, 5 ], M );
+#! <A morphism in SkeletalFinSets>
+NC := PseudoComplementSubobject( iotaN );
+#! <An object in SkeletalFinSets>
+Display( NC );
+#! 4
+tauN := EmbeddingOfPseudoComplementSubobject( iotaN );
+#! <A monomorphism in SkeletalFinSets>
+Display( tauN );
+#! [ 4, [ 1, 4, 6, 7 ], 7 ]
+L := FinSet( 4 );
+#! <An object in SkeletalFinSets>
+iotaL := MapOfFinSets( L, [ 2, 4, 5, 7 ], M );
+#! <A morphism in SkeletalFinSets>
+NIL := IntersectionSubobject( iotaN, iotaL );
+#! <An object in SkeletalFinSets>
+Display( NIL );
+#! 2
+iotaNiL := EmbeddingOfIntersectionSubobject( iotaN, iotaL );
+#! <A morphism in SkeletalFinSets>
+Display( iotaNiL );
+#! [ 2, [ 2, 5 ], 7 ]
+NUL := UnionSubobject( iotaN, iotaL );
+#! <An object in SkeletalFinSets>
+Display( NUL );
+#! 5
+iotaNuL := EmbeddingOfUnionSubobject( iotaN, iotaL );
+#! <A monomorphism in SkeletalFinSets>
+Display( iotaNuL );
+#! [ 5, [ 2, 3, 4, 5, 7 ], 7 ]
+NPL := RelativePseudoComplementSuboject( iotaN, iotaL );
+#! <An object in SkeletalFinSets>
+Display( NPL );
+#! 6
+iotaNpL := EmbeddingOfRelativePseudoComplementSuboject( iotaN, iotaL );
+#! <A monomorphism in SkeletalFinSets>
+Display( iotaNpL );
+#! [ 6, [ 1, 2, 4, 5, 6, 7 ], 7 ]
+#! @EndExample

gap/FinSetsForCAP.gi

@@ -25,6 +25,9 @@ InstallMethod( CategoryOfFinSets,
 
     INSTALL_FUNCTIONS_FOR_FIN_SETS( FinSets );
 
+    AddTheoremFileToCategory( FinSets,
+            Filename( DirectoriesPackageLibrary( "Toposes", "LogicForToposes" ), "PropositionsForToposes.tex" ) );
+    
     Finalize( FinSets );
 
     return FinSets;

gap/SkeletalFinSetsForCAP.gi

@@ -27,6 +27,9 @@ InstallMethod( CategoryOfSkeletalFinSets,
 
     INSTALL_FUNCTIONS_FOR_SKELETAL_FIN_SETS( cat );
 
+    AddTheoremFileToCategory( FinSets,
+            Filename( DirectoriesPackageLibrary( "Toposes", "LogicForToposes" ), "PropositionsForToposes.tex" ) );
+    
     Finalize( cat );
 
     return cat;