Merge pull request #603 from mohamed-barakat/ImageCoimage

regular ImageEmbedding/CoimageProjection in finite-bicomplete categories

FunctorCategories/PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "FunctorCategories",
 Subtitle := "Categories of functors",
-Version := "2024.11-01",
+Version := "2024.11-02",
 
 Date := ~.Version{[ 1 .. 10 ]},
 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)( ),
@@ -101,7 +101,7 @@ Dependencies := rec(
                    [ "LinearAlgebraForCAP", ">= 2024.08-07" ],
                    [ "FreydCategoriesForCAP", ">= 2024.08-07" ],
                    [ "SubcategoriesForCAP", ">= 2024.01-01" ],
-                   [ "Toposes", ">= 2024.06-02" ],
+                   [ "Toposes", ">= 2024.11-01" ],
                    [ "Locales", ">= 2024.03-23" ],
                    [ "FinSetsForCAP", ">= 2024.02-09" ],
                    [ "ToolsForHigherHomologicalAlgebra", ">= 2023.03-01" ],

FunctorCategories/examples/Dedekind2ndNumber.g

@@ -20,7 +20,7 @@ Display( Dist );
 #! A CAP category with name FreeDistributiveCompletion(
 #! PosetOfCategory( PathCategory( FinQuiver( "quiver(p,q)[]" ) ) ) ):
 #! 
-#! 58 primitive operations were used to derive 284 operations for this category
+#! 61 primitive operations were used to derive 293 operations for this category
 #! which algorithmically
 #! * IsCategoryWithDecidableColifts
 #! * IsCategoryWithDecidableLifts

Locales/PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "Locales",
 Subtitle := "Locales, frames, coframes, meet semi-lattices of locally closed subsets, and Boolean algebras of constructible sets",
-Version := "2024.10-03",
+Version := "2024.11-01",
 Date := ~.Version{[ 1 .. 10 ]},
 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",
@@ -107,6 +107,7 @@ Dependencies := rec(
                 [ "MonoidalCategories", ">= 2024.02-02" ],
                 [ "CartesianCategories", ">= 2024.02-02" ],
                 [ "ToolsForCategoricalTowers", ">= 2024.02-05" ],
+                [ "Toposes", ">= 2024.11-01" ],
                 [ "FpCategories", ">= 2024.02-11" ],
                 ],
   SuggestedOtherPackages := [

Locales/examples/ClosedMonoidalLatticeOfIdeals.g

@@ -17,7 +17,7 @@ Display( P );
 #! A CAP category with name
 #! PosetOfCategory( SliceCategoryOverTensorUnit( Rows( Q[x,y] ) ) ):
 #! 
-#! 17 primitive operations were used to derive 267 operations for this category
+#! 17 primitive operations were used to derive 276 operations for this category
 #! which algorithmically
 #! * IsCategoryWithDecidableColifts
 #! * IsCategoryWithDecidableLifts

Locales/examples/Dedekind1stNumber.g

@@ -12,7 +12,7 @@ IntervalCategory;
 Display( IntervalCategory );
 #! A CAP category with name IntervalCategory:
 #! 
-#! 21 primitive operations were used to derive 327 operations for this category
+#! 21 primitive operations were used to derive 336 operations for this category
 #!  which algorithmically
 #! * IsCategoryWithDecidableColifts
 #! * IsCategoryWithDecidableLifts
@@ -28,7 +28,7 @@ PSh := PreSheaves( IntervalCategory );
 Display( PSh );
 #! A CAP category with name PreSheaves( IntervalCategory, IntervalCategory ):
 #! 
-#! 58 primitive operations were used to derive 284 operations for this category
+#! 61 primitive operations were used to derive 293 operations for this category
 #! which algorithmically
 #! * IsCategoryWithDecidableColifts
 #! * IsCategoryWithDecidableLifts

Locales/examples/HeytingAlgebraOfRadicalIdeals.g

@@ -17,7 +17,7 @@ Display( P );
 #! A CAP category with name
 #! PosetOfCategory( SliceCategoryOverTensorUnit( Rows( Q[x,y] ) ) ):
 #! 
-#! 17 primitive operations were used to derive 267 operations for this category
+#! 17 primitive operations were used to derive 276 operations for this category
 #! which algorithmically
 #! * IsCategoryWithDecidableColifts
 #! * IsCategoryWithDecidableLifts
@@ -31,7 +31,7 @@ Display( L );
 #! StablePosetOfCategory( PosetOfCategory(
 #! SliceCategoryOverTensorUnit( Rows( Q[x,y] ) ) ) ):
 #! 
-#! 16 primitive operations were used to derive 329 operations for this category
+#! 16 primitive operations were used to derive 338 operations for this category
 #! which algorithmically
 #! * IsCategoryWithDecidableColifts
 #! * IsCategoryWithDecidableLifts

Toposes/PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "Toposes",
 Subtitle := "Elementary toposes",
-Version := "2024.09-03",
+Version := "2024.11-01",
 Date := ~.Version{[ 1 .. 10 ]},
 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",

Toposes/gap/ToposDerivedMethods.gi

@@ -145,9 +145,11 @@ AddDerivationToCAP( DirectProductComplement,
 
 end );
 
+## in a finite bicomplete category the regular image is the equalizer of cokernel pair
+## https://ncatlab.org/nlab/show/image#AsEqualizer
 ## Page 20 in Peter Freyd, Aspect of topoi, Bull. Austral. Math. Soc, 7 (1972)
 AddDerivationToCAP( ImageEmbedding,
-        "the (regular) image as the equalizer of the cokernel-pair",
+        "the regular image as the equalizer of the cokernel pair",
         [ [ EmbeddingOfEqualizer, 1 ],
           [ InjectionOfCofactorOfPushout, 2 ] ],
 
@@ -160,7 +162,25 @@ AddDerivationToCAP( ImageEmbedding,
                    [ InjectionOfCofactorOfPushout( cat, D, 1 ),
                      InjectionOfCofactorOfPushout( cat, D, 2 ) ] );
 
-end );
+end : CategoryFilter := IsFiniteBicompleteCategory );
+
+## in a finite bicomplete category the regular coimage is the coequalizer of kernel pair
+## https://ncatlab.org/nlab/show/image#AsEqualizer
+AddDerivationToCAP( CoimageProjection,
+        "the regular coimage as the equalizer of the kernel pair",
+        [ [ ProjectionOntoCoequalizer, 1 ],
+          [ ProjectionInFactorOfFiberProduct, 2 ] ],
+
+  function( cat, mor )
+    local D;
+
+    D := [ mor, mor ];
+
+    return ProjectionOntoCoequalizer( cat,
+                   [ ProjectionInFactorOfFiberProduct( cat, D, 1 ),
+                     ProjectionInFactorOfFiberProduct( cat, D, 2 ) ] );
+
+end : CategoryFilter := IsFiniteBicompleteCategory );
 
 ##
 AddDerivationToCAP( ImageEmbedding,