From 52334d78cf16ea74f57dbc8aa0623709db96cd42 Mon Sep 17 00:00:00 2001
From: Martin Bies <MBies87@googlemail.com>
Date: Sat, 22 Jun 2019 15:10:57 +0200
Subject: [PATCH] Add embedding and best approximation functors for Freyd

---
 FreydCategoriesForCAP/gap/FreydCategory.gd |  68 ++++++++
 FreydCategoriesForCAP/gap/FreydCategory.gi | 190 +++++++++++++++++++++
 2 files changed, 258 insertions(+)

diff --git a/FreydCategoriesForCAP/gap/FreydCategory.gd b/FreydCategoriesForCAP/gap/FreydCategory.gd
index 60f93a51b9..38c1ed25b8 100644
--- a/FreydCategoriesForCAP/gap/FreydCategory.gd
+++ b/FreydCategoriesForCAP/gap/FreydCategory.gd
@@ -98,3 +98,71 @@ DeclareGlobalFunction( "IsValidInputForFreydCategory" );
 #! @Arguments objects a, b
 DeclareOperationWithCache( "INTERNAL_HOM_EMBEDDING",
                            [ IsFreydCategoryObject, IsFreydCategoryObject ] );
+
+
+####################################################
+##
+#! @Section Embedding functor for additive categories
+##
+####################################################
+
+#! @Description
+#! The argument is a CapCategory $C$. Provided that $C$ admits a Freyd category, this
+#! attribute will be set to be the embedding functor into this Freyd category.
+#! @Returns a functor
+#! @Arguments C
+DeclareAttribute( "EmbeddingIntoFreydCategory",
+                  IsCapCategory );
+
+
+####################################################
+##
+#! @Section Functor BestProjectiveApproximation
+##
+####################################################
+
+#! @Description
+#! The argument is an object $A$ in a Freyd category. The output will be
+#! the object in the underlying additive category, which serves as the best
+#! approximation of the given object $A$.
+#! @Returns an object in the underlying additive category
+#! @Arguments A
+DeclareAttribute( "BestProjectiveApproximation",
+                  IsFreydCategoryObject );
+
+#! @Description
+#! The argument is an object $A$ in a Freyd category. The output will be the
+#! canonical morphism from the object $A$ into this best projective
+#! approximation, the latter canonically understood as object in the Freyd category.
+#! @Returns a morphism in the Freyd category
+#! @Arguments A
+DeclareAttribute( "MorphismIntoBestProjectiveApproximation",
+                  IsCapCategoryObject );
+
+#! @Description
+#! The argument is a morphism $\alpha$ in a Freyd category. The output is the
+#! morphism in the underlying additive category, which best approximates $\alpha$.
+#! @Returns a morphism in the underlying additive category
+#! @Arguments $\alpha$
+DeclareAttribute( "BestProjectiveApproximation",
+                  IsCapCategoryMorphism );
+
+#! @Description
+#! The argument is a CapCategory $C$. Provided that $C$ admits a Freyd category, this
+#! attribute will be set to be the functor that maps objects and morphisms in the Freyd 
+#! category to their best projective approximations in the underlying additive category.
+#! @Returns a functor
+#! @Arguments C
+DeclareAttribute( "BestProjectiveApproximationFunctor",
+                  IsCapCategory );
+
+#! @Description
+#! The argument is a CapCategory $C$. Provided that $C$ admits a Freyd category, this
+#! attribute will be set to be the functor that maps objects and morphisms in the Freyd
+#! category to their best projective approximations in the underlying additive category.
+#! In contrast to BestProjectiveApproximationFunctor, we canonically embed these projective
+#! objects into the Freyd category. So this returns an autofunctor of the Freyd category.
+#! @Returns a functor
+#! @Arguments C
+DeclareAttribute( "BestEmbeddedProjectiveApproximationFunctor",
+                  IsCapCategory );
diff --git a/FreydCategoriesForCAP/gap/FreydCategory.gi b/FreydCategoriesForCAP/gap/FreydCategory.gi
index dcd283cbbb..bb3a64d9f2 100644
--- a/FreydCategoriesForCAP/gap/FreydCategory.gi
+++ b/FreydCategoriesForCAP/gap/FreydCategory.gi
@@ -1639,3 +1639,193 @@ InstallGlobalFunction( IsValidInputForFreydCategory,
     return result;
 
 end );
