Fabian Zickgraf

Thanks for the analysis and confirmation @sebastianpos! I will talk to @mohamed-barakat about how we shall proceed.

> I am for globally replacing `Range` with `Target`. \+ 1 @sebastianpos Would you be fine with this? > The use of `Range` is a `homalg` legacy: > > *...

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...

For future reference: I think the following PR might have partially overlapping ideas, in the Abelian context: https://github.com/homalg-project/CAP_project/pull/1211

> I encountered the problem in the nonlinear setup where `LiftAlongMonomorphism`/`ColiftAlongEpimorphism` should not be computable, but were automatically derived from `Lift`/`Colift`. I don't understand your point: If we can compute...

> You have to take the context into account: What we currently implicitly mean by `LiftAlongMonomorphism` is that the monomorphism is regular and that it has lifts as a kernel/equalizer...

I think we have a different understanding of the role of `CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD`. You seem to say that the entries in `CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbelianCategory` compared to the entries in `CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsPreAbelianCategory` are used to...

I now understand the point. I never expected `CheckConstructivenessOfCategory` to decide mathematical properties exactly due to the situation for `IsAbelianCategory`. And I think there are more cases where `CheckConstructivenessOfCategory` currently...

> After this discussion I would suggest to replace `LiftAlongMonomorphism` and `ColiftAlongEpimorphism` in `CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbelianCategory` by `InverseMorphismFromCoimageToImageWithGivenObjects`, maybe after renaming it to `InverseOfMorphismFromCoimageToImageWithGivenObjects`. I agree! > Side note: Neither `MorphismFromCoimageToImage` nor...