Merge pull request #1554 from zickgraf/master

Prove that the additive closure of a preadditive category has a zero object

Author: zickgraf

CompilerForCAP/PackageInfo.g

@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "CompilerForCAP",
 Subtitle := "Speed up and verify categorical algorithms",
-Version := "2023.12-24",
+Version := "2023.12-25",
 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",
 

CompilerForCAP/tst/300_proof_AdditiveClosure_has_a_zero_object.tst

@@ -0,0 +1,129 @@
+gap> START_TEST( "AdditiveClosure_has_a_zero_object" );
+
+#
+gap> LoadPackage( "FreydCategoriesForCAP", false );
+true
+
+#
+gap> dummy := DummyCategory( rec(
+>     list_of_operations_to_install := [
+>         "IsWellDefinedForObjects",
+>         "IsWellDefinedForMorphismsWithGivenSourceAndRange",
+>         "IsEqualForObjects",
+>         "IsCongruentForMorphisms",
+>         "ZeroMorphism",
+>     ],
+>     properties := [
+>         "IsAbCategory",
+>     ],
+> ) );;
+gap> cat := AdditiveClosure( dummy );;
+
+# set a human readable name
+gap> cat!.Name := "the additive closure of a preadditive category";;
+
+#
+gap> LoadPackage( "CompilerForCAP", false );
+true
+
+#
+gap> CapJitEnableProofAssistantMode( );
+
+#
+gap> StopCompilationAtPrimitivelyInstalledOperationsOfCategory( dummy );
+
+#
+gap> StateProposition( cat, "has_zero_object" );
+Proposition:
+The additive closure of a preadditive category has a zero object.
+
+# ZeroObject is well-defined
+gap> StateNextLemma( );
+
+
+Lemma 1:
+In the additive closure of a preadditive category, the zero object is an objec\
+t:
+We have
+function ( cat )
+    return IsWellDefinedForObjects( cat, ZeroObject( cat ) );
+end
+gap> AttestValidInputs( );
+We let CompilerForCAP assume that all inputs are valid.
+gap> AssertLemma( );
+With this, the claim follows. ∎
+
+# UniversalMorphismIntoZeroObject is well-defined
+gap> StateNextLemma( );
+
+
+Lemma 2:
+In the additive closure of a preadditive category, the universal morphism into\
+ the zero objects defines a morphism:
+For an object A we have
+function ( cat, A )
+    return IsWellDefinedForMorphismsWithGivenSourceAndRange( cat, A, 
+       UniversalMorphismIntoZeroObject( cat, A ), ZeroObject( cat ) );
+end
+gap> AttestValidInputs( );
+We let CompilerForCAP assume that all inputs are valid.
+gap> AssertLemma( );
+With this, the claim follows. ∎
+
+# UniversalMorphismIntoZeroObject is unique
+gap> StateNextLemma( );
+
+
+Lemma 3:
+In the additive closure of a preadditive category, the universal morphism into\
+ the zero object is unique:
+For an object A and a morphism u : A → ZeroObject( cat ) we have
+function ( cat, A, u )
+    return 
+     IsCongruentForMorphisms( cat, UniversalMorphismIntoZeroObject( cat, A ), 
+       u );
+end
+This is immediate from the construction.
+
+# UniversalMorphismFromZeroObject is well-defined
+gap> StateNextLemma( );
+
+
+Lemma 4:
+In the additive closure of a preadditive category, the universal morphism from\
+ the zero objects defines a morphism:
+For an object B we have
+function ( cat, B )
+    return IsWellDefinedForMorphismsWithGivenSourceAndRange( cat, 
+       ZeroObject( cat ), UniversalMorphismFromZeroObject( cat, B ), B );
+end
+gap> AttestValidInputs( );
+We let CompilerForCAP assume that all inputs are valid.
+gap> AssertLemma( );
+With this, the claim follows. ∎
+
+# UniversalMorphismFromZeroObject is unique
+gap> StateNextLemma( );
+
+
+Lemma 5:
+In the additive closure of a preadditive category, the universal morphism from\
+ the zero object is unique:
+For an object B and a morphism u : ZeroObject( cat ) → B we have
+function ( cat, B, u )
+    return 
+     IsCongruentForMorphisms( cat, UniversalMorphismFromZeroObject( cat, B ), 
+       u );
+end
+This is immediate from the construction.
+gap> AssertProposition( );
+
+
+Summing up, we have shown:
+The additive closure of a preadditive category has a zero object. ∎
+
+#
+gap> CapJitDisableProofAssistantMode( );
+
+#
+gap> STOP_TEST( "AdditiveClosure_has_a_zero_object" );

CompilerForCAP/tst/300_proof_CategoryOfRows_has_kernels.tst

@@ -16,7 +16,7 @@ gap> k!.RingElementFilter := IsHomalgRingElement;;
 #
 gap> cat := CategoryOfRows( k );;
 
-# set a humand readable name
+# set a human readable name
 gap> cat!.Name := "a category of rows over a field";;
 
 #