+
+
+#############################################################################
+##
+## Embedding of additive category into its Freyd category
+##
+#############################################################################
+
+InstallMethod( EmbeddingIntoFreydCategory,
+               [ IsCapCategory ],
+  function( additive_category )
+    local freyd_category, functor;
+        
+        # check for valid input
+        if not IsValidInputForFreydCategory( additive_category ) then
+        
+          Error( "The input category does not admit a Freyd category" );
+          return 0;
+        
+        fi;
+        
+        # define the Freyd category
+        freyd_category := FreydCategory( additive_category );
+        
+        # and set up the basics of this functor
+        functor := CapFunctor( Concatenation( "Embedding functor of ", Name( additive_category ),
+                               " into its Freyd category" ),
+                               additive_category,
+                               freyd_category
+                               );
+        
+        # now define the operation on the objects
+        AddObjectFunction( functor,
+        
+          function( object )
+            
+            return AsFreydCategoryObject( object );
+            
+        end );
+        
+        # and the operation on the morphisms
+        AddMorphismFunction( functor,
+        
+          function( new_source, morphism, new_range )
+            
+            return AsFreydCategoryMorphism( morphism );
+            
+        end );
+        
+        # and return this functor
+        return functor;
+        
+end );
+
+
+####################################################
+##
+## Section Functor BestProjectiveApproximation
+##
+####################################################
+
+## Morhpism into best projective approximation
+InstallMethod( MorphismIntoBestProjectiveApproximation,
+               [ IsFreydCategoryObject ],
+
+  function( freyd_object )
+    local mor;
+    
+    mor := WeakCokernelProjection( RelationMorphism( freyd_object ) );
+    
+    return FreydCategoryMorphism( freyd_object, mor, AsFreydCategoryObject( Range( mor ) ) );
+    
+end );
+
+## Best projective approximation of a Freyd_object
+InstallMethod( BestProjectiveApproximation,
+               [ IsFreydCategoryObject ],
+
+  function( freyd_object )
+    
+    return WeakCokernelObject( RelationMorphism( freyd_object ) );
+    
+end );
+
+## Best projective approximation of a Freyd_morphism
+InstallMethod( BestProjectiveApproximation,
+               [ IsFreydCategoryMorphism ],
+
+  function( freyd_mor )
+    local mor1, mor2, new_mor_datum;
+    
+    mor1 := MorphismIntoBestProjectiveApproximation( Source( freyd_mor ) );
+    mor2 := PreCompose( MorphismDatum( freyd_mor ), MorphismIntoBestProjectiveApproximation( Range( freyd_mor ) ) );
+    
+    return WeakColiftAlongEpimorphism( mor1, mor2 );
+    
+end );
+
+InstallMethod( BestProjectiveApproximationFunctor,
+               [ IsCapCategory ],
+  function( additive_category )
+    local freyd_category, functor;
+        
+        # check for valid input
+        if not IsValidInputForFreydCategory( additive_category ) then
+        
+          Error( "The input category does not admit a Freyd category" );
+          return 0;
+        
+        fi;
+        
+        # define the Freyd category
+        freyd_category := FreydCategory( additive_category );
+        
+        # and set up the basics of this functor
+        functor := CapFunctor( Concatenation( "Best projective approximation functor of the Freyd category of ", 
+                                              Name( additive_category ) ),
+                               freyd_category,
+                               additive_category
+                               );
+        
+        # now define the operation on the objects
+        AddObjectFunction( functor,
+        
+          function( object )
+            
+            return BestProjectiveApproximation( object );
+            
+        end );
+        
+        # and the operation on the morphisms
+        AddMorphismFunction( functor,
+        
+          function( new_source, morphism, new_range )
+            
+            return BestProjectiveApproximation( morphism );
+            
+        end );
+        
+        # and return this functor
+        return functor;
+        
+end );
+
+
+InstallMethod( BestEmbeddedProjectiveApproximationFunctor,
+               [ IsCapCategory ],
+  function( additive_category )
+    local freyd_category, functor;
+        
+        # check for valid input
+        if not IsValidInputForFreydCategory( additive_category ) then
+        
+          Error( "The input category does not admit a Freyd category" );
+          return 0;
+        
+        fi;
+        
+        # define the Freyd category
+        freyd_category := FreydCategory( additive_category );
+        
+        # and set up the basics of this functor
+        functor := CapFunctor( Concatenation( "Best embedded projective approximation functor of the Freyd category of ", 
+                                              Name( additive_category ) ),
+                               freyd_category,
+                               additive_category
+                               );
+        
+        # now define the operation on the objects
+        AddObjectFunction( functor,
+        
+          function( object )
+            
+            return AsFreydCategoryObject( BestProjectiveApproximation( object ) );
+            
+        end );
+        
+        # and the operation on the morphisms
+        AddMorphismFunction( functor,
+        
+          function( new_source, morphism, new_range )
+            
+            return AsFreydCategoryMorphism( BestProjectiveApproximation( morphism ) );
+            
+        end );
+        
+        # and return this functor
+        return functor;
+        
+end );