The role of CanonicalIdentificationFromCoimageToImageObject

[zickgraf]

CanonicalIdentificationFromCoimageToImageObject was added relatively recently in 6c409ef (2019), but grepping shows no code using it. @sebastianpos Do you recall for which application you added it?

The role of CanonicalIdentificationFromCoimageToImageObject and its dual are unclear to me. Is it the same as MorphismFromCoimageToImage, just in an Abelian category? Or in any category where images and coimages are isomorphic?

Also, I missed to rename CanonicalIdentificationFromCoimageToImageObject to CanonicalIdentificationFromCoimage*Object*ToImageObject in 81d7767. But then again, MorphismFromCoimageToImage does not contain Object at all. I guess the names should be consistent.

[sebastianpos]

I cannot recall. I'm sorry.

It probably was meant for the abelian context. Anyway, you may get rid of it if you want to.

[zickgraf]

@sebastianpos Thanks for the fast reply! I'm planning to automatically dualize derivations as an application of CompilerForCAP, and since the derivations around CanonicalIdentificationFromCoimageToImageObject are not symmetric with regard to dualization, I indeed would like to get rid of it.

While trying to remove it, I noticed that there actually is a derivation for it, in Toposes: homalg-project/Toposes@3f9d8f0. This derivation was added right after the introduction in CAP, so that seems to be the application. @mohamed-barakat Do you need this derivation? If yes, could you also use MorphismFromCoimageToImage?

[mohamed-barakat]

@mohamed-barakat Do you need this derivation? If yes, could you also use MorphismFromCoimageToImage?

I don't know. You can delete it an we can see :)