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

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

installed derivations for Abelian categories #1211

wants to merge 1 commit into from

Conversation

@mohamed-barakat
Copy link
Member

  • IsomorphismFromKernelOfCokernelToImageObject
  • IsomorphismFromCoimageToCokernelOfKernel

@mohamed-barakat
Copy link
Member Author

This is a resurrection of #1196.

@codecov
Copy link

codecov bot commented Dec 19, 2022 •
edited
Loading

Codecov Report

Base: 76.75% // Head: 76.75% // No change to project coverage 👍

Coverage data is based on head (95ca8cb) compared to base (95ca8cb).
Patch has no changes to coverable lines.

❗ Current head 95ca8cb differs from pull request most recent head 8c109da. Consider uploading reports for the commit 8c109da to get more accurate results

Additional details and impacted files 
@@           Coverage Diff           @@
##           master    #1211   +/-   ##
=======================================
  Coverage   76.75%   76.75%           
=======================================
  Files         494      494           
  Lines       60462    60462           
=======================================
  Hits        46405    46405           
  Misses      14057    14057
Flag Coverage Δ
ActionsForCAP 41.23% <0.00%> (ø)
AttributeCategoryForCAP 86.34% <0.00%> (ø)
CAP 81.85% <0.00%> (ø)
CartesianCategories 92.69% <0.00%> (ø)
CompilerForCAP 95.12% <0.00%> (ø)
ComplexesAndFilteredObjectsForCAP 73.17% <0.00%> (ø)
DeductiveSystemForCAP 25.48% <0.00%> (ø)
FreydCategoriesForCAP 80.75% <0.00%> (ø)
GeneralizedMorphismsForCAP 62.47% <0.00%> (ø)
GradedModulePresentationsForCAP 44.57% <0.00%> (ø)
GroupRepresentationsForCAP 49.72% <0.00%> (ø)
HomologicalAlgebraForCAP 73.21% <0.00%> (ø)
InternalExteriorAlgebraForCAP 40.24% <0.00%> (ø)
LinearAlgebraForCAP 66.27% <0.00%> (ø)
ModulePresentationsForCAP 68.93% <0.00%> (ø)
ModulesOverLocalRingsForCAP 90.02% <0.00%> (ø)
MonoidalCategories 87.00% <0.00%> (ø)
ToricSheaves 21.79% <0.00%> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

zickgraf
zickgraf suggested changes Dec 21, 2022
View reviewed changes
CAP/gap/DerivedMethods.gi
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.

LinearAlgebraForCAP/gap/CompilerLogic.gi Outdated
)
);

# RightDivide( B, A ) * RightDivide( A, C ) => RightDivide( B, C )
Copy link
Member

Choose a reason for hiding this comment

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

Thinking more about this, I noticed that this is dangerous: Logic templates must respect the equality of objects and morphisms, i.e. in this case equality on the matrix level, to ensure consistency. In the concrete case, the results are uniquely determined, so this logic template actually gives equality on the matrix level, but it does not in general. The solution would be to introduce UniqueRightDivide and UniqueLeftDivide which can then be installed for (Co)LiftAlongMono/Epimorphism in MatrixCategory.

@mohamed-barakat
installed derivations for Abelian categories
8c109da 
* IsomorphismFromKernelOfCokernelToImageObject
* IsomorphismFromCoimageToCokernelOfKernel
@zickgraf
Copy link
Member

As just discussed verbally, I do not expect the current implementation to give something conceptionally different. And indeed, what this PR does simply corresponds to the rule UniqueRightDivide( HomalgIdentityMatrix( ... ), UniqueRightDivide( A, B ) ) ) = UniqueRightDivide( B, A ). Of course having this rule on a categorical level might be a good thing, but I think it would be interesting to first look at the suggestion above, which does something conceptionally different.

@mohamed-barakat
Copy link
Member Author

I agree

@zickgraf zickgraf mentioned this pull request Oct 4, 2023
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@zickgraf zickgraf zickgraf requested changes

Reviewers whose approvals may not affect merge requirements

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

waiting for author

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@mohamed-barakat @zickgraf