Missing properties of injection_of_cofactor and projection_in_factor

[mohamed-barakat]

In GeneralizedAddMethod.md you note:

• InjectionOfCofactorOfCoproduct/InjectionOfCofactorOfCoproductWithGivenCoproduct

  ## FIXME: it suffices that the category knows that it has a zero object
  if HasCanComputeZeroObject( category ) and CanComputeZeroObject( category ) then
  SetIsSplitMonomorphism( injection_of_cofactor, true );
  fi;

• ProjectionInFactorOfDirectProduct/ProjectionInFactorOfDirectProductWithGivenDirectProduct

  ## FIXME: it suffices that the category knows that it has a zero object
  if HasCanComputeZeroObject( category ) and CanComputeZeroObject( category ) then
  SetIsSplitEpimorphism( projection_in_factor, true );
  fi;

However, CanComputeZeroObject does not exist in CAP (anymore?). It would be nice to add the missing properties in contexts where they are true.

[sebastianpos]

• CanCompute now is an operation taking a category and a string as its arguments
• The infrastructure Cap provides for logical implications is given by the logic files. For this particular case, I can think of two possible solutions:

1. Add the property IsCategoryWithZeroObject as another kind of category Cap supports and create a logic file for this category
2. Simply add these theorems to the logic files of AdditiveCategories (although this is not the most general context in which these theorems hold)

[mohamed-barakat]

I see. Then I would prefer solution 2. Let me know if I should do this. Maybe it is a good exercise.