Open mohamed-barakat opened 11 months ago
I encountered the problem in the nonlinear setup where
LiftAlongMonomorphism
/ColiftAlongEpimorphism
should not be computable, but were automatically derived fromLift
/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 inCAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbelianCategory
compared to the entries inCAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsPreAbelianCategory
are used to distinguish between the categorical propertiesIsAbelianCategory
andIsPreAbelianCategory
. 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 forIsAbelianCategory
. And I think there are more cases whereCheckConstructivenessOfCategory
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 butLiftAlongMonomorphism
should not be computable, so you want to modify the derivation. In your third comment you say that the derivation ofLiftAlongMonomorphism
fromLift
is correct, butLiftAlongMonomorphism
should not be used inCAP_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
andColiftAlongEpimorphism
inCAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbelianCategory
byInverseMorphismFromCoimageToImageWithGivenObjects
, maybe after renaming it toInverseOfMorphismFromCoimageToImageWithGivenObjects
.
I agree!
Side note: Neither
MorphismFromCoimageToImage
norInverseMorphismFromCoimageToImage
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 :)
The ability to compute
LiftAlongMonomorphism
/ColiftAlongEpimorphism
is currently used to distinguish pre-abelian categories from abelian ones. However, inCAP
they can be derived from the set-theoretic operationsLift
/Colift
with no further restriction. This defeats their purpose.I encountered the problem in the nonlinear setup where
LiftAlongMonomorphism
/ColiftAlongEpimorphism
should not be computable, but were automatically derived fromLift
/Colift
.Solution: I would suggest adding the categorical properties
IsCategoryWithRegularMonos
/IsCategoryWithRegularEpis
(or better names) and only deriveLiftAlongMonomorphism
/ColiftAlongEpimorphism
fromLift
/Colift
only in caseIsCategoryWithRegularMonos
/IsCategoryWithRegularEpis
was set to true.