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 lifts along arbitrary morphisms, we can certainly compute lifts along monomorphisms. So how can LiftAlongMonomorphism not be computable in a case where Lift is?

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

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

That would be an undocumented assumption regarding the input of LiftAlongMonomorphism. But the derivation should still be correct: For example in the case that a category has no regular monos at all and one requires the input of LiftAlongMonomorphism to be a regular mono, any implementation will fulfill the specification.

Why should the mere existence of the operation LiftAlongMonomorphism imply that every mono in the category is a regular mono?

That would be an undocumented assumption regarding the input of LiftAlongMonomorphism.

Yes, we use it implicitly in the definition of CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbelianCategory

But the derivation should still be correct: For example in the case that a category has no regular monos at all and one requires the input of LiftAlongMonomorphism to be a regular mono, any implementation will fulfill the specification.

Yes, the derivation is correct, but its computability should not be implicitly used distinguish IsAbelianCategory for IsPreAbelianCategory.

Why should the mere existence of the operation LiftAlongMonomorphism imply that every mono in the category is a regular mono?

It does not, and this is the point :)

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 distinguish between the categorical properties IsAbelianCategory and IsPreAbelianCategory. But I don't see where this is the case.

The entries of CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbelianCategory are used to distinguish between non-constructive Abelian categories and constructive Abelian categories. So the entries of CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbelianCategory only are of relevance if the category already has the property IsAbelianCategory. In a constructive Abelian category, every mono is regular and we can compute KernelLift, so we expect to be able to compute LiftAlongMonomorphism. That's why LiftAlongMonomorphism is in the list CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbelianCategory.

In particular I think that CheckConstructivenessOfCategory only has a well-defined meaning if the category already has the corresponding mathematical property.

For further discussion:

gap> LoadPackage( "Freyd", false );
true
gap> zz := HomalgRingOfIntegers( );
Z
gap> ZZ_freemods := CategoryOfRows( zz );
Rows( Z )
gap> HasIsAbelianCategory( ZZ_freemods );
false
gap> CheckConstructivenessOfCategory( ZZ_freemods, "IsAbelianCategory" );
[ "KernelObject", "KernelEmbedding", "KernelLift", "CokernelObject", "CokernelProjection", "CokernelColift" ]

If we would install the missing CAP operations, which we can since ZZ_freemods is indeed pre-abelian, then CheckConstructivenessOfCategory would return an empty list.

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 distinguish between the categorical properties IsAbelianCategory and IsPreAbelianCategory. But I don't see where this is the case.

Yes, we have different expectations for the role of CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD. I expect that when I can compute the algorithms listed for a specific doctrine then the category lies in this doctrine constructively.

Here is an example in ZZ_freemods you are aware of:

The cokernel projection of the monomorphism 2:ℤ → ℤ is 0:ℤ → 0. However, the former cannot lift 1:ℤ → ℤ although its composition with the latter is zero.

It is this sort of LiftAlongMonomorphism that I am expecting in CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbelianCategory.

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 cannot be used to decide mathematical properties.

I still do not understand which solution you propose: In your first comment, you say that you have a setup where Lift is computable but LiftAlongMonomorphism should not be computable, so you want to modify the derivation. In your third comment you say that the derivation of LiftAlongMonomorphism from Lift is correct, but LiftAlongMonomorphism should not be used in CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.

Regarding regular monos: I think this notion is intricate in the context of CAP. At least when reading the definition naively, then "every mono is a regular mono" implies that "every object is a kernel object". The latter does not hold true in LazyCategory( abelian_category ).

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 cannot be used to decide mathematical properties.

I still do not understand which solution you propose: In your first comment, you say that you have a setup where Lift is computable but LiftAlongMonomorphism should not be computable, so you want to modify the derivation. In your third comment you say that the derivation of LiftAlongMonomorphism from Lift is correct, but LiftAlongMonomorphism should not be used in CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.

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.

Regarding regular monos: I think this notion is intricate in the context of CAP. At least when reading the definition naively, then "every mono is a regular mono" implies that "every object is a kernel object". The latter does not hold true in LazyCategory( abelian_category ).

I would say it would imply "every object is isomorphic to a kernel object".

Addendum: InverseMorphismFromCoimageToImageWithGivenObjects is currently correctly installed by a derivation for IsAbelianCategory, so we won't run into the situation I criticized above for ZZ_freemods. The user who wants to implement a new abelian category will eventually only have [ InverseMorphismFromCoimageToImageWithGivenObjects ] as the output of CheckConstructivenessOfCategory. Then she has to invoke DerivationsOfMethodByCategory( ..., "InverseMorphismFromCoimageToImageWithGivenObjects" ) to see that she needs to install InverseForMorphisms and MorphismFromCoimageToImageWithGivenObjects after marking the category IsAbelianCategory.

Side note: Neither MorphismFromCoimageToImage nor InverseMorphismFromCoimageToImage are CAP operations, they are only GAP operations. Are they simply missing?

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 InverseMorphismFromCoimageToImage are CAP operations, they are only GAP operations. Are they simply missing?

I had not noticed this before, good catch. Yes, I think the are simply missing and could/should be added.

Wonderful, we are converging :)