CAP_project
CAP_project copied to clipboard
homalg-project
derived ImageEmbedding as the colift along the coastriction to image
Codecov Report
Attention: 6 lines in your changes are missing coverage. Please review.
| Files | Coverage Δ | |
|---|---|---|
| CAP/PackageInfo.g | 100.00% <100.00%> (ø) |
|
| CAP/gap/DerivedMethods.autogen.gi | 86.93% <88.88%> (+0.03%) |
:arrow_up: |
| CAP/gap/DerivedMethods.gi | 84.00% <71.42%> (-0.11%) |
:arrow_down: |
:loudspeaker: Thoughts on this report? Let us know!.
![codecov[bot] avatar](https://avatars.githubusercontent.com/in/254?v=4 "Published by a pub.dev verified publisher"){kind=small}
Please also add a WithGiven version of the derivation to make it consistent with the analogous derivations of CoastrictionToImage(WithGiven...).
I just noticed that CAP's definition of Image does not require the coastriction to the image to be epi. Hence, in general this derivation is not valid, or am I missing something?
I just noticed that CAP's definition of Image does not require the coastriction to the image to be epi. Hence, in general this derivation is not valid, or am I missing something?
You are right, I have to use the general lift an colift.
You are right, I have to use the general lift an colift.
Such a factorization is always unique up to unique isomorphism.
It is now unclear to me why the colift is necessarily a monomorphism.
I restricted the derivation to IsAbelianCategory. I remember that the natural morphism from the coimage to image is both mono and epi, making these derivations also valid for IsPreAbelianCategory. I can relax the conditions in a later PR once I have a proof.