search

homalg-project / CAP_project

CAP project -- Categories, Algorithms, and Programming
https://homalg-project.github.io/docs/CAP_project-based/
24 stars 18 forks source link

When using only_primitive_operations in OppositeCategory prevents the installation of the hom structure if the hom structure in the underlying category is derived #1249

Closed mohamed-barakat closed 1 year ago

mohamed-barakat commented 1 year ago

This issue should be addressed before https://github.com/homalg-project/CAP_project/pull/1240 is merged.

zickgraf commented 1 year ago

Does this problem get worse with #1240? If yes, why? If no, why do you want to address it together with #1240?

mohamed-barakat commented 1 year ago

PR #1240 had multiple versions and is not yet in final form so it is difficult to answer the question at this point:

But here is the issue with the opposite category constructor further detailed:

In line https://github.com/homalg-project/CAP_project/blob/5d2f3fa735cb6095a2f9d5e044a1738b31f2ff4a/CAP/gap/OppositeCategory.gi#L72 the range category is manually set.

  1. Currently (i.e., without #1240), this prevents the final derivations from triggering since they all require the range category not to be set, e.g. when the opposite category happens to be cartesian or monoidal closed.
  2. On the other side, if the operations of the homomorphism structures of the underlying category are not primitively installed (e.g., themselves installed by a final derivation), they are not installed if the option only_primitive_operations is set to true.
  3. The wrapper category constructor applied to this opposite category will find the range category set but won't find the operations for the homomorphism structure, so it will not set the range category for the wrapper category and the final derivations might now be triggered for the latter.

This asymmetry can be fixed for the current master branch (093bbcd1032bc93cc7ed60ee61f8a1cd28e90be1) and prior to PR #1240 by preventing the opposite category constructor from setting the range category if it is not able to install the operations of the homomorphism structure.

Now PR #1240 reverses the situation and expects the range category to be set for the final derivations to be triggered.

zickgraf commented 1 year ago

Ah, thanks for the details, I wasn't aware that WrapperCategory also plays a role here.