installed derivations for Abelian categories #1211
Conversation
mohamed-barakat
commented
Dec 19, 2022
mohamed-barakat
commented
- IsomorphismFromKernelOfCokernelToImageObject
- IsomorphismFromCoimageToCokernelOfKernel
|
This is a resurrection of #1196. |
mohamed-barakat
force-pushed
the
Derivations
branch
from
0af42c7
to
64d67bd
Compare
Codecov ReportBase: 76.75% // Head: 76.75% // No change to project coverage 👍
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
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. |
| 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" |
There was a problem hiding this comment.
Please make this analogous to
CAP_project/CAP/gap/DerivedMethods.gi
Lines 1853 to 1864 in 64d67bd
There was a problem hiding this comment.
Now that I looked into it I am confused, isn't going through the kernel lift the wrong direction?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
| @@ -54,3 +54,13 @@ CapJitAddLogicTemplate( | |||
| needed_packages := [ [ "MatricesForHomalg", ">= 2020.05.19" ] ], | |||
| ) | |||
| ); | |||
|
|
|||
| # RightDivide( B, A ) * RightDivide( A, C ) => RightDivide( B, C ) | |||
There was a problem hiding this comment.
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.
* IsomorphismFromKernelOfCokernelToImageObject * IsomorphismFromCoimageToCokernelOfKernel
mohamed-barakat
force-pushed
the
Derivations
branch
from
64d67bd
to
8c109da
Compare
|
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 |
|
I agree |
