Skip to content

installed derivations for Abelian categories #1211

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

installed derivations for Abelian categories #1211

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion CAP/PackageInfo.g
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ SetPackageInfo( rec(

PackageName := "CAP",
Subtitle := "Categories, Algorithms, Programming",
Version := "2022.12-15",
Version := "2022.12-16",
Date := Concatenation( "01/", ~.Version{[ 6, 7 ]}, "/", ~.Version{[ 1 .. 4 ]} ),
License := "GPL-2.0-or-later",

Expand Down
40 changes: 40 additions & 0 deletions CAP/gap/DerivedMethods.gi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1820,6 +1820,26 @@ AddDerivationToCAP( IsomorphismFromKernelOfCokernelToImageObject,

end : Description := "IsomorphismFromKernelOfCokernelToImageObject as the inverse of IsomorphismFromImageObjectToKernelOfCokernel" );

##
AddDerivationToCAP( IsomorphismFromKernelOfCokernelToImageObject,
[ [ ImageEmbedding, 1 ],
[ CokernelProjection, 1 ],
[ KernelEmbedding, 1 ],
[ LiftAlongMonomorphism, 1 ] ],

function( cat, mor )
local image_embedding, ker_of_coker_embedding;

image_embedding := ImageEmbedding( cat, mor );

ker_of_coker_embedding := KernelEmbedding( cat, CokernelProjection( cat, mor ) );

return LiftAlongMonomorphism( cat, image_embedding, ker_of_coker_embedding );

end : CategoryFilter := IsAbelianCategory, ##FIXME: PreAbelian?
Description := "IsomorphismFromKernelOfCokernelToImageObject as the unique lift of the kernel of the cokernel along the image embedding"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please make this analogous to

CAP_project/CAP/gap/DerivedMethods.gi

Lines 1853 to 1864 in 64d67bd

AddDerivationToCAP( IsomorphismFromImageObjectToKernelOfCokernel,
function( cat, morphism )
local kernel_emb, morphism_to_kernel;
kernel_emb := KernelEmbedding( cat, CokernelProjection( cat, morphism ) );
morphism_to_kernel := LiftAlongMonomorphism( cat, kernel_emb, morphism );
return UniversalMorphismFromImage( cat, morphism, [ morphism_to_kernel, kernel_emb ] );
end : Description := "IsomorphismFromImageObjectToKernelOfCokernel using the universal property of the image" );
, i.e. use the universality of the kernel (KernelLift).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Now that I looked into it I am confused, isn't going through the kernel lift the wrong direction?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have not thought this through in detail, but maybe/probably one also has to use the universality of the cokernel somewhere. And/or the property of being Abelian, i.e. InverseMorphismFromCoimageToImage? I will have to think more about this.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think using the universality would mean using InverseMorphismFromCoimageToImage, IsomorphismFromCoimageToCokernelOfKernel and CokernelColift, which corresponds to how one proves that taking the kernel of the cokernel in an abelian category actually fulfills the universal property of an image. But I'm not sure if this really gives a better result.

);

##
AddDerivationToCAP( IsomorphismFromImageObjectToKernelOfCokernel,

Expand Down Expand Up @@ -1875,6 +1895,26 @@ AddDerivationToCAP( IsomorphismFromCoimageToCokernelOfKernel,

end : Description := "IsomorphismFromCoimageToCokernelOfKernel as the inverse of IsomorphismFromCokernelOfKernelToCoimage" );

##
AddDerivationToCAP( IsomorphismFromCoimageToCokernelOfKernel,
[ [ CoimageProjection, 1 ],
[ KernelEmbedding, 1 ],
[ CokernelProjection, 1 ],
[ ColiftAlongEpimorphism, 1 ] ],

function( cat, mor )
local coimage_projection, coker_of_ker_projection;

coimage_projection := CoimageProjection( cat, mor );

coker_of_ker_projection := CokernelProjection( cat, KernelEmbedding( cat, mor ) );

return ColiftAlongEpimorphism( cat, coimage_projection, coker_of_ker_projection );

end : CategoryFilter := IsAbelianCategory, ##FIXME: PreAbelian?
Description := "IsomorphismFromCoimageToCokernelOfKernel as the unique colift of the cokernel of the kernel along the coimage projection"
);

##
AddDerivationToCAP( IsomorphismFromFiberProductToKernelOfDiagonalDifference,

Expand Down
4 changes: 2 additions & 2 deletions LinearAlgebraForCAP/PackageInfo.g
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ SetPackageInfo( rec(

PackageName := "LinearAlgebraForCAP",
Subtitle := "Category of Matrices over a Field for CAP",
Version := "2022.12-04",
Version := "2022.12-05",
Date := Concatenation( "01/", ~.Version{[ 6, 7 ]}, "/", ~.Version{[ 1 .. 4 ]} ),
License := "GPL-2.0-or-later",

Expand Down Expand Up @@ -89,7 +89,7 @@ Dependencies := rec(
NeededOtherPackages := [ [ "ToolsForHomalg", ">=2015.09.18" ],
[ "MatricesForHomalg", ">= 2021.12-01" ],
[ "GaussForHomalg", ">= 2021.04-02" ],
[ "CAP", ">= 2022.12-07" ],
[ "CAP", ">= 2022.12-16" ],
[ "MonoidalCategories", ">= 2022.06-01" ],
],
SuggestedOtherPackages := [
Expand Down
24 changes: 11 additions & 13 deletions LinearAlgebraForCAP/gap/precompiled_categories/MatrixCategoryPrecompiled.gi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2165,16 +2165,15 @@ end

########
function ( cat_1, C_1, alpha_1, I_1 )
local morphism_attr_1_1, deduped_2_1, deduped_3_1, deduped_4_1;
deduped_4_1 := UnderlyingRing( cat_1 );
local morphism_attr_1_1, deduped_2_1, deduped_3_1;
deduped_3_1 := UnderlyingMatrix( alpha_1 );
deduped_2_1 := SyzygiesOfRows( SyzygiesOfColumns( deduped_3_1 ) );
morphism_attr_1_1 := RightDivide( HomalgIdentityMatrix( RowRankOfMatrix( deduped_3_1 ), deduped_4_1 ), RightDivide( LeftDivide( BasisOfColumns( deduped_3_1 ), deduped_3_1 ), deduped_2_1 ) * RightDivide( HomalgIdentityMatrix( NumberRows( deduped_2_1 ), deduped_4_1 ), RightDivide( BasisOfRows( deduped_3_1 ), deduped_2_1 ) ) );
morphism_attr_1_1 := RightDivide( HomalgIdentityMatrix( RowRankOfMatrix( deduped_3_1 ), UnderlyingRing( cat_1 ) ), RightDivide( LeftDivide( BasisOfColumns( deduped_3_1 ), deduped_3_1 ), deduped_2_1 ) * RightDivide( deduped_2_1, BasisOfRows( deduped_3_1 ) ) );
return CreateCapCategoryMorphismWithAttributes( cat_1, CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberRows( morphism_attr_1_1 ) ), C_1, UnderlyingMatrix, morphism_attr_1_1 );
end
########

, 1817 : IsPrecompiledDerivation := true );
, 1512 : IsPrecompiledDerivation := true );

##
AddIsAutomorphism( cat,
Expand Down Expand Up @@ -2603,12 +2602,12 @@ end
function ( cat_1, alpha_1 )
local morphism_attr_1_1, deduped_2_1;
deduped_2_1 := UnderlyingMatrix( alpha_1 );
morphism_attr_1_1 := RightDivide( HomalgIdentityMatrix( ColumnRankOfMatrix( deduped_2_1 ), UnderlyingRing( cat_1 ) ), LeftDivide( SyzygiesOfColumns( SyzygiesOfRows( deduped_2_1 ) ), BasisOfColumns( deduped_2_1 ) ) );
morphism_attr_1_1 := LeftDivide( BasisOfColumns( deduped_2_1 ), SyzygiesOfColumns( SyzygiesOfRows( deduped_2_1 ) ) );
return CreateCapCategoryMorphismWithAttributes( cat_1, CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberRows( morphism_attr_1_1 ) ), CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberColumns( morphism_attr_1_1 ) ), UnderlyingMatrix, morphism_attr_1_1 );
end
########

, 808 : IsPrecompiledDerivation := true );
, 503 : IsPrecompiledDerivation := true );

##
AddIsomorphismFromCokernelOfDiagonalDifferenceToPushout( cat,
Expand Down Expand Up @@ -2984,15 +2983,14 @@ end

########
function ( cat_1, alpha_1 )
local morphism_attr_1_1, deduped_2_1, deduped_3_1;
deduped_3_1 := UnderlyingMatrix( alpha_1 );
deduped_2_1 := SyzygiesOfRows( SyzygiesOfColumns( deduped_3_1 ) );
morphism_attr_1_1 := RightDivide( HomalgIdentityMatrix( NumberRows( deduped_2_1 ), UnderlyingRing( cat_1 ) ), RightDivide( BasisOfRows( deduped_3_1 ), deduped_2_1 ) );
local morphism_attr_1_1, deduped_2_1;
deduped_2_1 := UnderlyingMatrix( alpha_1 );
morphism_attr_1_1 := RightDivide( SyzygiesOfRows( SyzygiesOfColumns( deduped_2_1 ) ), BasisOfRows( deduped_2_1 ) );
return CreateCapCategoryMorphismWithAttributes( cat_1, CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberRows( morphism_attr_1_1 ) ), CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberColumns( morphism_attr_1_1 ) ), UnderlyingMatrix, morphism_attr_1_1 );
end
########

, 808 : IsPrecompiledDerivation := true );
, 503 : IsPrecompiledDerivation := true );

