installed derivations for Abelian categories

[mohamed-barakat]

• IsomorphismFromKernelOfCokernelToImageObject
• IsomorphismFromCoimageToCokernelOfKernel

[mohamed-barakat]

This is a resurrection of #1196.

[codecov]

Codecov Report

Base: 76.75% // Head: 76.75% // No change to project coverage 👍

Coverage data is based on head (95ca8cb) compared to base (95ca8cb).
Patch has no changes to coverable lines.

❗ Current head 95ca8cb differs from pull request most recent head 8c109da. Consider uploading reports for the commit 8c109da to get more accurate results

Additional details and impacted files

@@           Coverage Diff           @@
##           master    #1211   +/-   ##
=======================================
  Coverage   76.75%   76.75%           
=======================================
  Files         494      494           
  Lines       60462    60462           
=======================================
  Hits        46405    46405           
  Misses      14057    14057           

Flag	Coverage Δ
ActionsForCAP	41.23% <0.00%> (ø)
AttributeCategoryForCAP	86.34% <0.00%> (ø)
CAP	81.85% <0.00%> (ø)
CartesianCategories	92.69% <0.00%> (ø)
CompilerForCAP	95.12% <0.00%> (ø)
ComplexesAndFilteredObjectsForCAP	73.17% <0.00%> (ø)
DeductiveSystemForCAP	25.48% <0.00%> (ø)
FreydCategoriesForCAP	80.75% <0.00%> (ø)
GeneralizedMorphismsForCAP	62.47% <0.00%> (ø)
GradedModulePresentationsForCAP	44.57% <0.00%> (ø)
GroupRepresentationsForCAP	49.72% <0.00%> (ø)
HomologicalAlgebraForCAP	73.21% <0.00%> (ø)
InternalExteriorAlgebraForCAP	40.24% <0.00%> (ø)
LinearAlgebraForCAP	66.27% <0.00%> (ø)
ModulePresentationsForCAP	68.93% <0.00%> (ø)
ModulesOverLocalRingsForCAP	90.02% <0.00%> (ø)
MonoidalCategories	87.00% <0.00%> (ø)
ToricSheaves	21.79% <0.00%> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

[zickgraf]

Please make this analogous to

CAP_project/CAP/gap/DerivedMethods.gi

Lines 1853 to 1864 in 64d67bd

	AddDerivationToCAP( IsomorphismFromImageObjectToKernelOfCokernel,
	function( cat, morphism )
	local kernel_emb, morphism_to_kernel;
	kernel_emb := KernelEmbedding( cat, CokernelProjection( cat, morphism ) );
	morphism_to_kernel := LiftAlongMonomorphism( cat, kernel_emb, morphism );
	return UniversalMorphismFromImage( cat, morphism, [ morphism_to_kernel, kernel_emb ] );
	end : Description := "IsomorphismFromImageObjectToKernelOfCokernel using the universal property of the image" );

, i.e. use the universality of the kernel (KernelLift).

[mohamed-barakat]

Now that I looked into it I am confused, isn't going through the kernel lift the wrong direction?

[zickgraf]

I have not thought this through in detail, but maybe/probably one also has to use the universality of the cokernel somewhere. And/or the property of being Abelian, i.e. InverseMorphismFromCoimageToImage? I will have to think more about this.

[zickgraf]

I think using the universality would mean using InverseMorphismFromCoimageToImage, IsomorphismFromCoimageToCokernelOfKernel and CokernelColift, which corresponds to how one proves that taking the kernel of the cokernel in an abelian category actually fulfills the universal property of an image. But I'm not sure if this really gives a better result.

[zickgraf]

Thinking more about this, I noticed that this is dangerous: Logic templates must respect the equality of objects and morphisms, i.e. in this case equality on the matrix level, to ensure consistency. In the concrete case, the results are uniquely determined, so this logic template actually gives equality on the matrix level, but it does not in general. The solution would be to introduce UniqueRightDivide and UniqueLeftDivide which can then be installed for (Co)LiftAlongMono/Epimorphism in MatrixCategory.

[zickgraf]

As just discussed verbally, I do not expect the current implementation to give something conceptionally different. And indeed, what this PR does simply corresponds to the rule UniqueRightDivide( HomalgIdentityMatrix( ... ), UniqueRightDivide( A, B ) ) ) = UniqueRightDivide( B, A ). Of course having this rule on a categorical level might be a good thing, but I think it would be interesting to first look at the suggestion above, which does something conceptionally different.

[mohamed-barakat]

I agree