derived ImageEmbedding as the colift along the coastriction to image

[mohamed-barakat]

No description provided.

[codecov]

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%)	⬆️
CAP/gap/DerivedMethods.gi	84.00% <71.42%> (-0.11%)	⬇️

📢 Thoughts on this report? Let us know!.

[zickgraf]

Please also add a WithGiven version of the derivation to make it consistent with the analogous derivations of CoastrictionToImage(WithGiven...).

[zickgraf]

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?

[mohamed-barakat]

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.

[mohamed-barakat]

You are right, I have to use the general lift an colift.

Such a factorization is always unique up to unique isomorphism.

[mohamed-barakat]

It is now unclear to me why the colift is necessarily a monomorphism.

[mohamed-barakat]

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.