##
AddIsomorphismFromKernelOfDiagonalDifferenceToFiberProduct( cat,
Expand Down Expand Up @@ -4142,12 +4140,12 @@ function ( cat_1, C_1, alpha_1, I_1 )
local morphism_attr_1_1, deduped_2_1, deduped_3_1;
deduped_3_1 := UnderlyingMatrix( alpha_1 );
deduped_2_1 := SyzygiesOfRows( SyzygiesOfColumns( deduped_3_1 ) );
morphism_attr_1_1 := RightDivide( LeftDivide( BasisOfColumns( deduped_3_1 ), deduped_3_1 ), deduped_2_1 ) * RightDivide( HomalgIdentityMatrix( NumberRows( deduped_2_1 ), UnderlyingRing( cat_1 ) ), RightDivide( BasisOfRows( deduped_3_1 ), deduped_2_1 ) );
morphism_attr_1_1 := RightDivide( LeftDivide( BasisOfColumns( deduped_3_1 ), deduped_3_1 ), deduped_2_1 ) * RightDivide( deduped_2_1, BasisOfRows( deduped_3_1 ) );
return CreateCapCategoryMorphismWithAttributes( cat_1, C_1, CreateCapCategoryObjectWithAttributes( cat_1, Dimension, NumberColumns( morphism_attr_1_1 ) ), UnderlyingMatrix, morphism_attr_1_1 );
end
########

, 1614 : IsPrecompiledDerivation := true );
, 1309 : IsPrecompiledDerivation := true );

##
AddMorphismFromFiberProductToSink( cat,
Expand Down